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