diff options
Diffstat (limited to 'tests/examplefiles/test.sil')
-rw-r--r-- | tests/examplefiles/test.sil | 206 |
1 files changed, 0 insertions, 206 deletions
diff --git a/tests/examplefiles/test.sil b/tests/examplefiles/test.sil deleted file mode 100644 index 3bcee835..00000000 --- a/tests/examplefiles/test.sil +++ /dev/null @@ -1,206 +0,0 @@ -domain Option__Node { - unique function Option__Node__Some(): Option__Node - unique function Option__Node__None(): Option__Node - - function variantOfOptionNode(self: Ref): Option__Node - - function isOptionNode(self: Ref): Bool - - axiom ax_variantOfOptionNodeChoices { - forall x: Ref :: { variantOfOptionNode(x) } - (variantOfOptionNode(x) == Option__Node__Some() || variantOfOptionNode(x) == Option__Node__None()) - } - - axiom ax_isCounterState { - forall x: Ref :: { variantOfOptionNode(x) } - isOptionNode(x) == (variantOfOptionNode(x) == Option__Node__Some() || - variantOfOptionNode(x) == Option__Node__None()) - } -} - -predicate validOption(this: Ref) { - isOptionNode(this) && - variantOfOptionNode(this) == Option__Node__Some() ==> ( - acc(this.Option__Node__Some__1, write) && - acc(validNode(this.Option__Node__Some__1)) - ) -} - -field Option__Node__Some__1: Ref - -field Node__v: Int -field Node__next: Ref - -predicate validNode(this: Ref) { - acc(this.Node__v) && - acc(this.Node__next) && - acc(validOption(this.Node__next)) -} - - -function length(this: Ref): Int - requires acc(validNode(this), write) - ensures result >= 1 -{ - (unfolding acc(validNode(this), write) in - unfolding acc(validOption(this.Node__next)) in - (variantOfOptionNode(this.Node__next) == Option__Node__None()) ? - 1 : 1 + length(this.Node__next.Option__Node__Some__1) - ) -} - -function itemAt(this: Ref, i: Int): Int - requires acc(validNode(this), write) - requires 0 <= i && i < length(this) -{ - unfolding acc(validNode(this), write) in unfolding acc(validOption(this.Node__next)) in ( - (i == 0) ? - this.Node__v: - (variantOfOptionNode(this.Node__next) == Option__Node__Some()) ? - itemAt(this.Node__next.Option__Node__Some__1, i-1) : this.Node__v - ) -} - -function sum(this$1: Ref): Int - requires acc(validNode(this$1), write) -{ - (unfolding acc(validNode(this$1), write) in unfolding acc(validOption(this$1.Node__next)) in - (variantOfOptionNode(this$1.Node__next) == Option__Node__None()) ? this$1.Node__v : this$1.Node__v + sum(this$1.Node__next.Option__Node__Some__1)) -} - -method append(this: Ref, val: Int) - requires acc(validNode(this), write) - ensures acc(validNode(this), write) /* POST1 */ - ensures length(this) == (old(length(this)) + 1) /* POST2 */ - ensures (forall i: Int :: (0 <= i && i < old(length(this))) ==> (itemAt(this, i) == old(itemAt(this, i)))) /* POST3 */ - ensures itemAt(this, length(this) - 1) == val /* POST4 */ - ensures true ==> true -{ - var tmp_node: Ref - var tmp_option: Ref - - unfold acc(validNode(this), write) - unfold acc(validOption(this.Node__next), write) - - if (variantOfOptionNode(this.Node__next) == Option__Node__None()) { - tmp_node := new(Node__next, Node__v) - tmp_node.Node__next := null - tmp_node.Node__v := val - - assume variantOfOptionNode(tmp_node.Node__next) == Option__Node__None() - fold acc(validOption(tmp_node.Node__next)) - fold acc(validNode(tmp_node), write) - - tmp_option := new(Option__Node__Some__1) - tmp_option.Option__Node__Some__1 := tmp_node - assume variantOfOptionNode(tmp_option) == Option__Node__Some() - fold acc(validOption(tmp_option)) - - this.Node__next := tmp_option - - - unfold validOption(tmp_option) - assert length(tmp_node) == 1 /* TODO: Required by Silicon, POST2 fails otherwise */ - assert itemAt(tmp_node, 0) == val /* TODO: Required by Silicon, POST4 fails otherwise */ - fold validOption(tmp_option) - } else { - append(this.Node__next.Option__Node__Some__1, val) - fold acc(validOption(this.Node__next), write) - } - - fold acc(validNode(this), write) -} - -method prepend(tail: Ref, val: Int) returns (res: Ref) - requires acc(validNode(tail)) - ensures acc(validNode(res)) - //ensures acc(validNode(tail)) - ensures length(res) == old(length(tail)) + 1 - - ensures (forall i: Int :: (1 <= i && i < length(res)) ==> (itemAt(res, i) == old(itemAt(tail, i-1)))) /* POST3 */ - ensures itemAt(res, 0) == val -{ - var tmp_option: Ref - - res := new(Node__v, Node__next) - res.Node__v := val - - tmp_option := new(Option__Node__Some__1) - tmp_option.Option__Node__Some__1 := tail - assume variantOfOptionNode(tmp_option) == Option__Node__Some() - - res.Node__next := tmp_option - - assert acc(validNode(tail)) - fold acc(validOption(res.Node__next)) - fold acc(validNode(res)) -} - -method length_iter(list: Ref) returns (len: Int) - requires acc(validNode(list), write) - ensures old(length(list)) == len - // TODO we have to preserve this property - // ensures acc(validNode(list)) -{ - var curr: Ref := list - var tmp: Ref := list - - len := 1 - - unfold acc(validNode(curr)) - unfold acc(validOption(curr.Node__next)) - while(variantOfOptionNode(curr.Node__next) == Option__Node__Some()) - invariant acc(curr.Node__v) - invariant acc(curr.Node__next) - invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> ( - acc(curr.Node__next.Option__Node__Some__1, write) && - acc(validNode(curr.Node__next.Option__Node__Some__1)) - )) - invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> len + length(curr.Node__next.Option__Node__Some__1) == old(length(list))) - invariant (variantOfOptionNode(curr.Node__next) == Option__Node__None() ==> len == old(length(list))) - { - assert acc(validNode(curr.Node__next.Option__Node__Some__1)) - len := len + 1 - tmp := curr - curr := curr.Node__next.Option__Node__Some__1 - unfold acc(validNode(curr)) - unfold acc(validOption(curr.Node__next)) - } -} - -method t1() -{ - var l: Ref - - l := new(Node__v, Node__next) - l.Node__next := null - l.Node__v := 1 - assume variantOfOptionNode(l.Node__next) == Option__Node__None() - - fold validOption(l.Node__next) - fold validNode(l) - - assert length(l) == 1 - assert itemAt(l, 0) == 1 - - append(l, 7) - assert itemAt(l, 1) == 7 - assert itemAt(l, 0) == 1 - assert length(l) == 2 - - l := prepend(l, 10) - assert itemAt(l, 2) == 7 - assert itemAt(l, 1) == 1 - assert itemAt(l, 0) == 10 - assert length(l) == 3 - - //assert sum(l) == 18 -} - -method t2(l: Ref) returns (res: Ref) - requires acc(validNode(l), write) - ensures acc(validNode(res), write) - ensures length(res) > old(length(l)) -{ - res := prepend(l, 10) -} |