зеркало из https://github.com/microsoft/ivy.git
35 строки
681 B
XML
35 строки
681 B
XML
#lang ivy1.7
|
|
|
|
type node
|
|
isolate nset = {
|
|
type this
|
|
relation member(N:node, S:this)
|
|
individual emptyset : nset
|
|
invariant ~member(N, emptyset)
|
|
implementation {
|
|
|
|
relation _member(N:node, S:this)
|
|
definition member(N, S) = _member(N, S)
|
|
after init {
|
|
_member(N, emptyset) := false;
|
|
}
|
|
}
|
|
|
|
specification {
|
|
after init {
|
|
ensure ~member(N, emptyset)
|
|
}
|
|
}
|
|
}
|
|
with node
|
|
|
|
object localstate = {
|
|
individual my_voters : nset
|
|
invariant ~nset.member(VOTER, my_voters)
|
|
after init {
|
|
my_voters := nset.emptyset;
|
|
}
|
|
} #localstate
|
|
|
|
isolate ilocalstate = localstate with nset, node
|