'/*'          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
