summaryrefslogtreecommitdiff
path: root/tests/lexers/silver
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lexers/silver')
-rw-r--r--tests/lexers/silver/example.txt2606
1 files changed, 2606 insertions, 0 deletions
diff --git a/tests/lexers/silver/example.txt b/tests/lexers/silver/example.txt
new file mode 100644
index 00000000..e44d4a38
--- /dev/null
+++ b/tests/lexers/silver/example.txt
@@ -0,0 +1,2606 @@
+---input---
+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)
+}
+
+---tokens---
+'domain' Keyword
+' ' Text
+'Option__Node' Name
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'unique' Keyword
+' ' Text
+'function' Keyword
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+':' Operator
+' ' Text
+'Option__Node' Name
+'\n' Text
+
+' ' Text
+'unique' Keyword
+' ' Text
+'function' Keyword
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+':' Operator
+' ' Text
+'Option__Node' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'function' Keyword
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'self' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+':' Operator
+' ' Text
+'Option__Node' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'function' Keyword
+' ' Text
+'isOptionNode' Name
+'(' Punctuation
+'self' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+':' Operator
+' ' Text
+'Bool' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'axiom' Keyword
+' ' Text
+'ax_variantOfOptionNodeChoices' Name
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'forall' Keyword
+' ' Text
+'x' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+' ' Text
+':' Operator
+':' Operator
+' ' Text
+'{ variantOfOptionNode(x) }' Generic.Emph
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'x' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'|' Operator
+'|' Operator
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'x' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'axiom' Keyword
+' ' Text
+'ax_isCounterState' Name
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'forall' Keyword
+' ' Text
+'x' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+' ' Text
+':' Operator
+':' Operator
+' ' Text
+'{ variantOfOptionNode(x) }' Generic.Emph
+'\n' Text
+
+' ' Text
+'isOptionNode' Name
+'(' Punctuation
+'x' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'x' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'|' Operator
+'|' Operator
+'\n' Text
+
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'x' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'}' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'predicate' Keyword
+' ' Text
+'validOption' Name
+'(' Punctuation
+'this' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'isOptionNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+' ' Text
+'&' Operator
+'&' Operator
+'\n' Text
+
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'(' Punctuation
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'&' Operator
+'&' Operator
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'field' Keyword
+' ' Text
+'Option__Node__Some__1' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+'field' Keyword
+' ' Text
+'Node__v' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+'\n' Text
+
+'field' Keyword
+' ' Text
+'Node__next' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+'predicate' Keyword
+' ' Text
+'validNode' Name
+'(' Punctuation
+'this' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__v' Name
+')' Punctuation
+' ' Text
+'&' Operator
+'&' Operator
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'&' Operator
+'&' Operator
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'\n' Text
+
+'function' Keyword
+' ' Text
+'length' Name
+'(' Punctuation
+'this' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+':' Operator
+' ' Text
+'Int' Keyword.Type
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'result' Keyword
+' ' Text
+'>' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'in' Keyword
+'\n' Text
+
+' ' Text
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'in' Keyword
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'?' Operator
+' \n ' Text
+'1' Literal.Number.Integer
+' ' Text
+':' Operator
+' ' Text
+'1' Literal.Number.Integer
+' ' Text
+'+' Operator
+' ' Text
+'length' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'function' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'this' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+',' Punctuation
+' ' Text
+'i' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+')' Punctuation
+':' Operator
+' ' Text
+'Int' Keyword.Type
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'0' Literal.Number.Integer
+' ' Text
+'<' Operator
+'=' Operator
+' ' Text
+'i' Name
+' ' Text
+'&' Operator
+'&' Operator
+' ' Text
+'i' Name
+' ' Text
+'<' Operator
+' ' Text
+'length' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'in' Keyword
+' ' Text
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'in' Keyword
+' ' Text
+'(' Punctuation
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'i' Name
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'?' Operator
+'\n' Text
+
+' ' Text
+'this' Name
+'.' Punctuation
+'Node__v' Name
+':' Operator
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'?' Operator
+' \n ' Text
+'itemAt' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+',' Punctuation
+' ' Text
+'i' Name
+'-' Operator
+'1' Literal.Number.Integer
+')' Punctuation
+' ' Text
+':' Operator
+' ' Text
+'this' Name
+'.' Punctuation
+'Node__v' Name
+'\n' Text
+
+' ' Text
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'function' Keyword
+' ' Text
+'sum' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+':' Operator
+' ' Text
+'Int' Keyword.Type
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'(' Punctuation
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'in' Keyword
+' ' Text
+'unfolding' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'in' Keyword
+' \n ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'?' Operator
+' ' Text
+'this' Name
+'$1' Name
+'.' Punctuation
+'Node__v' Name
+' ' Text
+':' Operator
+' ' Text
+'this' Name
+'$1' Name
+'.' Punctuation
+'Node__v' Name
+' ' Text
+'+' Operator
+' ' Text
+'sum' Name
+'(' Punctuation
+'this' Name
+'$1' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'method' Keyword
+' ' Text
+'append' Name
+'(' Punctuation
+'this' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+',' Punctuation
+' ' Text
+'val' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+')' Punctuation
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'/*' Comment.Multiline
+' POST1 ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'length' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'(' Punctuation
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'+' Operator
+' ' Text
+'1' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'/*' Comment.Multiline
+' POST2 ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'(' Punctuation
+'forall' Keyword
+' ' Text
+'i' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+' ' Text
+':' Operator
+':' Operator
+' ' Text
+'(' Punctuation
+'0' Literal.Number.Integer
+' ' Text
+'<' Operator
+'=' Operator
+' ' Text
+'i' Name
+' ' Text
+'&' Operator
+'&' Operator
+' ' Text
+'i' Name
+' ' Text
+'<' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'(' Punctuation
+'itemAt' Name
+'(' Punctuation
+'this' Name
+',' Punctuation
+' ' Text
+'i' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'itemAt' Name
+'(' Punctuation
+'this' Name
+',' Punctuation
+' ' Text
+'i' Name
+')' Punctuation
+')' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'/*' Comment.Multiline
+' POST3 ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'this' Name
+',' Punctuation
+' ' Text
+'length' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+' ' Text
+'-' Operator
+' ' Text
+'1' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'val' Name
+' ' Text
+'/*' Comment.Multiline
+' POST4 ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'true' Keyword
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'true' Keyword
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'tmp_node' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'tmp_option' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'if' Keyword
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'tmp_node' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'new' Keyword
+'(' Punctuation
+'Node__next' Name
+',' Punctuation
+' ' Text
+'Node__v' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'tmp_node' Name
+'.' Punctuation
+'Node__next' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'null' Keyword
+'\n' Text
+
+' ' Text
+'tmp_node' Name
+'.' Punctuation
+'Node__v' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'val' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'assume' Keyword
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'tmp_node' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'tmp_node' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'tmp_node' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'tmp_option' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'new' Keyword
+'(' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'tmp_option' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'tmp_node' Name
+'\n' Text
+
+' ' Text
+'assume' Keyword
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'tmp_option' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'tmp_option' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'this' Name
+'.' Punctuation
+'Node__next' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'tmp_option' Name
+'\n' Text
+
+'\n' Text
+
+' \n ' Text
+'unfold' Keyword
+' ' Text
+'validOption' Name
+'(' Punctuation
+'tmp_option' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'length' Name
+'(' Punctuation
+'tmp_node' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+' ' Text
+'/*' Comment.Multiline
+' TODO: Required by Silicon, POST2 fails otherwise ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'tmp_node' Name
+',' Punctuation
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'val' Name
+' ' Text
+'/*' Comment.Multiline
+' TODO: Required by Silicon, POST4 fails otherwise ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'validOption' Name
+'(' Punctuation
+'tmp_option' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'}' Punctuation
+' ' Text
+'else' Keyword
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'append' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+',' Punctuation
+' ' Text
+'val' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'this' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'this' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'method' Keyword
+' ' Text
+'prepend' Name
+'(' Punctuation
+'tail' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+',' Punctuation
+' ' Text
+'val' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+')' Punctuation
+' ' Text
+'returns' Keyword
+' ' Text
+'(' Punctuation
+'res' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'tail' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'//ensures acc(validNode(tail))\n' Comment.Single
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'length' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'tail' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'+' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'(' Punctuation
+'forall' Keyword
+' ' Text
+'i' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+' ' Text
+':' Operator
+':' Operator
+' ' Text
+'(' Punctuation
+'1' Literal.Number.Integer
+' ' Text
+'<' Operator
+'=' Operator
+' ' Text
+'i' Name
+' ' Text
+'&' Operator
+'&' Operator
+' ' Text
+'i' Name
+' ' Text
+'<' Operator
+' ' Text
+'length' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'(' Punctuation
+'itemAt' Name
+'(' Punctuation
+'res' Name
+',' Punctuation
+' ' Text
+'i' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'itemAt' Name
+'(' Punctuation
+'tail' Name
+',' Punctuation
+' ' Text
+'i' Name
+'-' Operator
+'1' Literal.Number.Integer
+')' Punctuation
+')' Punctuation
+')' Punctuation
+')' Punctuation
+' ' Text
+'/*' Comment.Multiline
+' POST3 ' Comment.Multiline
+'*/' Comment.Multiline
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'res' Name
+',' Punctuation
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'val' Name
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'tmp_option' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'res' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'new' Keyword
+'(' Punctuation
+'Node__v' Name
+',' Punctuation
+' ' Text
+'Node__next' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'res' Name
+'.' Punctuation
+'Node__v' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'val' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'tmp_option' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'new' Keyword
+'(' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'tmp_option' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'tail' Name
+'\n' Text
+
+' ' Text
+'assume' Keyword
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'tmp_option' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'res' Name
+'.' Punctuation
+'Node__next' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'tmp_option' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'tail' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'res' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'method' Keyword
+' ' Text
+'length_iter' Name
+'(' Punctuation
+'list' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+' ' Text
+'returns' Keyword
+' ' Text
+'(' Punctuation
+'len' Name
+':' Operator
+' ' Text
+'Int' Keyword.Type
+')' Punctuation
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'list' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'list' Name
+')' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'len' Name
+'\n' Text
+
+' ' Text
+'// TODO we have to preserve this property\n' Comment.Single
+
+' ' Text
+'// ensures acc(validNode(list))\n' Comment.Single
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'curr' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'list' Name
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'tmp' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'list' Name
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'len' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'curr' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'while' Keyword
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'invariant' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__v' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'invariant' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'invariant' Name.Decorator
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'(' Punctuation
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+' ' Text
+'&' Operator
+'&' Operator
+'\n' Text
+
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'invariant' Name.Decorator
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__Some' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'len' Name
+' ' Text
+'+' Operator
+' ' Text
+'length' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'list' Name
+')' Punctuation
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'invariant' Name.Decorator
+' ' Text
+'(' Punctuation
+'variantOfOptionNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+'>' Operator
+' ' Text
+'len' Name
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'list' Name
+')' Punctuation
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'len' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'len' Name
+' ' Text
+'+' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'tmp' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'curr' Name
+'\n' Text
+
+' ' Text
+'curr' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+'.' Punctuation
+'Option__Node__Some__1' Name
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'curr' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'unfold' Keyword
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validOption' Name
+'(' Punctuation
+'curr' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+' ' Text
+'}' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'method' Keyword
+' ' Text
+'t1' Name
+'(' Punctuation
+')' Punctuation
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'var' Keyword
+' ' Text
+'l' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'l' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'new' Keyword
+'(' Punctuation
+'Node__v' Name
+',' Punctuation
+' ' Text
+'Node__next' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'l' Name
+'.' Punctuation
+'Node__next' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'null' Keyword
+'\n' Text
+
+' ' Text
+'l' Name
+'.' Punctuation
+'Node__v' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assume' Keyword
+' ' Text
+'variantOfOptionNode' Name
+'(' Punctuation
+'l' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'Option__Node__None' Name
+'(' Punctuation
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'validOption' Name
+'(' Punctuation
+'l' Name
+'.' Punctuation
+'Node__next' Name
+')' Punctuation
+'\n' Text
+
+' ' Text
+'fold' Keyword
+' ' Text
+'validNode' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'length' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'append' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'7' Literal.Number.Integer
+')' Punctuation
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'1' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'7' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'length' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'2' Literal.Number.Integer
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'l' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'prepend' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'10' Literal.Number.Integer
+')' Punctuation
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'2' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'7' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'1' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'1' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'itemAt' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'0' Literal.Number.Integer
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'10' Literal.Number.Integer
+'\n' Text
+
+' ' Text
+'assert' Keyword
+' ' Text
+'length' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+' ' Text
+'=' Operator
+'=' Operator
+' ' Text
+'3' Literal.Number.Integer
+'\n' Text
+
+'\n' Text
+
+' ' Text
+'//assert sum(l) == 18\n' Comment.Single
+
+'}' Punctuation
+'\n' Text
+
+'\n' Text
+
+'method' Keyword
+' ' Text
+'t2' Name
+'(' Punctuation
+'l' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+' ' Text
+'returns' Keyword
+' ' Text
+'(' Punctuation
+'res' Name
+':' Operator
+' ' Text
+'Ref' Keyword.Type
+')' Punctuation
+'\n' Text
+
+' ' Text
+'requires' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'acc' Keyword
+'(' Punctuation
+'validNode' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+',' Punctuation
+' ' Text
+'write' Keyword
+')' Punctuation
+'\n' Text
+
+' ' Text
+'ensures' Name.Decorator
+' ' Text
+'length' Name
+'(' Punctuation
+'res' Name
+')' Punctuation
+' ' Text
+'>' Operator
+' ' Text
+'old' Keyword
+'(' Punctuation
+'length' Name
+'(' Punctuation
+'l' Name
+')' Punctuation
+')' Punctuation
+'\n' Text
+
+'{' Punctuation
+'\n' Text
+
+' ' Text
+'res' Name
+' ' Text
+':' Operator
+'=' Operator
+' ' Text
+'prepend' Name
+'(' Punctuation
+'l' Name
+',' Punctuation
+' ' Text
+'10' Literal.Number.Integer
+')' Punctuation
+'\n' Text
+
+'}' Punctuation
+'\n' Text
View Lorry Controller Status