Merged in fhahn/pygments-main (pull request #420)

Add lexer for Boogie

3 files changed, 189 insertions, 3 deletions

diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py
index 2d14432d..fcab216b 100644
--- a/pygments/lexers/_mapping.py
+++ b/pygments/lexers/_mapping.py
@@ -51,6 +51,7 @@ LEXERS = {
     'BlitzBasicLexer': ('pygments.lexers.basic', 'BlitzBasic', ('blitzbasic', 'b3d', 'bplus'), ('*.bb', '*.decls'), ('text/x-bb',)),
     'BlitzMaxLexer': ('pygments.lexers.basic', 'BlitzMax', ('blitzmax', 'bmax'), ('*.bmx',), ('text/x-bmx',)),
     'BooLexer': ('pygments.lexers.dotnet', 'Boo', ('boo',), ('*.boo',), ('text/x-boo',)),
+    'BoogieLexer': ('pygments.lexers.esoteric', 'Boogie', ('boogie',), ('*.bpl',), ()),
     'BrainfuckLexer': ('pygments.lexers.esoteric', 'Brainfuck', ('brainfuck', 'bf'), ('*.bf', '*.b'), ('application/x-brainfuck',)),
     'BroLexer': ('pygments.lexers.dsls', 'Bro', ('bro',), ('*.bro',), ()),
     'BugsLexer': ('pygments.lexers.modeling', 'BUGS', ('bugs', 'winbugs', 'openbugs'), ('*.bug',), ()),
diff --git a/pygments/lexers/esoteric.py b/pygments/lexers/esoteric.py
index f61b292d..1f317260 100644
--- a/pygments/lexers/esoteric.py
+++ b/pygments/lexers/esoteric.py
@@ -9,11 +9,11 @@
     :license: BSD, see LICENSE for details.
 """
 
-from pygments.lexer import RegexLexer, include
+from pygments.lexer import RegexLexer, include, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
-    Number, Punctuation, Error
+    Number, Punctuation, Error, Whitespace
 
-__all__ = ['BrainfuckLexer', 'BefungeLexer', 'RedcodeLexer']
+__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer']
 
 
 class BrainfuckLexer(RegexLexer):
@@ -112,3 +112,48 @@ class RedcodeLexer(RegexLexer):
             (r'[-+]?\d+', Number.Integer),
         ],
     }
+
+
+class BoogieLexer(RegexLexer):
+    """
+    For `Boogie <https://boogie.codeplex.com/>`_ source code.
+
+    .. versionadded:: 2.0
+    """
+    name = 'Boogie'
+    aliases = ['boogie']
+    filenames = ['*.bpl']
+
+    tokens = {
+        'root': [
+            # Whitespace and Comments
+            (r'\n', Whitespace),
+            (r'\s+', Whitespace),
+            (r'//[/!](.*?)\n', Comment.Doc),
+            (r'//(.*?)\n', Comment.Single),
+            (r'/\*', Comment.Multiline, 'comment'),
+
+            (words((
+                'axiom', 'break', 'call', 'ensures', 'else', 'exists', 'function',
+                'forall', 'if', 'invariant', 'modifies', 'procedure',  'requires',
+                'then', 'var', 'while'),
+             suffix=r'\b'), Keyword),
+            (words(('const',), suffix=r'\b'), Keyword.Reserved),
+
+            (words(('bool', 'int', 'ref'), suffix=r'\b'), Keyword.Type),
+            include('numbers'),
+            (r"(>=|<=|:=|!=|==>|&&|\|\||[+/\-=>*<\[\]])", Operator),
+            (r"([{}():;,.])", Punctuation),
+            # Identifier
+            (r'[a-zA-Z_]\w*', Name),
+        ],
+        'comment': [
+            (r'[^*/]+', Comment.Multiline),
+            (r'/\*', Comment.Multiline, '#push'),
+            (r'\*/', Comment.Multiline, '#pop'),
+            (r'[*/]', Comment.Multiline),
+        ],
+        'numbers': [
+            (r'[0-9]+', Number.Integer),
+        ],
+    }
diff --git a/tests/examplefiles/test.bpl b/tests/examplefiles/test.bpl
new file mode 100644
index 00000000..add25e1a
--- /dev/null
+++ b/tests/examplefiles/test.bpl
@@ -0,0 +1,140 @@
+/*
+ * Test Boogie rendering
+*/
+
+const N: int;
+axiom 0 <= N;
+
+procedure foo() {
+    break;
+}
+// array to sort as global array, because partition & quicksort have to 
+var a: [int] int;
+var original: [int] int;
+var perm: [int] int;
+
+// Is array a of length N sorted?
+function is_sorted(a: [int] int, l: int, r: int): bool
+{
+    (forall j, k: int :: l <= j && j < k && k <= r ==> a[j] <= a[k])
+}
+
+// is range a[l:r] unchanged?
+function is_unchanged(a: [int] int, b: [int] int, l: int, r: int): bool {
+    (forall i: int :: l <= i && i <= r ==> a[i] == b[i]) 
+}
+
+function is_permutation(a: [int] int, original: [int] int, perm: [int] int, N: int): bool
+{
+    (forall k: int :: 0 <= k && k < N ==> 0 <= perm[k] && perm[k] < N) &&
+    (forall k, j: int :: 0 <= k && k < j && j < N ==> perm[k] != perm[j]) &&
+    (forall k: int :: 0 <= k && k < N ==> a[k] == original[perm[k]])
+}
+
+function count(a: [int] int, x: int, N: int) returns (int)
+{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
+
+
+/*
+function count(a: [int] int, x: int, N: int) returns (int)
+{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
+
+function is_permutation(a: [int] int, b: [int] int, l: int, r: int): bool {
+  (forall i: int :: l <= i && i <= r ==> count(a, a[i], r+1) == count(b, a[i], r+1))
+}
+*/
+
+procedure partition(l: int, r: int, N: int) returns (p: int)
+    modifies a, perm;
+    requires N > 0;
+    requires l >= 0 && l < r && r < N;
+    requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
+    requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
+
+    /* a is a permutation of the original array original */
+    requires is_permutation(a, original, perm, N);
+
+    ensures (forall k: int :: (k >= l &&  k <= p ) ==> a[k] <= a[p]);
+    ensures (forall k: int :: (k > p &&  k <= r ) ==> a[k] > a[p]);
+    ensures p >= l && p <= r;
+    ensures is_unchanged(a, old(a), 0, l-1);
+    ensures is_unchanged(a, old(a), r+1, N);
+    ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
+    ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
+
+    /* a is a permutation of the original array original */
+    ensures is_permutation(a, original, perm, N);
+{
+    var i: int;
+    var sv: int;
+    var pivot: int;
+    var tmp: int;
+
+    i := l;
+    sv := l;
+    pivot := a[r];
+
+    while (i < r)
+        invariant i <= r && i >= l;
+        invariant sv <= i && sv >= l;
+        invariant pivot == a[r];
+        invariant (forall k: int :: (k >= l &&  k < sv) ==> a[k] <= old(a[r]));
+        invariant (forall k: int :: (k >= sv &&  k < i) ==> a[k] > old(a[r]));
+
+        /* a is a permutation of the original array original */
+        invariant is_permutation(a, original, perm, N);
+
+        invariant is_unchanged(a, old(a), 0, l-1);
+        invariant is_unchanged(a, old(a), r+1, N);
+        invariant ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
+        invariant ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
+    {
+        if ( a[i] <= pivot) {
+            tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
+            tmp := perm[i];  perm[i] := perm[sv];  perm[sv] := tmp;
+            sv := sv +1;
+        }
+        i := i + 1;
+    }
+
+    //swap
+    tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
+    tmp := perm[i];  perm[i] := perm[sv];  perm[sv] := tmp;
+
+    p := sv;
+}
+
+
+procedure quicksort(l: int, r: int, N: int)
+    modifies a, perm;
+
+    requires N > 0;
+    requires l >= 0 && l < r && r < N;
+    requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
+    requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
+
+    /* a is a permutation of the original array original */
+    requires is_permutation(a, original, perm, N);
+
+    ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
+    ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
+
+    ensures is_unchanged(a, old(a), 0, l-1);
+    ensures is_unchanged(a, old(a), r+1, N);
+    ensures is_sorted(a, l, r);
+
+    /* a is a permutation of the original array original */
+    ensures is_permutation(a, original, perm, N);
+{
+    var p: int;
+
+    call p := partition(l, r, N);
+
+    if ((p-1) > l) {
+        call quicksort(l, p-1, N);
+    }
+
+    if ((p+1) < r) {
+        call quicksort(p+1, r, N);
+    }
+}