From 791adc9910560834c8159f892fad1b8acf0965dd Mon Sep 17 00:00:00 2001 From: Nadia Polikarpova Date: Sun, 16 Sep 2012 14:25:58 +0200 Subject: Added the new keyword (calc) to Util --- Util/latex/dafny.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Util/latex') diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 81b04694..d60488d1 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ % expressions match,case,false,true,null,old,fresh,choose,this, % statements - assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where + assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where,calc }, literate=% {:}{$\colon$}1 -- cgit v1.2.3 From 623a87c132abec61b5c74a6a00a7b162073a6a8d Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:42 +0200 Subject: Boogie: new syntax for integer division and modulus: use div and mod instead of / and % --- Binaries/DafnyPrelude.bpl | 12 ++-- Source/Core/AbsyExpr.cs | 4 +- Source/Core/BoogiePL.atg | 4 +- Source/Core/Parser.cs | 4 +- Source/Core/Scanner.cs | 82 ++++++++++------------ Source/Core/Util.cs | 4 +- Test/livevars/bla1.bpl | 2 +- Test/livevars/daytona_bug2_ioctl_example_1.bpl | 2 +- Test/livevars/daytona_bug2_ioctl_example_2.bpl | 2 +- Test/livevars/stack_overflow.bpl | 2 +- Test/prover/EQ_v2.Eval__v4.Eval_out.bpl | 4 +- Test/test0/Answer | 8 ++- Test/test0/BadLabels1.bpl | 2 +- Test/test0/PrettyPrint.bpl | 7 +- Test/test2/strings-no-where.bpl | 20 +++--- Test/test2/strings-where.bpl | 20 +++--- Util/Emacs/boogie-mode.el | 2 +- .../VS2010/Boogie/BoogieLanguageService/Grammar.cs | 7 +- Util/latex/boogie.sty | 2 +- Util/vim/syntax/boogie.vim | 2 +- 20 files changed, 98 insertions(+), 94 deletions(-) (limited to 'Util/latex') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ca526173..53e8e86a 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -613,15 +613,15 @@ var $Tick: TickType; // -- Arithmetic ------------------------------------------------- // --------------------------------------------------------------- -// the connection between % and / -axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y); +// the connection between mod and div +axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y); // remainder is always Euclidean Modulus. -axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y); -axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y); +axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y); +axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y); -// the following axiom has some unfortunate matching, but it does state a property about % that +// the following axiom has some unfortunate matching, but it does state a property about mod that // is sometimes useful -axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); +axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); // --------------------------------------------------------------- diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f2ed5790..d2b8506a 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1214,9 +1214,9 @@ namespace Microsoft.Boogie { case Opcode.Mul: return "*"; case Opcode.Div: - return "/"; + return "div"; case Opcode.Mod: - return "%"; + return "mod"; case Opcode.Eq: return "=="; case Opcode.Neq: diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index a2ad40f6..26b70bd3 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1171,8 +1171,8 @@ Factor MulOp = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .) ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .) - | "/" (. x = t; op=BinaryOperator.Opcode.Div; .) - | "%" (. x = t; op=BinaryOperator.Opcode.Mod; .) + | "div" (. x = t; op=BinaryOperator.Opcode.Div; .) + | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .) ) . diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index e95bccda..8638d9c3 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -2157,8 +2157,8 @@ public class Errors { case 68: s = "\"++\" expected"; break; case 69: s = "\"+\" expected"; break; case 70: s = "\"-\" expected"; break; - case 71: s = "\"/\" expected"; break; - case 72: s = "\"%\" expected"; break; + case 71: s = "\"div\" expected"; break; + case 72: s = "\"mod\" expected"; break; case 73: s = "\"!\" expected"; break; case 74: s = "\"\\u00ac\" expected"; break; case 75: s = "\"false\" expected"; break; diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index cfef86c7..b9f4ec42 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -262,36 +262,34 @@ public class Scanner { start[59] = 12; start[40] = 13; start[41] = 14; - start[58] = 49; + start[58] = 47; start[44] = 15; start[91] = 16; start[93] = 17; - start[60] = 50; - start[62] = 51; + start[60] = 48; + start[62] = 49; start[123] = 18; - start[125] = 52; - start[61] = 53; + start[125] = 50; + start[61] = 51; start[42] = 19; start[8660] = 22; start[8658] = 24; start[8656] = 25; start[38] = 26; start[8743] = 28; - start[124] = 54; + start[124] = 52; start[8744] = 30; - start[33] = 55; + start[33] = 53; start[8800] = 34; start[8804] = 35; start[8805] = 36; - start[43] = 56; + start[43] = 54; start[45] = 38; - start[47] = 39; - start[37] = 40; - start[172] = 41; - start[8704] = 44; - start[8707] = 45; - start[955] = 46; - start[8226] = 48; + start[172] = 39; + start[8704] = 42; + start[8707] = 43; + start[955] = 44; + start[8226] = 46; start[Buffer.EOF] = -1; } @@ -519,6 +517,8 @@ public class Scanner { case "havoc": t.kind = 46; break; case "call": t.kind = 48; break; case "forall": t.kind = 49; break; + case "div": t.kind = 71; break; + case "mod": t.kind = 72; break; case "false": t.kind = 75; break; case "true": t.kind = 76; break; case "old": t.kind = 77; break; @@ -658,68 +658,64 @@ public class Scanner { case 38: {t.kind = 70; break;} case 39: - {t.kind = 71; break;} - case 40: - {t.kind = 72; break;} - case 41: {t.kind = 74; break;} - case 42: + case 40: {t.kind = 78; break;} - case 43: + case 41: {t.kind = 79; break;} - case 44: + case 42: {t.kind = 81; break;} - case 45: + case 43: {t.kind = 83; break;} - case 46: + case 44: {t.kind = 85; break;} - case 47: + case 45: {t.kind = 86; break;} - case 48: + case 46: {t.kind = 87; break;} - case 49: + case 47: recEnd = pos; recKind = 10; if (ch == '=') {AddCh(); goto case 20;} - else if (ch == ':') {AddCh(); goto case 47;} + else if (ch == ':') {AddCh(); goto case 45;} else {t.kind = 10; break;} - case 50: + case 48: recEnd = pos; recKind = 17; - if (ch == '=') {AddCh(); goto case 57;} + if (ch == '=') {AddCh(); goto case 55;} else if (ch == ':') {AddCh(); goto case 33;} else {t.kind = 17; break;} - case 51: + case 49: recEnd = pos; recKind = 18; if (ch == '=') {AddCh(); goto case 31;} else {t.kind = 18; break;} - case 52: + case 50: recEnd = pos; recKind = 26; - if (ch == '|') {AddCh(); goto case 43;} + if (ch == '|') {AddCh(); goto case 41;} else {t.kind = 26; break;} - case 53: + case 51: recEnd = pos; recKind = 29; - if (ch == '=') {AddCh(); goto case 58;} + if (ch == '=') {AddCh(); goto case 56;} else {t.kind = 29; break;} - case 54: + case 52: if (ch == '|') {AddCh(); goto case 29;} - else if (ch == '{') {AddCh(); goto case 42;} + else if (ch == '{') {AddCh(); goto case 40;} else {goto case 0;} - case 55: + case 53: recEnd = pos; recKind = 73; if (ch == '=') {AddCh(); goto case 32;} else {t.kind = 73; break;} - case 56: + case 54: recEnd = pos; recKind = 69; if (ch == '+') {AddCh(); goto case 37;} else {t.kind = 69; break;} - case 57: + case 55: recEnd = pos; recKind = 61; - if (ch == '=') {AddCh(); goto case 59;} + if (ch == '=') {AddCh(); goto case 57;} else {t.kind = 61; break;} - case 58: + case 56: recEnd = pos; recKind = 60; if (ch == '>') {AddCh(); goto case 23;} else {t.kind = 60; break;} - case 59: + case 57: recEnd = pos; recKind = 54; if (ch == '>') {AddCh(); goto case 21;} else {t.kind = 54; break;} diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index a8e12f63..f8b8b82b 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -451,7 +451,7 @@ namespace Microsoft.Boogie { op = " && "; break; case Microsoft.Boogie.BinaryOperator.Opcode.Div: - op = " / "; + op = " div "; break; case Microsoft.Boogie.BinaryOperator.Opcode.Eq: op = " == "; @@ -475,7 +475,7 @@ namespace Microsoft.Boogie { op = " < "; break; case Microsoft.Boogie.BinaryOperator.Opcode.Mod: - op = " % "; + op = " mod "; break; case Microsoft.Boogie.BinaryOperator.Opcode.Mul: op = " * "; diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl index 2854e5df..12ccc44a 100644 --- a/Test/livevars/bla1.bpl +++ b/Test/livevars/bla1.bpl @@ -471,7 +471,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl index 1decba12..ae8ff08c 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl @@ -510,7 +510,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl index 0b49364b..44e51827 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl @@ -521,7 +521,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl index 242acd65..fae3e863 100644 --- a/Test/livevars/stack_overflow.bpl +++ b/Test/livevars/stack_overflow.bpl @@ -831,7 +831,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index e4da94f4..e53e00b4 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -382,7 +382,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); -axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y); +axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); @@ -1173,7 +1173,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); -axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y); +axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); diff --git a/Test/test0/Answer b/Test/test0/Answer index 51a139b7..d57e7647 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -48,9 +48,13 @@ axiom x * y * z == x * y * z; axiom x * y * z * x == x * y * z; -axiom x / y / z == x / (y / z); +axiom x div y div z == x div (y div z); -axiom x / y / (z / x) == x / y / z; +axiom x div y div (z div x) == x div y div z; + +axiom x + y mod z == y mod z + x; + +axiom (x + y) mod z == x mod z + y mod z; axiom x - y - z == x - (y - z); diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl index 28fb47b8..c040ce26 100644 --- a/Test/test0/BadLabels1.bpl +++ b/Test/test0/BadLabels1.bpl @@ -28,7 +28,7 @@ procedure P1(y: int) { K: goto A; - if (y % 2 == 0) { + if (y mod 2 == 0) { goto L; M: } diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index a1f941d8..955faad8 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -11,8 +11,11 @@ axiom (x * y) + z == (x + y) * z; axiom x * y * z == (x * (y * z)); axiom (x * y) * (z * x) == (x * y) * z; -axiom x / y / z == (x / (y / z)); -axiom (x / y) / (z / x) == (x / y) / z; +axiom x div y div z == (x div (y div z)); +axiom (x div y) div (z div x) == (x div y) div z; + +axiom x + y mod z == ((y mod z) + x); +axiom (x + y) mod z == (x mod z) + (y mod z); axiom x - y - z == (x - (y - z)); axiom (x - y) - (z - x) == (x - y) - z; diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index ff723db2..c8ef88c8 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -330,23 +330,23 @@ function #shl(int, int) returns (int); function #shr(int, int) returns (int); -axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); +axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y); -axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); +axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y); -axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); +axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y); -axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); +axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0); -axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); +axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0); -axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); +axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y); -axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); +axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y); -axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); +axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y); -axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); +axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); @@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); -axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2); +axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2); const unique $UnknownRef: ref; diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index da529b84..05e392cb 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -330,23 +330,23 @@ function #shl(int, int) returns (int); function #shr(int, int) returns (int); -axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); +axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y); -axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); +axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y); -axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); +axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y); -axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); +axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0); -axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); +axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0); -axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); +axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y); -axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); +axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y); -axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); +axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y); -axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); +axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); @@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); -axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2); +axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2); const unique $UnknownRef: ref; diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 5b60dcab..86721a74 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -36,7 +36,7 @@ )) . font-lock-builtin-face) `(,(boogie-regexp-opt '( "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while" - "old" "forall" "exists" "lambda" "cast" + "old" "forall" "exists" "lambda" "cast" "div" "mod" "false" "true")) . font-lock-keyword-face) `(,(boogie-regexp-opt '("bool" "int" "bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9" diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index 02d14b93..4e38f654 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -23,13 +23,14 @@ namespace Demo "bv30", "bv31", "bv32", "bv64", "call", "complete", "const", + "div", "else", "ensures", "exists", "extends", "false", "forall", "free", "function", "goto", "havoc", "if", "implementation", "int", "invariant", "lambda", - "modifies", + "mod", "modifies", "old", "procedure", "requires", @@ -181,7 +182,7 @@ namespace Demo identList.Rule = MakePlusRule(identList, comma, ident); NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen; NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket; - BinOp.Rule = ToTerm("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|" + BinOp.Rule = ToTerm("+") | "-" | "*" | "div" | "mod" | "^" | "&" | "|" | "&&" | "||" | "==" | "!=" | greater | less | ">=" | "<=" | "is" | "=" | "+=" | "-=" @@ -376,7 +377,7 @@ namespace Demo #region 5. Operators precedence RegisterOperators(1, "<==>"); RegisterOperators(2, "+", "-"); - RegisterOperators(3, "*", "/", "%", "!!"); + RegisterOperators(3, "*", "div", "mod", "!!"); RegisterOperators(4, Associativity.Right, "^"); RegisterOperators(5, "||"); RegisterOperators(6, "&&"); diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 45eb050d..43336262 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -34,7 +34,7 @@ procedure,implementation, requires,modifies,ensures,free, % expressions - false,true,null,old,then, + false,true,null,old,then,div,mod, % statements assert,assume,havoc,call,if,else,while,invariant,break,return,goto, }, diff --git a/Util/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim index 667a2b8c..673f967e 100644 --- a/Util/vim/syntax/boogie.vim +++ b/Util/vim/syntax/boogie.vim @@ -15,7 +15,7 @@ set cpo&vim " type syn keyword bplType bool int " repeat / condition / label -syn keyword bplExpr forall exists cast returns lambda +syn keyword bplExpr forall exists cast returns lambda div mod syn keyword bplStmt goto return while call else if assert assume havoc then syn keyword bplDecl axiom function procedure type requires ensures modifies unique const var free implementation invariant " user labels -- cgit v1.2.3 From d3a315961bf6a7b83225f6311dcf40b0dbba6463 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Sep 2012 16:12:27 -0700 Subject: Boogie: updated syntax highlighting ("real") --- Util/Emacs/boogie-mode.el | 2 +- Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs | 8 +++----- Util/latex/boogie.sty | 2 +- Util/vim/syntax/boogie.vim | 2 +- 4 files changed, 6 insertions(+), 8 deletions(-) (limited to 'Util/latex') diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 86721a74..5763d695 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -38,7 +38,7 @@ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while" "old" "forall" "exists" "lambda" "cast" "div" "mod" "false" "true")) . font-lock-keyword-face) - `(,(boogie-regexp-opt '("bool" "int" + `(,(boogie-regexp-opt '("bool" "int" "real" "bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9" "bv10" "bv11" "bv12" "bv13" "bv14" "bv15" "bv16" "bv17" "bv18" "bv19" "bv20" "bv21" "bv22" "bv23" "bv24" "bv25" "bv26" "bv27" "bv28" "bv29" diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index 4e38f654..fd7c561d 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -33,8 +33,7 @@ namespace Demo "mod", "modifies", "old", "procedure", - "requires", - "return", "returns", + "real", "requires", "return", "returns", "then", "true", "type", "unique", "var", @@ -271,8 +270,7 @@ namespace Demo "modifies" | "old" | "procedure" | - "requires" | - "return" | "returns" | + "real" | "requires" | "return" | "returns" | "then" | "true" | "type" | "unique" | "var" | @@ -323,7 +321,7 @@ namespace Demo ; typeDecl.Rule - = (ToTerm("int") | "bool" | ident) + = (ToTerm("int") | "bool" | "real" | ident) ; fieldDecl.Rule diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 43336262..e67c61f4 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -19,7 +19,7 @@ \usepackage{listings} \lstdefinelanguage{boogie}{ - morekeywords={type,finite,bool,int,ref,% + morekeywords={type,bool,int,real,% bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,% bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,% bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,% diff --git a/Util/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim index 673f967e..6af66279 100644 --- a/Util/vim/syntax/boogie.vim +++ b/Util/vim/syntax/boogie.vim @@ -13,7 +13,7 @@ set cpo&vim " type -syn keyword bplType bool int +syn keyword bplType bool int real " repeat / condition / label syn keyword bplExpr forall exists cast returns lambda div mod syn keyword bplStmt goto return while call else if assert assume havoc then -- cgit v1.2.3