1domain Option__Node {
2    unique function Option__Node__Some(): Option__Node
3    unique function Option__Node__None(): Option__Node
4
5    function variantOfOptionNode(self: Ref): Option__Node
6
7    function isOptionNode(self: Ref): Bool
8
9    axiom ax_variantOfOptionNodeChoices {
10        forall x: Ref :: { variantOfOptionNode(x) }
11            (variantOfOptionNode(x) == Option__Node__Some() || variantOfOptionNode(x) == Option__Node__None())
12    }
13
14    axiom ax_isCounterState {
15        forall x: Ref ::  { variantOfOptionNode(x) }
16            isOptionNode(x) == (variantOfOptionNode(x) == Option__Node__Some() ||
17                variantOfOptionNode(x) == Option__Node__None())
18    }
19}
20
21predicate validOption(this: Ref) {
22    isOptionNode(this) &&
23    variantOfOptionNode(this) == Option__Node__Some() ==> (
24        acc(this.Option__Node__Some__1, write) &&
25        acc(validNode(this.Option__Node__Some__1))
26    )
27}
28
29field Option__Node__Some__1: Ref
30
31field Node__v: Int
32field Node__next: Ref
33
34predicate validNode(this: Ref) {
35    acc(this.Node__v) &&
36    acc(this.Node__next) &&
37    acc(validOption(this.Node__next))
38}
39
40
41function length(this: Ref): Int
42    requires acc(validNode(this), write)
43    ensures result >= 1
44{
45    (unfolding acc(validNode(this), write) in
46        unfolding acc(validOption(this.Node__next)) in
47        (variantOfOptionNode(this.Node__next) == Option__Node__None()) ?
48            1 : 1 + length(this.Node__next.Option__Node__Some__1)
49    )
50}
51
52function itemAt(this: Ref, i: Int): Int
53    requires acc(validNode(this), write)
54    requires 0 <= i && i < length(this)
55{
56    unfolding acc(validNode(this), write) in unfolding acc(validOption(this.Node__next)) in (
57        (i == 0) ?
58            this.Node__v:
59            (variantOfOptionNode(this.Node__next) == Option__Node__Some()) ?
60                itemAt(this.Node__next.Option__Node__Some__1, i-1) : this.Node__v
61    )
62}
63
64function sum(this$1: Ref): Int
65    requires acc(validNode(this$1), write)
66{
67    (unfolding acc(validNode(this$1), write) in unfolding acc(validOption(this$1.Node__next)) in
68        (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))
69}
70
71method append(this: Ref, val: Int)
72    requires acc(validNode(this), write)
73    ensures acc(validNode(this), write) /* POST1 */
74    ensures length(this) == (old(length(this)) + 1) /* POST2 */
75    ensures (forall i: Int :: (0 <= i && i < old(length(this))) ==> (itemAt(this, i) == old(itemAt(this, i)))) /* POST3 */
76    ensures itemAt(this, length(this) - 1) == val /* POST4 */
77    ensures true ==> true
78{
79    var tmp_node: Ref
80    var tmp_option: Ref
81
82    unfold acc(validNode(this), write)
83    unfold acc(validOption(this.Node__next), write)
84
85    if (variantOfOptionNode(this.Node__next) == Option__Node__None()) {
86        tmp_node := new(Node__next, Node__v)
87        tmp_node.Node__next := null
88        tmp_node.Node__v := val
89
90        assume variantOfOptionNode(tmp_node.Node__next) == Option__Node__None()
91        fold acc(validOption(tmp_node.Node__next))
92        fold acc(validNode(tmp_node), write)
93
94        tmp_option := new(Option__Node__Some__1)
95        tmp_option.Option__Node__Some__1 := tmp_node
96        assume variantOfOptionNode(tmp_option) == Option__Node__Some()
97        fold acc(validOption(tmp_option))
98
99        this.Node__next := tmp_option
100
101
102        unfold validOption(tmp_option)
103        assert length(tmp_node) == 1 /* TODO: Required by Silicon, POST2 fails otherwise */
104        assert itemAt(tmp_node, 0) == val /* TODO: Required by Silicon, POST4 fails otherwise */
105        fold validOption(tmp_option)
106    } else {
107        append(this.Node__next.Option__Node__Some__1, val)
108        fold acc(validOption(this.Node__next), write)
109    }
110
111    fold acc(validNode(this), write)
112}
113
114method prepend(tail: Ref, val: Int) returns (res: Ref)
115    requires acc(validNode(tail))
116    ensures acc(validNode(res))
117    //ensures acc(validNode(tail))
118    ensures length(res) == old(length(tail)) + 1
119
120    ensures (forall i: Int :: (1 <= i && i < length(res)) ==> (itemAt(res, i) == old(itemAt(tail, i-1)))) /* POST3 */
121    ensures itemAt(res, 0) == val
122{
123    var tmp_option: Ref
124
125    res := new(Node__v, Node__next)
126    res.Node__v := val
127
128    tmp_option := new(Option__Node__Some__1)
129    tmp_option.Option__Node__Some__1 := tail
130    assume variantOfOptionNode(tmp_option) == Option__Node__Some()
131
132    res.Node__next := tmp_option
133
134    assert acc(validNode(tail))
135    fold acc(validOption(res.Node__next))
136    fold acc(validNode(res))
137}
138
139method length_iter(list: Ref) returns (len: Int)
140    requires acc(validNode(list), write)
141    ensures old(length(list)) == len
142    // TODO we have to preserve this property
143    // ensures acc(validNode(list))
144{
145    var curr: Ref := list
146    var tmp: Ref := list
147
148    len := 1
149
150    unfold acc(validNode(curr))
151    unfold acc(validOption(curr.Node__next))
152    while(variantOfOptionNode(curr.Node__next) == Option__Node__Some())
153        invariant acc(curr.Node__v)
154        invariant acc(curr.Node__next)
155        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> (
156            acc(curr.Node__next.Option__Node__Some__1, write) &&
157            acc(validNode(curr.Node__next.Option__Node__Some__1))
158        ))
159        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> len + length(curr.Node__next.Option__Node__Some__1) == old(length(list)))
160        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__None() ==> len == old(length(list)))
161    {
162        assert acc(validNode(curr.Node__next.Option__Node__Some__1))
163        len := len + 1
164        tmp := curr
165        curr := curr.Node__next.Option__Node__Some__1
166        unfold acc(validNode(curr))
167        unfold acc(validOption(curr.Node__next))
168    }
169}
170
171method t1()
172{
173    var l: Ref
174
175    l := new(Node__v, Node__next)
176    l.Node__next := null
177    l.Node__v := 1
178    assume variantOfOptionNode(l.Node__next) == Option__Node__None()
179
180    fold validOption(l.Node__next)
181    fold validNode(l)
182
183    assert length(l) == 1
184    assert itemAt(l, 0) == 1
185
186    append(l, 7)
187    assert itemAt(l, 1) == 7
188    assert itemAt(l, 0) == 1
189    assert length(l) == 2
190
191    l := prepend(l, 10)
192    assert itemAt(l, 2) == 7
193    assert itemAt(l, 1) == 1
194    assert itemAt(l, 0) == 10
195    assert length(l) == 3
196
197    //assert sum(l) == 18
198}
199
200method t2(l: Ref) returns (res: Ref)
201    requires acc(validNode(l), write)
202    ensures acc(validNode(res), write)
203    ensures length(res) > old(length(l))
204{
205    res := prepend(l, 10)
206}
207