Order
module totally_ordered(t) = {
property [transitivity] (T:t < U & U < V) -> (T < V)
property [antisymmetry] ~(T:t < U & U < T)
property [totality] T:t < U | T = U | U < T
}
module totally_ordered_with_zero(t) = {
instantiate totally_ordered(t)
property 0 <= X:t
}
module unbounded_sequence = {
type this
alias t = this
action next(x:t) returns (y:t)
action prev(x:t) returns (y:t)
relation succ(X:t,Y:t)
object spec = {
property succ(X,Z) -> (X < Z & ~(X < Y & Y < Z))
instantiate totally_ordered_with_zero(t)
after next {
assert x < y & (x < Y -> y <= Y);
assert succ(x,y)
}
before prev {
assert 0 < x
}
after prev {
assert y < x & (Y < x -> Y <= y);
assert succ(y,x)
}
}
object impl = {
interpret t -> nat
definition succ(X,Y) = (Y = X + 1)
implement next {
y := x + 1
}
implement prev {
y := x - 1
}
}
isolate iso = impl,spec
attribute test = impl
}
module long_unbounded_sequence = {
type this
alias t = this
action next(x:t) returns (y:t)
action prev(x:t) returns (y:t)
relation succ(X:t,Y:t)
object spec = {
property succ(X,Z) -> (X < Z & ~(X < Y & Y < Z))
instantiate totally_ordered_with_zero(t)
after next {
assert x < y & (x < Y -> y <= Y);
assert succ(x,y)
}
before prev {
assert 0 < x
}
after prev {
assert y < x & (Y < x -> Y <= y);
assert succ(y,x)
}
}
object impl = {
interpret t -> longbv[1][13][16]
definition succ(X,Y) = (Y = X + 1)
implement next {
<<<
y.val = x.val + 1;
>>>
}
implement prev {
<<<
y.val = x.val - 1;
>>>
}
}
isolate iso = impl,spec
attribute test = impl
}
module bounded_sequence_spec = {
type this
alias t = this
action next(x:t) returns (y:t)
action prev(x:t) returns (y:t)
action is_max(x:t) returns (r:bool)
relation succ(X:t,Y:t)
object spec = {
property N:t >= 0
property succ(X,Z) -> (X < Z & ~(X < Y & Y < Z))
instantiate totally_ordered(t)
before next {
assert exists S. S > x;
}
after next {
assert x < y & (x < Y -> y <= Y);
assert succ(x,y)
}
before prev {
assert 0 < x
}
after prev {
assert y < x & (Y < x -> Y <= y);
assert succ(y,x)
}
after is_max {
assert r <-> ~exists S. S > x
}
}
}
module bounded_sequence(interp) = {
instantiate bounded_sequence_spec
object impl = {
interpret t -> interp
definition succ(X,Y) = (Y = X + 1 & X < Y)
implement next {
y := x + 1
}
implement prev {
y := x - 1
}
implement is_max {
r := ~(x + 1 > x)
}
}
isolate iso = impl,spec
attribute test = impl
}
module bit_vector(length) = {
instantiate bounded_sequence(bv[length])
action random returns (res:this)
implementation {
implement random {
<<<
res = 0;
for (int b = `length`; b > 0; b -= 15) {
int q = ( b < 15 ) ? b : 15;
res = (res << q) | (::random() & ~(-1 << q));
}
>>>
}
}
}
module order_iterator(range) = {
type t = struct {
is_end : bool,
val : range.t
}
definition (X < Y) = ~is_end(X) & is_end(Y)
| ~is_end(X) & ~is_end(Y) & val(X) < val(Y)
function done(X,Y) = is_end(Y) | X < val(Y)
function ahead(X,Y) = ~is_end(Y) & val(Y) < X
function between(X,V,Y) = ~done(V,X) & done(V,Y)
action create(x:range.t) returns (y:t)
action end returns (y:t)
object spec = {
after create {
assert ~is_end(y);
assert val(y) = x
}
after end {
assert is_end(y);
assert val(y) = 0
}
}
object impl = {
implement create {
is_end(y) := false;
val(y) := x
}
implement end {
is_end(y) := true;
val(y) := 0
}
}
isolate iso = impl,spec with range
attribute test = impl
}
module order_iterator_impl(range) = {
type t = struct {
is_end : bool,
val : range.t
}
definition (X < Y) = ~is_end(X) & is_end(Y)
| ~is_end(X) & ~is_end(Y) & val(X) < val(Y)
function done(X,Y) = is_end(Y) | X < val(Y)
function ahead(X,Y) = ~is_end(Y) & val(Y) < X
function between(X,V,Y) = ~done(V,X) & done(V,Y)
action create(x:range.t) returns (y:t)
action end returns (y:t)
implement create {
is_end(y) := false;
val(y) := x
}
implement end {
is_end(y) := true;
val(y) := 0
}
}
module sequence_iterator(range) = {
instantiate order_iterator(range)
action next(x:t) returns (x:t)
action prev(x:t) returns (x:t)
object spec = {
...
before next {
assert ~is_end(x)
}
after next {
assert X <= val(old x) & is_end(x)
| ~(val(old x) < Y & Y < val(x))
& val(old x) < val(x) & ~is_end(x)
}
before prev {
assert is_end(x) | exists X. X < val(x)
}
after prev {
assert ~is_end(x);
assert X <= val(x) & is_end(old x)
| ~(val(x) < Y & Y < val(old x))
& val(x) < val(old x) & ~is_end(old x)
}
}
object impl = {
...
implement next {
if range.is_max(val(x)) {
x := end
} else {
x := create(range.next(val(x)))
}
}
implement prev {
x := create(range.prev(val(x)))
}
}
}
¤
Queue
¤
module unbounded_queue(data) = {
instance index : unbounded_sequence
individual head : index.t
individual tail : index.t
function contents(X:index.t) : data
after init {
head := 0;
tail := 0;
}
derived empty = tail >= head
derived first = contents(tail)
action push(d:data) = {
contents(head) := d;
head := head.next;
}
action pop returns (res:data) = {
assert ~empty;
res := contents(tail);
tail := tail.next;
}
delegate pop
}
¤
Iterable
This is a totally ordered sort that can be iterated over. It's good, for example, for process ID's.
¤
module iterable = {
instantiate bounded_sequence_spec
instance iter : sequence_iterator(this)
isolate iso_iter = iter with this
individual max : t
specification {
property 0 <= X:t & X <= max
}
implementation {
parameter size : t
interpret t -> <<< int >>>
definition (x:t < y:t) = <<< x < y >>>
definition (x:t - y:t) = <<< x - y >>>
definition 0:t = <<< 0 >>>
definition max = <<< `size` - 1 >>>
implement next(x:t) returns (y:t) {
<<< y = x + 1; >>>
}
implement prev(x:t) returns (y:t) {
<<< y = x - 1; >>>
}
implement is_max(x:t) returns (r:bool) {
<<< r = (x == `size` - 1); >>>
}
}
trusted isolate iso = this
attribute cardinality = size
attribute test = impl
}