summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-11-05 01:24:43 +0000
committerGravatar rustanleino <unknown>2009-11-05 01:24:43 +0000
commitddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 (patch)
treeb2c7adc1e94b67d774aec3520d9c285662f94b60
parentb5a942353fc4cf0b6a6c3df853860171e421a26a (diff)
Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)".
Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness.
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 10:32:03 +0000