summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg5
-rw-r--r--Source/Dafny/DafnyAst.ssc7
-rw-r--r--Source/Dafny/Parser.ssc315
-rw-r--r--Source/Dafny/Printer.ssc1
-rw-r--r--Source/Dafny/Resolver.ssc7
-rw-r--r--Source/Dafny/Scanner.ssc101
-rw-r--r--Source/Dafny/Translator.ssc6
-rw-r--r--Test/VSI-Benchmarks/Answer4
-rw-r--r--Test/VSI-Benchmarks/b4.dfy10
-rw-r--r--Test/VSI-Benchmarks/b6.dfy2
-rw-r--r--Test/VSI-Benchmarks/b7.dfy4
-rw-r--r--Test/VSI-Benchmarks/b8.dfy32
-rw-r--r--Test/VSI-Benchmarks/runtest.bat3
-rw-r--r--Test/dafny0/BinaryTree.dfy8
-rw-r--r--Test/dafny0/DTypes.dfy6
-rw-r--r--Test/dafny0/ListContents.dfy4
-rw-r--r--Test/dafny0/ListReverse.dfy2
-rw-r--r--Test/dafny0/SchorrWaite.dfy12
-rw-r--r--Util/latex/dafny.sty1
19 files changed, 277 insertions, 253 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3d7630ae..9ab826ac 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1,8 +1,8 @@
-//-----------------------------------------------------------------------------
+/*-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
-//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------
// Dafny
@@ -679,6 +679,7 @@ RelOp<out Token! x, out BinaryExpr.Opcode op>
| "!=" (. x = token; op = BinaryExpr.Opcode.Neq; .)
| "!!" (. x = token; op = BinaryExpr.Opcode.Disjoint; .)
| "in" (. x = token; op = BinaryExpr.Opcode.In; .)
+ | "!in" (. x = token; op = BinaryExpr.Opcode.NotIn; .)
| '\u2260' (. x = token; op = BinaryExpr.Opcode.Neq; .)
| '\u2264' (. x = token; op = BinaryExpr.Opcode.Le; .)
| '\u2265' (. x = token; op = BinaryExpr.Opcode.Ge; .)
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 8f6821dd..59d1d0ae 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -936,7 +936,7 @@ namespace Microsoft.Dafny
public class BinaryExpr : Expression {
public enum Opcode { Iff, Imp, And, Or,
Eq, Neq, Lt, Le, Ge, Gt,
- Disjoint, In,
+ Disjoint, In, NotIn,
Add, Sub, Mul, Div, Mod }
public readonly Opcode Op;
public enum ResolvedOpcode {
@@ -947,10 +947,10 @@ namespace Microsoft.Dafny
// integers
Lt, Le, Ge, Gt, Add, Sub, Mul, Div, Mod,
// sets
- SetEq, SetNeq, ProperSubset, Subset, Superset, ProperSuperset, Disjoint, InSet,
+ SetEq, SetNeq, ProperSubset, Subset, Superset, ProperSuperset, Disjoint, InSet, NotInSet,
Union, Intersection, SetDifference,
// sequences
- SeqEq, SeqNeq, ProperPrefix, Prefix, Concat, InSeq
+ SeqEq, SeqNeq, ProperPrefix, Prefix, Concat, InSeq, NotInSeq
}
public ResolvedOpcode ResolvedOp; // filled in by resolution
@@ -968,6 +968,7 @@ namespace Microsoft.Dafny
case Opcode.Neq: return "!=";
case Opcode.Disjoint: return "!!";
case Opcode.In: return "in";
+ case Opcode.NotIn: return "!in";
case Opcode.Add: return "+";
case Opcode.Sub: return "-";
case Opcode.Mul: return "*";
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index a7c30d2f..0dc7df24 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -1,8 +1,3 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
using System.Collections.Generic;
using Microsoft.Boogie;
using Microsoft.Contracts;
@@ -10,7 +5,7 @@ using Microsoft.Contracts;
namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 86;
+ const int maxT = 87;
const bool T = true;
const bool x = false;
@@ -181,7 +176,7 @@ public static int Parse (List<ClassDecl!>! classes) {
mm.Add(m);
} else if (t.kind == 13) {
FrameDecl();
- } else Error(87);
+ } else Error(88);
}
static void FieldDecl(List<MemberDecl!>! mm) {
@@ -240,7 +235,7 @@ public static int Parse (List<ClassDecl!>! classes) {
}
ExtendedExpr(out bb);
body = bb;
- } else Error(88);
+ } else Error(89);
parseVarScope.PopMarker();
f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
@@ -282,7 +277,7 @@ public static int Parse (List<ClassDecl!>! classes) {
}
BlockStmt(out bb);
body = bb;
- } else Error(89);
+ } else Error(90);
parseVarScope.PopMarker();
m = new Method(id, id.val, typeArgs, ins, outs, req, mod, ens, body, attrs);
@@ -318,7 +313,7 @@ public static int Parse (List<ClassDecl!>! classes) {
ty = new IntType();
} else if (StartOf(4)) {
ReferenceType(out ty);
- } else Error(90);
+ } else Error(91);
}
static void IdentTypeOptional(out BoundVar! var) {
@@ -378,8 +373,8 @@ public static int Parse (List<ClassDecl!>! classes) {
Expression(out e);
Expect(9);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(91);
- } else Error(92);
+ } else Error(92);
+ } else Error(93);
}
static void BlockStmt(out Statement! block) {
@@ -442,7 +437,7 @@ public static int Parse (List<ClassDecl!>! classes) {
}
ty = new SeqType(gt[0]);
- } else Error(93);
+ } else Error(94);
}
static void GenericInstantiation(List<Type!>! gt) {
@@ -467,7 +462,7 @@ public static int Parse (List<ClassDecl!>! classes) {
reqs.Add(e);
} else if (t.kind == 29) {
ReadsClause(reads);
- } else Error(94);
+ } else Error(95);
}
static void ExtendedExpr(out Expression! e) {
@@ -477,7 +472,7 @@ public static int Parse (List<ClassDecl!>! classes) {
IfThenElseExpr(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(95);
+ } else Error(96);
Expect(6);
}
@@ -513,7 +508,7 @@ public static int Parse (List<ClassDecl!>! classes) {
IfThenElseExpr(out e1);
} else if (t.kind == 5) {
ExtendedExpr(out e1);
- } else Error(96);
+ } else Error(97);
e = new ITEExpr(x, e, e0, e1);
}
@@ -528,7 +523,7 @@ public static int Parse (List<ClassDecl!>! classes) {
ss.Add(s);
} else if (t.kind == 7) {
VarDeclStmts(ss);
- } else Error(97);
+ } else Error(98);
}
static void OneStmt(out Statement! s) {
@@ -548,7 +543,7 @@ public static int Parse (List<ClassDecl!>! classes) {
UseStmt(out s);
break;
}
- case 1: case 2: case 5: case 20: case 45: case 65: case 68: case 69: case 70: case 71: case 72: case 73: case 74: case 78: case 79: {
+ case 1: case 2: case 5: case 20: case 45: case 66: case 69: case 70: case 71: case 72: case 73: case 74: case 75: case 79: case 80: {
AssignStmt(out s);
break;
}
@@ -598,7 +593,7 @@ public static int Parse (List<ClassDecl!>! classes) {
s = new ReturnStmt(x);
break;
}
- default: Error(98); break;
+ default: Error(99); break;
}
}
@@ -743,7 +738,7 @@ public static int Parse (List<ClassDecl!>! classes) {
} else if (t.kind == 5) {
BlockStmt(out s);
els = s;
- } else Error(99);
+ } else Error(100);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -834,7 +829,7 @@ public static int Parse (List<ClassDecl!>! classes) {
} else if (t.kind == 37) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(100);
+ } else Error(101);
Expect(6);
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
parseVarScope.PopMarker();
@@ -855,7 +850,7 @@ public static int Parse (List<ClassDecl!>! classes) {
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(101);
+ } else Error(102);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -895,7 +890,7 @@ public static int Parse (List<ClassDecl!>! classes) {
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(102);
+ } else Error(103);
Expect(21);
}
@@ -903,11 +898,11 @@ public static int Parse (List<ClassDecl!>! classes) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 20 || t.kind == 78 || t.kind == 79) {
+ } else if (t.kind == 20 || t.kind == 79 || t.kind == 80) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(103);
- while (t.kind == 74 || t.kind == 76) {
+ } else Error(104);
+ while (t.kind == 75 || t.kind == 77) {
SelectOrCallSuffix(ref e);
}
}
@@ -928,7 +923,7 @@ public static int Parse (List<ClassDecl!>! classes) {
Get();
} else if (t.kind == 49) {
Get();
- } else Error(104);
+ } else Error(105);
}
static void LogicalExpression(out Expression! e0) {
@@ -966,7 +961,7 @@ public static int Parse (List<ClassDecl!>! classes) {
Get();
} else if (t.kind == 51) {
Get();
- } else Error(105);
+ } else Error(106);
}
static void RelationalExpression(out Expression! e0) {
@@ -984,7 +979,7 @@ public static int Parse (List<ClassDecl!>! classes) {
Get();
} else if (t.kind == 53) {
Get();
- } else Error(106);
+ } else Error(107);
}
static void OrOp() {
@@ -992,13 +987,13 @@ public static int Parse (List<ClassDecl!>! classes) {
Get();
} else if (t.kind == 55) {
Get();
- } else Error(107);
+ } else Error(108);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 64 || t.kind == 65) {
+ while (t.kind == 65 || t.kind == 66) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1050,27 +1045,32 @@ public static int Parse (List<ClassDecl!>! classes) {
}
case 61: {
Get();
- x = token; op = BinaryExpr.Opcode.Neq;
+ x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
case 62: {
Get();
- x = token; op = BinaryExpr.Opcode.Le;
+ x = token; op = BinaryExpr.Opcode.Neq;
break;
}
case 63: {
Get();
+ x = token; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 64: {
+ Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(108); break;
+ default: Error(109); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 41 || t.kind == 66 || t.kind == 67) {
+ while (t.kind == 41 || t.kind == 67 || t.kind == 68) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1079,23 +1079,23 @@ public static int Parse (List<ClassDecl!>! classes) {
static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 64) {
+ if (t.kind == 65) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 65) {
+ } else if (t.kind == 66) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(109);
+ } else Error(110);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 65) {
+ if (t.kind == 66) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 68 || t.kind == 69) {
+ } else if (t.kind == 69 || t.kind == 70) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1104,7 +1104,7 @@ public static int Parse (List<ClassDecl!>! classes) {
SelectExpression(out e);
} else if (StartOf(11)) {
ConstAtomExpression(out e);
- } else Error(110);
+ } else Error(111);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
@@ -1112,31 +1112,31 @@ public static int Parse (List<ClassDecl!>! classes) {
if (t.kind == 41) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 66) {
+ } else if (t.kind == 67) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 67) {
+ } else if (t.kind == 68) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(111);
+ } else Error(112);
}
static void NegOp() {
- if (t.kind == 68) {
+ if (t.kind == 69) {
Get();
- } else if (t.kind == 69) {
+ } else if (t.kind == 70) {
Get();
- } else Error(112);
+ } else Error(113);
}
static void SelectExpression(out Expression! e) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 20 || t.kind == 78 || t.kind == 79) {
+ } else if (t.kind == 20 || t.kind == 79 || t.kind == 80) {
ObjectExpression(out e);
- } else Error(113);
- while (t.kind == 74 || t.kind == 76) {
+ } else Error(114);
+ while (t.kind == 75 || t.kind == 77) {
SelectOrCallSuffix(ref e);
}
}
@@ -1146,17 +1146,17 @@ public static int Parse (List<ClassDecl!>! classes) {
e = dummyExpr;
switch (t.kind) {
- case 70: {
+ case 71: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 71: {
+ case 72: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 72: {
+ case 73: {
Get();
e = new LiteralExpr(token);
break;
@@ -1166,7 +1166,7 @@ public static int Parse (List<ClassDecl!>! classes) {
e = new LiteralExpr(token, n);
break;
}
- case 73: {
+ case 74: {
Get();
x = token;
Expect(20);
@@ -1193,17 +1193,17 @@ public static int Parse (List<ClassDecl!>! classes) {
Expect(6);
break;
}
- case 74: {
+ case 75: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(5)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(75);
+ Expect(76);
break;
}
- default: Error(114); break;
+ default: Error(115); break;
}
}
@@ -1242,10 +1242,10 @@ public static int Parse (List<ClassDecl!>! classes) {
static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 78) {
+ if (t.kind == 79) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 79) {
+ } else if (t.kind == 80) {
Get();
x = token;
Expect(20);
@@ -1258,9 +1258,9 @@ public static int Parse (List<ClassDecl!>! classes) {
QuantifierGuts(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(115);
+ } else Error(116);
Expect(21);
- } else Error(116);
+ } else Error(117);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1268,7 +1268,7 @@ public static int Parse (List<ClassDecl!>! classes) {
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 76) {
+ if (t.kind == 77) {
Get();
Ident(out id);
if (t.kind == 20) {
@@ -1281,13 +1281,13 @@ public static int Parse (List<ClassDecl!>! classes) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 74) {
+ } else if (t.kind == 75) {
Get();
x = token;
if (StartOf(5)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 77) {
+ if (t.kind == 78) {
Get();
anyDots = true;
if (StartOf(5)) {
@@ -1295,11 +1295,11 @@ public static int Parse (List<ClassDecl!>! classes) {
e1 = ee;
}
}
- } else if (t.kind == 77) {
+ } else if (t.kind == 78) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(117);
+ } else Error(118);
if (!anyDots) {
assert e1 == null;
e = new SeqSelectExpr(x, true, e, e0, null);
@@ -1308,8 +1308,8 @@ public static int Parse (List<ClassDecl!>! classes) {
e = new SeqSelectExpr(x, false, e, e0, e1);
}
- Expect(75);
- } else Error(118);
+ Expect(76);
+ } else Error(119);
}
static void QuantifierGuts(out Expression! q) {
@@ -1322,13 +1322,13 @@ public static int Parse (List<ClassDecl!>! classes) {
Triggers trigs = null;
Expression! body;
- if (t.kind == 80 || t.kind == 81) {
+ if (t.kind == 81 || t.kind == 82) {
Forall();
x = token; univ = true;
- } else if (t.kind == 82 || t.kind == 83) {
+ } else if (t.kind == 83 || t.kind == 84) {
Exists();
x = token;
- } else Error(119);
+ } else Error(120);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1352,27 +1352,27 @@ public static int Parse (List<ClassDecl!>! classes) {
}
static void Forall() {
- if (t.kind == 80) {
+ if (t.kind == 81) {
Get();
- } else if (t.kind == 81) {
+ } else if (t.kind == 82) {
Get();
- } else Error(120);
+ } else Error(121);
}
static void Exists() {
- if (t.kind == 82) {
+ if (t.kind == 83) {
Get();
- } else if (t.kind == 83) {
+ } else if (t.kind == 84) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void QSep() {
- if (t.kind == 84) {
+ if (t.kind == 85) {
Get();
- } else if (t.kind == 85) {
+ } else if (t.kind == 86) {
Get();
- } else Error(122);
+ } else Error(123);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1385,7 +1385,7 @@ public static int Parse (List<ClassDecl!>! classes) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(123);
+ } else Error(124);
Expect(6);
}
@@ -1417,7 +1417,7 @@ public static int Parse (List<ClassDecl!>! classes) {
} else if (StartOf(5)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(124);
+ } else Error(125);
}
@@ -1497,70 +1497,71 @@ public static int Parse (List<ClassDecl!>! classes) {
case 58: s = ">= expected"; break;
case 59: s = "!= expected"; break;
case 60: s = "!! expected"; break;
- case 61: s = "\\u2260 expected"; break;
- case 62: s = "\\u2264 expected"; break;
- case 63: s = "\\u2265 expected"; break;
- case 64: s = "+ expected"; break;
- case 65: s = "- expected"; break;
- case 66: s = "/ expected"; break;
- case 67: s = "% expected"; break;
- case 68: s = "! expected"; break;
- case 69: s = "\\u00ac expected"; break;
- case 70: s = "false expected"; break;
- case 71: s = "true expected"; break;
- case 72: s = "null expected"; break;
- case 73: s = "fresh expected"; break;
- case 74: s = "[ expected"; break;
- case 75: s = "] expected"; break;
- case 76: s = ". expected"; break;
- case 77: s = ".. expected"; break;
- case 78: s = "this expected"; break;
- case 79: s = "old expected"; break;
- case 80: s = "forall expected"; break;
- case 81: s = "\\u2200 expected"; break;
- case 82: s = "exists expected"; break;
- case 83: s = "\\u2203 expected"; break;
- case 84: s = ":: expected"; break;
- case 85: s = "\\u2022 expected"; break;
- case 86: s = "??? expected"; break;
- case 87: s = "invalid ClassMemberDecl"; break;
- case 88: s = "invalid FunctionDecl"; break;
- case 89: s = "invalid MethodDecl"; break;
- case 90: s = "invalid Type"; break;
- case 91: s = "invalid MethodSpec"; break;
+ case 61: s = "!in expected"; break;
+ case 62: s = "\\u2260 expected"; break;
+ case 63: s = "\\u2264 expected"; break;
+ case 64: s = "\\u2265 expected"; break;
+ case 65: s = "+ expected"; break;
+ case 66: s = "- expected"; break;
+ case 67: s = "/ expected"; break;
+ case 68: s = "% expected"; break;
+ case 69: s = "! expected"; break;
+ case 70: s = "\\u00ac expected"; break;
+ case 71: s = "false expected"; break;
+ case 72: s = "true expected"; break;
+ case 73: s = "null expected"; break;
+ case 74: s = "fresh expected"; break;
+ case 75: s = "[ expected"; break;
+ case 76: s = "] expected"; break;
+ case 77: s = ". expected"; break;
+ case 78: s = ".. expected"; break;
+ case 79: s = "this expected"; break;
+ case 80: s = "old expected"; break;
+ case 81: s = "forall expected"; break;
+ case 82: s = "\\u2200 expected"; break;
+ case 83: s = "exists expected"; break;
+ case 84: s = "\\u2203 expected"; break;
+ case 85: s = ":: expected"; break;
+ case 86: s = "\\u2022 expected"; break;
+ case 87: s = "??? expected"; break;
+ case 88: s = "invalid ClassMemberDecl"; break;
+ case 89: s = "invalid FunctionDecl"; break;
+ case 90: s = "invalid MethodDecl"; break;
+ case 91: s = "invalid Type"; break;
case 92: s = "invalid MethodSpec"; break;
- case 93: s = "invalid ReferenceType"; break;
- case 94: s = "invalid FunctionSpec"; break;
- case 95: s = "invalid ExtendedExpr"; break;
- case 96: s = "invalid IfThenElseExpr"; break;
- case 97: s = "invalid Stmt"; break;
- case 98: s = "invalid OneStmt"; break;
- case 99: s = "invalid IfStmt"; break;
- case 100: s = "invalid ForeachStmt"; break;
- case 101: s = "invalid AssignRhs"; break;
- case 102: s = "invalid Guard"; break;
- case 103: s = "invalid CallStmtSubExpr"; break;
- case 104: s = "invalid EquivOp"; break;
- case 105: s = "invalid ImpliesOp"; break;
- case 106: s = "invalid AndOp"; break;
- case 107: s = "invalid OrOp"; break;
- case 108: s = "invalid RelOp"; break;
- case 109: s = "invalid AddOp"; break;
- case 110: s = "invalid UnaryExpression"; break;
- case 111: s = "invalid MulOp"; break;
- case 112: s = "invalid NegOp"; break;
- case 113: s = "invalid SelectExpression"; break;
- case 114: s = "invalid ConstAtomExpression"; break;
- case 115: s = "invalid ObjectExpression"; break;
+ case 93: s = "invalid MethodSpec"; break;
+ case 94: s = "invalid ReferenceType"; break;
+ case 95: s = "invalid FunctionSpec"; break;
+ case 96: s = "invalid ExtendedExpr"; break;
+ case 97: s = "invalid IfThenElseExpr"; break;
+ case 98: s = "invalid Stmt"; break;
+ case 99: s = "invalid OneStmt"; break;
+ case 100: s = "invalid IfStmt"; break;
+ case 101: s = "invalid ForeachStmt"; break;
+ case 102: s = "invalid AssignRhs"; break;
+ case 103: s = "invalid Guard"; break;
+ case 104: s = "invalid CallStmtSubExpr"; break;
+ case 105: s = "invalid EquivOp"; break;
+ case 106: s = "invalid ImpliesOp"; break;
+ case 107: s = "invalid AndOp"; break;
+ case 108: s = "invalid OrOp"; break;
+ case 109: s = "invalid RelOp"; break;
+ case 110: s = "invalid AddOp"; break;
+ case 111: s = "invalid UnaryExpression"; break;
+ case 112: s = "invalid MulOp"; break;
+ case 113: s = "invalid NegOp"; break;
+ case 114: s = "invalid SelectExpression"; break;
+ case 115: s = "invalid ConstAtomExpression"; break;
case 116: s = "invalid ObjectExpression"; break;
- case 117: s = "invalid SelectOrCallSuffix"; break;
+ case 117: s = "invalid ObjectExpression"; break;
case 118: s = "invalid SelectOrCallSuffix"; break;
- case 119: s = "invalid QuantifierGuts"; break;
- case 120: s = "invalid Forall"; break;
- case 121: s = "invalid Exists"; break;
- case 122: s = "invalid QSep"; break;
- case 123: s = "invalid AttributeOrTrigger"; break;
- case 124: s = "invalid AttributeArg"; break;
+ case 119: s = "invalid SelectOrCallSuffix"; break;
+ case 120: s = "invalid QuantifierGuts"; break;
+ case 121: s = "invalid Forall"; break;
+ case 122: s = "invalid Exists"; break;
+ case 123: s = "invalid QSep"; break;
+ case 124: s = "invalid AttributeOrTrigger"; break;
+ case 125: s = "invalid AttributeArg"; break;
default: s = "error " + n; break;
}
@@ -1568,20 +1569,20 @@ public static int Parse (List<ClassDecl!>! classes) {
}
static bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,x,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,x, x,x,T,T, x,x,x,x, x,x,x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,x,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index 4a861553..ba44f9a9 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -575,6 +575,7 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Disjoint:
case BinaryExpr.Opcode.In:
+ case BinaryExpr.Opcode.NotIn:
opBindingStrength = 0x30; fragileLeftContext = fragileRightContext = true; break;
case BinaryExpr.Opcode.And:
opBindingStrength = 0x20; break;
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 66cdabe1..2159d3dc 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -1201,6 +1201,7 @@ namespace Microsoft.Dafny {
break;
case BinaryExpr.Opcode.In:
+ case BinaryExpr.Opcode.NotIn:
if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type))) {
Error(expr, "second argument to {0} must be a set or sequence of type {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
}
@@ -1355,6 +1356,12 @@ namespace Microsoft.Dafny {
} else {
return BinaryExpr.ResolvedOpcode.InSeq;
}
+ case BinaryExpr.Opcode.NotIn:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.NotInSet;
+ } else {
+ return BinaryExpr.ResolvedOpcode.NotInSeq;
+ }
case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod;
default:
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc
index e026ca7e..adbb7e1c 100644
--- a/Source/Dafny/Scanner.ssc
+++ b/Source/Dafny/Scanner.ssc
@@ -1,8 +1,3 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
using System.IO;
using System.Collections;
using System.Collections.Generic;
@@ -35,20 +30,20 @@ public class Scanner {
[Microsoft.Contracts.Verify(false)]
static Scanner() {
- start[0] = 50;
+ start[0] = 52;
start[33] = 31;
start[34] = 3;
- start[37] = 40;
+ start[37] = 42;
start[38] = 25;
start[39] = 1;
start[40] = 12;
start[41] = 13;
start[42] = 15;
- start[43] = 37;
+ start[43] = 39;
start[44] = 7;
- start[45] = 38;
- start[46] = 44;
- start[47] = 39;
+ start[45] = 40;
+ start[46] = 46;
+ start[47] = 41;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -91,9 +86,9 @@ public class Scanner {
start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 42;
+ start[91] = 44;
start[92] = 1;
- start[93] = 43;
+ start[93] = 45;
start[95] = 1;
start[96] = 1;
start[97] = 1;
@@ -125,19 +120,19 @@ public class Scanner {
start[123] = 5;
start[124] = 16;
start[125] = 6;
- start[172] = 41;
- start[8226] = 49;
+ start[172] = 43;
+ start[8226] = 51;
start[8658] = 24;
start[8660] = 20;
- start[8704] = 46;
- start[8707] = 47;
+ start[8704] = 48;
+ start[8707] = 49;
start[8743] = 27;
start[8744] = 29;
- start[8800] = 34;
- start[8804] = 35;
- start[8805] = 36;
+ start[8800] = 36;
+ start[8804] = 37;
+ start[8805] = 38;
}
- const int noSym = 86;
+ const int noSym = 87;
static short[] start = new short[16385];
@@ -221,7 +216,7 @@ public class Scanner {
}
}
-
+
static bool Comment0() {
int level = 1, line0 = line, lineStart0 = lineStart;
NextCh();
@@ -244,7 +239,7 @@ public class Scanner {
}
return false;
}
-
+
static bool Comment1() {
int level = 1, line0 = line, lineStart0 = lineStart;
NextCh();
@@ -311,14 +306,14 @@ public class Scanner {
case "in": t.kind = 44; break;
case "assert": t.kind = 46; break;
case "assume": t.kind = 47; break;
- case "false": t.kind = 70; break;
- case "true": t.kind = 71; break;
- case "null": t.kind = 72; break;
- case "fresh": t.kind = 73; break;
- case "this": t.kind = 78; break;
- case "old": t.kind = 79; break;
- case "forall": t.kind = 80; break;
- case "exists": t.kind = 82; break;
+ case "false": t.kind = 71; break;
+ case "true": t.kind = 72; break;
+ case "null": t.kind = 73; break;
+ case "fresh": t.kind = 74; break;
+ case "this": t.kind = 79; break;
+ case "old": t.kind = 80; break;
+ case "forall": t.kind = 81; break;
+ case "exists": t.kind = 83; break;
default: break;
}
@@ -357,7 +352,7 @@ public class Scanner {
{t.kind = 9; goto done;}
case 9:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 14;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 48;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 50;}
else {t.kind = 10; goto done;}
case 10:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
@@ -412,45 +407,51 @@ public class Scanner {
case 31:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 33;}
- else {t.kind = 68; goto done;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 34;}
+ else {t.kind = 69; goto done;}
case 32:
{t.kind = 59; goto done;}
case 33:
{t.kind = 60; goto done;}
case 34:
- {t.kind = 61; goto done;}
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 35;}
+ else {t.kind = noSym; goto done;}
case 35:
- {t.kind = 62; goto done;}
+ {t.kind = 61; goto done;}
case 36:
- {t.kind = 63; goto done;}
+ {t.kind = 62; goto done;}
case 37:
- {t.kind = 64; goto done;}
+ {t.kind = 63; goto done;}
case 38:
- {t.kind = 65; goto done;}
+ {t.kind = 64; goto done;}
case 39:
- {t.kind = 66; goto done;}
+ {t.kind = 65; goto done;}
case 40:
- {t.kind = 67; goto done;}
+ {t.kind = 66; goto done;}
case 41:
- {t.kind = 69; goto done;}
+ {t.kind = 67; goto done;}
case 42:
- {t.kind = 74; goto done;}
+ {t.kind = 68; goto done;}
case 43:
- {t.kind = 75; goto done;}
+ {t.kind = 70; goto done;}
case 44:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 45;}
- else {t.kind = 76; goto done;}
+ {t.kind = 75; goto done;}
case 45:
- {t.kind = 77; goto done;}
+ {t.kind = 76; goto done;}
case 46:
- {t.kind = 81; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 47;}
+ else {t.kind = 77; goto done;}
case 47:
- {t.kind = 83; goto done;}
+ {t.kind = 78; goto done;}
case 48:
- {t.kind = 84; goto done;}
+ {t.kind = 82; goto done;}
case 49:
+ {t.kind = 84; goto done;}
+ case 50:
{t.kind = 85; goto done;}
- case 50: {t.kind = 0; goto done;}
+ case 51:
+ {t.kind = 86; goto done;}
+ case 52: {t.kind = 0; goto done;}
}
done:
t.val = buf.ToString();
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index b1e6c3ea..09be93fa 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1919,6 +1919,9 @@ namespace Microsoft.Dafny {
Bpl.Expr e0 = TrExpr(e.E0);
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
return TrInSet(expr.tok, e0, e.E1, e.E0.Type); // let TrInSet translate e.E1
+ } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
+ Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, e.E0.Type); // let TrInSet translate e.E1
+ return Bpl.Expr.Not(arg);
}
Bpl.Expr e1 = TrExpr(e.E1);
switch (e.ResolvedOp) {
@@ -1998,6 +2001,9 @@ namespace Microsoft.Dafny {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(((SeqType!)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.InSeq:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1, e0);
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ Bpl.Expr arg = translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1, e0);
+ return Bpl.Expr.Not(arg);
default:
assert false; // unexpected binary expression
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 0149855c..a9fd2367 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -26,3 +26,7 @@ Dafny program verifier finished with 12 verified, 0 errors
-------------------- b7.dfy --------------------
Dafny program verifier finished with 11 verified, 0 errors
+
+-------------------- b8.dfy --------------------
+
+Dafny program verifier finished with 21 verified, 0 errors
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b0b370a0..ac58b7d1 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -26,7 +26,7 @@ class Map<Key,Value> {
method Find(key: Key) returns (present: bool, val: Value)
requires Valid();
- ensures !present ==> !(key in keys);
+ ensures !present ==> key !in keys;
ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
@@ -78,9 +78,9 @@ class Map<Key,Value> {
ensures (forall k :: k in old(keys) ==> k in keys || k == key);
// the given key is not there:
// other values don't change:
- ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);
+ ensures key !in old(keys) ==> keys == old(keys) && values == old(values);
ensures key in old(keys) ==>
- !(key in keys) &&
+ key !in keys &&
(exists h ::
0 <= h && h <= |keys| &&
keys[..h] == old(keys)[..h] &&
@@ -99,13 +99,13 @@ class Map<Key,Value> {
method FindIndex(key: Key) returns (idx: int)
requires Valid();
ensures -1 <= idx && idx < |keys|;
- ensures idx == -1 ==> !(key in keys);
+ ensures idx == -1 ==> key !in keys;
ensures 0 <= idx ==> keys[idx] == key;
{
var j := 0;
while (j < |keys|)
invariant j <= |keys|;
- invariant !(key in keys[..j]);
+ invariant key !in keys[..j];
decreases |keys| -j;
{
if (keys[j] == key) {
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index e5d061d2..f6e7879f 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -63,7 +63,7 @@ class Iterator {
function Valid():bool
reads this, footprint;
{
- this in footprint && c!= null && -1<= pos && !(null in footprint)
+ this in footprint && c!= null && -1<= pos && null !in footprint
}
method Init(coll:Collection)
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 13a8ccd2..95267823 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -36,7 +36,7 @@ class Stream {
function Valid():bool
reads this, footprint;
{
- !(null in footprint) && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method GetCount() returns (c:int)
@@ -152,7 +152,7 @@ class Client {
var wr:= new Stream;
call wr.Create();
while (0<|q.contents|)
- invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
decreases |q.contents|;
{
call ch:= q.Dequeue();
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index d499d017..643609d0 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -54,10 +54,10 @@ class Glossary {
while (true)
invariant rs.Valid() && fresh(rs.footprint);
invariant glossary.Valid();
- invariant !(glossary in rs.footprint);
- invariant !(null in glossary.keys);
+ invariant glossary !in rs.footprint;
+ invariant null !in glossary.keys;
//to do add invariant invariant (forall d:: d in glossary.values ==>!(null in d)); ***
- invariant !(q in rs.footprint);
+ invariant q !in rs.footprint;
// ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)
// we leave out the decreases clause - unbounded stream
{
@@ -80,8 +80,8 @@ class Glossary {
while (0<|q.contents|)
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
- invariant !(glossary in wr.footprint) && !(null in glossary.keys);
- invariant !(q in wr.footprint);
+ invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant q !in wr.footprint;
decreases |q.contents|;
{
var term, present, definition;
@@ -97,8 +97,8 @@ class Glossary {
while (i < |definition|)
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
- invariant !(glossary in wr.footprint) && !(null in glossary.keys);
- invariant !(q in wr.footprint);
+ invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant q !in wr.footprint;
invariant qcon == q.contents;
decreases |definition| -i;
{
@@ -125,7 +125,7 @@ class Glossary {
requires rs != null && rs.Valid();
modifies rs.footprint;
ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));
- ensures term != null ==> !(null in definition);
+ ensures term != null ==> null !in definition;
{
call term := rs.GetWord();
if (term != null)
@@ -133,7 +133,7 @@ class Glossary {
definition := [];
while (true)
invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
- invariant !(null in definition);
+ invariant null !in definition;
{
var w;
call w := rs.GetWord();
@@ -159,7 +159,7 @@ class ReaderStream {
function Valid():bool
reads this, footprint;
{
- !(null in footprint) && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method Open() //reading
@@ -193,7 +193,7 @@ class WriterStream {
function Valid():bool
reads this, footprint;
{
- !(null in footprint) && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method Create() //writing
@@ -271,7 +271,7 @@ class Map<Key,Value> {
method Find(key: Key) returns (present: bool, val: Value)
requires Valid();
- ensures !present ==> !(key in keys);
+ ensures !present ==> key !in keys;
ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
@@ -323,9 +323,9 @@ class Map<Key,Value> {
ensures (forall k :: k in old(keys) ==> k in keys || k == key);
// the given key is not there:
// other values don't change:
- ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);
+ ensures key !in old(keys) ==> keys == old(keys) && values == old(values);
ensures key in old(keys) ==>
- !(key in keys) &&
+ key !in keys &&
(exists h ::
0 <= h && h <= |keys| &&
keys[..h] == old(keys)[..h] &&
@@ -344,13 +344,13 @@ class Map<Key,Value> {
method FindIndex(key: Key) returns (idx: int)
requires Valid();
ensures -1 <= idx && idx < |keys|;
- ensures idx == -1 ==> !(key in keys);
+ ensures idx == -1 ==> key !in keys;
ensures 0 <= idx ==> keys[idx] == key;
{
var j := 0;
while (j < |keys|)
invariant j <= |keys|;
- invariant !(key in keys[..j]);
+ invariant key !in keys[..j];
decreases |keys| -j;
{
if (keys[j] == key) {
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a8658aef..fa737dca 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -7,7 +7,8 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy) do (
+for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy
+ b8.dfy ) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% %* %%f
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index b3bcc823..7a5fb3c7 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -12,7 +12,7 @@ class IntSet {
(root != null ==>
root in footprint && root.Valid() &&
contents == root.contents &&
- root.footprint <= footprint && !(this in root.footprint))
+ root.footprint <= footprint && this !in root.footprint)
}
method Init()
@@ -112,14 +112,14 @@ class Node {
reads this, footprint;
{
this in footprint &&
- !(null in footprint) &&
+ null !in footprint &&
(left != null ==>
left in footprint && left.Valid() &&
- left.footprint <= footprint && !(this in left.footprint) &&
+ left.footprint <= footprint && this !in left.footprint &&
(forall y :: y in left.contents ==> y < data)) &&
(right != null ==>
right in footprint && right.Valid() &&
- right.footprint <= footprint && !(this in right.footprint) &&
+ right.footprint <= footprint && this !in right.footprint &&
(forall y :: y in right.contents ==> data < y)) &&
(left == null && right == null ==>
contents == {data}) &&
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index f6e0a2b4..c468cff4 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -5,14 +5,14 @@ class C {
requires v != null;
{
var o: object := v;
- assert !(o in n); // should be known from the types involved
+ assert o !in n; // should be known from the types involved
}
method N(v: Stack)
/* this time without the precondition */
{
var o: object := v;
- assert !(o in n); // error: v may be null
+ assert o !in n; // error: v may be null
}
method A0(a: CP<int,C>, b: CP<int,object>)
@@ -31,7 +31,7 @@ class C {
var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
- requires !(null in b);
+ requires null !in b;
{
var x: set<object> := a2x;
var y: set<object> := b;
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 6cb7c5a0..01d8b63b 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -8,11 +8,11 @@ class Node<T> {
function Valid(): bool
reads this, footprint;
{
- this in this.footprint && !(null in this.footprint) &&
+ this in this.footprint && null !in this.footprint &&
(next == null ==> list == [data]) &&
(next != null ==>
next in footprint && next.footprint <= footprint &&
- !(this in next.footprint) &&
+ this !in next.footprint &&
list == [data] + next.list &&
next.Valid())
}
diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy
index af61a7a3..08b14751 100644
--- a/Test/dafny0/ListReverse.dfy
+++ b/Test/dafny0/ListReverse.dfy
@@ -3,7 +3,7 @@ class Node {
var nxt: Node;
method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)
- requires !(null in r);
+ requires null !in r;
requires x == null || x in r;
requires (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
modifies r;
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index db5928f4..20db882a 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -92,7 +92,7 @@ class Main {
var stackNodes := [];
var unmarkedNodes := S - {t}; // used as ghost variable
while (true)
- invariant root.marked && t in S && !(t in stackNodes);
+ invariant root.marked && t in S && t !in stackNodes;
// stackNodes has no duplicates:
invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>
stackNodes[i] != stackNodes[j]);
@@ -108,9 +108,9 @@ class Main {
stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]);
invariant 0 < |stackNodes| ==>
stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;
- invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n: Node :: n.children == old(n.children));
invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);
@@ -161,7 +161,7 @@ class Main {
var stackNodes := []; // used as ghost variable
var unmarkedNodes := S - {t}; // used as ghost variable
while (true)
- invariant root.marked && t != null && t in S && !(t in stackNodes);
+ invariant root.marked && t != null && t in S && t !in stackNodes;
invariant |stackNodes| == 0 <==> p == null;
invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1];
// stackNodes has no duplicates:
@@ -174,9 +174,9 @@ class Main {
(forall j :: 0 <= j && j < n.childrenVisited ==>
n.children[j] == null || n.children[j].marked));
invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);
- invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n :: n in stackNodes || n.children == old(n.children));
invariant (forall n :: n in stackNodes ==>
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 9f7a76b3..69cd6b0a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -33,6 +33,7 @@
{<==>}{$\Longleftrightarrow$}4
{forall}{$\forall$}1
{exists}{$\exists$}1
+ {!in}{$\not\in$}1
{\\in}{$\in$}1
% the following isn't actually Dafny, but it gives the option to produce nicer latex
{<<}{$\langle$}1
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 13:17:53 +0000