'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