coffee/coffee.pygments
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
This repository has been archived on 2024-06-20. You can view files and clone it, but you cannot make any changes to it's state, such as pushing and creating new issues, pull requests or comments.
coffee.pygments/tests/examplefiles/boogie/test.bpl.output
Oleh Prypin 6f43092173
Also add auto-updatable output-based tests to examplefiles (#1689) 
Co-authored-by: Georg Brandl <georg@python.org>
2021-01-20 10:48:45 +01:00

2311 lines
47 KiB
Text
Generated
Raw Permalink Blame History

'/*' Comment.Multiline
'\n ' Comment.Multiline
'*' Comment.Multiline
' Test Boogie rendering\n' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
'\n' Text
'const' Keyword.Reserved
' ' Text
'N' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'axiom' Keyword
' ' Text
'0' Literal.Number.Integer
' ' Text
'<=' Operator
' ' Text
'N' Name
';' Punctuation
'\n' Text
'\n' Text
'procedure' Keyword
' ' Text
'foo' Name
'(' Punctuation
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'break' Keyword
';' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'// array to sort as global array, because partition & quicksort have to \n' Comment.Single
'var' Keyword
' ' Text
'a' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'var' Keyword
' ' Text
'original' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'var' Keyword
' ' Text
'perm' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'\n' Text
'// Is array a of length N sorted?\n' Comment.Single
'function' Keyword
' ' Text
'is_sorted' Name
'(' Punctuation
'a' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'l' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'r' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
':' Punctuation
' ' Text
'bool' Keyword.Type
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'j' Name
',' Punctuation
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'l' Name
' ' Text
'<=' Operator
' ' Text
'j' Name
' ' Text
'&&' Operator
' ' Text
'j' Name
' ' Text
'<' Operator
' ' Text
'k' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'j' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'// is range a[l:r] unchanged?\n' Comment.Single
'function' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'b' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'l' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'r' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
':' Punctuation
' ' Text
'bool' Keyword.Type
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'i' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'l' Name
' ' Text
'<=' Operator
' ' Text
'i' Name
' ' Text
'&&' Operator
' ' Text
'i' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'b' Name
'[' Operator
'i' Name
']' Operator
')' Punctuation
' \n' Text
'}' Punctuation
'\n' Text
'\n' Text
'function' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'original' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'perm' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'N' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
':' Punctuation
' ' Text
'bool' Keyword.Type
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'0' Literal.Number.Integer
' ' Text
'<=' Operator
' ' Text
'k' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<' Operator
' ' Text
'N' Name
' ' Text
'==>' Operator
' ' Text
'0' Literal.Number.Integer
' ' Text
'<=' Operator
' ' Text
'perm' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'&&' Operator
' ' Text
'perm' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'&&' Operator
'\n' Text
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
',' Punctuation
' ' Text
'j' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'0' Literal.Number.Integer
' ' Text
'<=' Operator
' ' Text
'k' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<' Operator
' ' Text
'j' Name
' ' Text
'&&' Operator
' ' Text
'j' Name
' ' Text
'<' Operator
' ' Text
'N' Name
' ' Text
'==>' Operator
' ' Text
'perm' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'!=' Operator
' ' Text
'perm' Name
'[' Operator
'j' Name
']' Operator
')' Punctuation
' ' Text
'&&' Operator
'\n' Text
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'0' Literal.Number.Integer
' ' Text
'<=' Operator
' ' Text
'k' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<' Operator
' ' Text
'N' Name
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'=' Operator
'=' Operator
' ' Text
'original' Name
'[' Operator
'perm' Name
'[' Operator
'k' Name
']' Operator
']' Operator
')' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'function' Keyword
' ' Text
'count' Name
'(' Punctuation
'a' Name
':' Punctuation
' ' Text
'[' Operator
'int' Keyword.Type
']' Operator
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'x' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'N' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
' ' Text
'returns' Name
' ' Text
'(' Punctuation
'int' Keyword.Type
')' Punctuation
'\n' Text
'{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }' Generic.Emph
'\n' Text
'\n' Text
'\n' Text
'/*' Comment.Multiline
'\nfunction count(a: [int] int, x: int, N: int) returns (int)\n{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }\n\nfunction is_permutation(a: [int] int, b: [int] int, l: int, r: int): bool {\n (forall i: int :: l <= i && i <= r ==> count(a, a[i], r+1) == count(b, a[i], r+1))\n}\n' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
'\n' Text
'procedure' Keyword
' ' Text
'partition' Name
'(' Punctuation
'l' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'r' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'N' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
' ' Text
'returns' Name
' ' Text
'(' Punctuation
'p' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'modifies' Keyword
' ' Text
'a' Name
',' Punctuation
' ' Text
'perm' Name
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'N' Name
' ' Text
'>' Operator
' ' Text
'0' Literal.Number.Integer
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'l' Name
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
' ' Text
'&&' Operator
' ' Text
'l' Name
' ' Text
'<' Operator
' ' Text
'r' Name
' ' Text
'&&' Operator
' ' Text
'r' Name
' ' Text
'<' Operator
' ' Text
'N' Name
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'r' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
'+' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'l' Name
'-' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'/*' Comment.Multiline
' a is a permutation of the original array original ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'original' Name
',' Punctuation
' ' Text
'perm' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'p' Name
' ' Text
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'p' Name
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>' Operator
' ' Text
'p' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
' ' Text
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'p' Name
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'p' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'p' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'0' Literal.Number.Integer
',' Punctuation
' ' Text
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'r' Name
'+' Operator
'1' Literal.Number.Integer
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'r' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
'+' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'l' Name
'-' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'/*' Comment.Multiline
' a is a permutation of the original array original ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'original' Name
',' Punctuation
' ' Text
'perm' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'i' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'sv' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'pivot' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'tmp' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'i' Name
' ' Text
':=' Operator
' ' Text
'l' Name
';' Punctuation
'\n' Text
' ' Text
'sv' Name
' ' Text
':=' Operator
' ' Text
'l' Name
';' Punctuation
'\n' Text
' ' Text
'pivot' Name
' ' Text
':=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
']' Operator
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'while' Keyword
' ' Text
'(' Punctuation
'i' Name
' ' Text
'<' Operator
' ' Text
'r' Name
')' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'i' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
' ' Text
'&&' Operator
' ' Text
'i' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'sv' Name
' ' Text
'<=' Operator
' ' Text
'i' Name
' ' Text
'&&' Operator
' ' Text
'sv' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'pivot' Name
' ' Text
'=' Operator
'=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
']' Operator
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<' Operator
' ' Text
'sv' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'old' Name
'(' Punctuation
'a' Name
'[' Operator
'r' Name
']' Operator
')' Punctuation
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'sv' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<' Operator
' ' Text
'i' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'old' Name
'(' Punctuation
'a' Name
'[' Operator
'r' Name
']' Operator
')' Punctuation
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'/*' Comment.Multiline
' a is a permutation of the original array original ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'original' Name
',' Punctuation
' ' Text
'perm' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'0' Literal.Number.Integer
',' Punctuation
' ' Text
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'r' Name
'+' Operator
'1' Literal.Number.Integer
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'r' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
'+' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'invariant' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'l' Name
'-' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'if' Keyword
' ' Text
'(' Punctuation
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'pivot' Name
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'tmp' Name
' ' Text
':=' Operator
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
';' Punctuation
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'a' Name
'[' Operator
'sv' Name
']' Operator
';' Punctuation
' ' Text
'a' Name
'[' Operator
'sv' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'tmp' Name
';' Punctuation
'\n' Text
' ' Text
'tmp' Name
' ' Text
':=' Operator
' ' Text
'perm' Name
'[' Operator
'i' Name
']' Operator
';' Punctuation
' ' Text
'perm' Name
'[' Operator
'i' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'perm' Name
'[' Operator
'sv' Name
']' Operator
';' Punctuation
' ' Text
'perm' Name
'[' Operator
'sv' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'tmp' Name
';' Punctuation
'\n' Text
' ' Text
'sv' Name
' ' Text
':=' Operator
' ' Text
'sv' Name
' ' Text
'+' Operator
'1' Literal.Number.Integer
';' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
' ' Text
'i' Name
' ' Text
':=' Operator
' ' Text
'i' Name
' ' Text
'+' Operator
' ' Text
'1' Literal.Number.Integer
';' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'\n' Text
' ' Text
'//swap\n' Comment.Single
' ' Text
'tmp' Name
' ' Text
':=' Operator
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
';' Punctuation
' ' Text
'a' Name
'[' Operator
'i' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'a' Name
'[' Operator
'sv' Name
']' Operator
';' Punctuation
' ' Text
'a' Name
'[' Operator
'sv' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'tmp' Name
';' Punctuation
'\n' Text
' ' Text
'tmp' Name
' ' Text
':=' Operator
' ' Text
'perm' Name
'[' Operator
'i' Name
']' Operator
';' Punctuation
' ' Text
'perm' Name
'[' Operator
'i' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'perm' Name
'[' Operator
'sv' Name
']' Operator
';' Punctuation
' ' Text
'perm' Name
'[' Operator
'sv' Name
']' Operator
' ' Text
':=' Operator
' ' Text
'tmp' Name
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'p' Name
' ' Text
':=' Operator
' ' Text
'sv' Name
';' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
'\n' Text
'\n' Text
'procedure' Keyword
' ' Text
'quicksort' Name
'(' Punctuation
'l' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'r' Name
':' Punctuation
' ' Text
'int' Keyword.Type
',' Punctuation
' ' Text
'N' Name
':' Punctuation
' ' Text
'int' Keyword.Type
')' Punctuation
'\n' Text
' ' Text
'modifies' Keyword
' ' Text
'a' Name
',' Punctuation
' ' Text
'perm' Name
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'N' Name
' ' Text
'>' Operator
' ' Text
'0' Literal.Number.Integer
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'l' Name
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
' ' Text
'&&' Operator
' ' Text
'l' Name
' ' Text
'<' Operator
' ' Text
'r' Name
' ' Text
'&&' Operator
' ' Text
'r' Name
' ' Text
'<' Operator
' ' Text
'N' Name
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'r' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
'+' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'l' Name
'-' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'/*' Comment.Multiline
' a is a permutation of the original array original ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'requires' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'original' Name
',' Punctuation
' ' Text
'perm' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'r' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'N' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'<=' Operator
' ' Text
'a' Name
'[' Operator
'r' Name
'+' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>=' Operator
' ' Text
'0' Literal.Number.Integer
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'(' Punctuation
'forall' Keyword
' ' Text
'k' Name
':' Punctuation
' ' Text
'int' Keyword.Type
' ' Text
':' Punctuation
':' Punctuation
' ' Text
'(' Punctuation
'k' Name
' ' Text
'>=' Operator
' ' Text
'l' Name
' ' Text
'&&' Operator
' ' Text
'k' Name
' ' Text
'<=' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'==>' Operator
' ' Text
'a' Name
'[' Operator
'k' Name
']' Operator
' ' Text
'>' Operator
' ' Text
'a' Name
'[' Operator
'l' Name
'-' Operator
'1' Literal.Number.Integer
']' Operator
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'0' Literal.Number.Integer
',' Punctuation
' ' Text
'l' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_unchanged' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'old' Name
'(' Punctuation
'a' Name
')' Punctuation
',' Punctuation
' ' Text
'r' Name
'+' Operator
'1' Literal.Number.Integer
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_sorted' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'l' Name
',' Punctuation
' ' Text
'r' Name
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'/*' Comment.Multiline
' a is a permutation of the original array original ' Comment.Multiline
'*/' Comment.Multiline
'\n' Text
' ' Text
'ensures' Keyword
' ' Text
'is_permutation' Name
'(' Punctuation
'a' Name
',' Punctuation
' ' Text
'original' Name
',' Punctuation
' ' Text
'perm' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'{' Punctuation
'\n' Text
' ' Text
'var' Keyword
' ' Text
'p' Name
':' Punctuation
' ' Text
'int' Keyword.Type
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'call' Keyword
' ' Text
'p' Name
' ' Text
':=' Operator
' ' Text
'partition' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'r' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
'\n' Text
' ' Text
'if' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'p' Name
'-' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'>' Operator
' ' Text
'l' Name
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'call' Keyword
' ' Text
'quicksort' Name
'(' Punctuation
'l' Name
',' Punctuation
' ' Text
'p' Name
'-' Operator
'1' Literal.Number.Integer
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'\n' Text
' ' Text
'if' Keyword
' ' Text
'(' Punctuation
'(' Punctuation
'p' Name
'+' Operator
'1' Literal.Number.Integer
')' Punctuation
' ' Text
'<' Operator
' ' Text
'r' Name
')' Punctuation
' ' Text
'{' Punctuation
'\n' Text
' ' Text
'call' Keyword
' ' Text
'quicksort' Name
'(' Punctuation
'p' Name
'+' Operator
'1' Literal.Number.Integer
',' Punctuation
' ' Text
'r' Name
',' Punctuation
' ' Text
'N' Name
')' Punctuation
';' Punctuation
'\n' Text
' ' Text
'}' Punctuation
'\n' Text
'}' Punctuation
'\n' Text
Reference in a new issue View git blame Copy permalink