summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg23
-rw-r--r--Source/Dafny/Parser.cs58
-rw-r--r--Test/dafny0/Answer7
-rw-r--r--Test/dafny0/ChainingDisjointTests.dfy33
-rw-r--r--Test/dafny0/ParseErrors.dfy2
-rw-r--r--Test/dafny0/runtest.bat2
6 files changed, 96 insertions, 29 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ac573660..f6e40722 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1060,18 +1060,22 @@ OrOp = "||" | '\u2228'.
/*------------------------------------------------------------------------*/
RelationalExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken x, firstOpTok = null; Expression e0, e1; BinaryExpr.Opcode op;
+ IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
List<Expression> chain = null;
List<BinaryExpr.Opcode> ops = null;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
// 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
// 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
// 3 ("illegal") indicates illegal chain
+ // 4 ("disjoint") indicates chain of disjoint set operators
bool hasSeenNeq = false;
.)
Term<out e0> (. e = e0; .)
[ RelOp<out x, out op> (. firstOpTok = x; .)
- Term<out e1> (. e = new BinaryExpr(x, op, e0, e1); .)
+ Term<out e1> (. e = new BinaryExpr(x, op, e0, e1);
+ if (op == BinaryExpr.Opcode.Disjoint)
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+ .)
{ (. if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1087,6 +1091,8 @@ RelationalExpression<out Expression/*!*/ e>
case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge:
kind = 2; break;
+ case BinaryExpr.Opcode.Disjoint:
+ kind = 4; break;
default:
kind = 3; break;
}
@@ -1095,10 +1101,11 @@ RelationalExpression<out Expression/*!*/ e>
.)
RelOp<out x, out op> (. switch (op) {
case BinaryExpr.Opcode.Eq:
- if (kind == 3) { SemErr(x, "chaining not allowed from the previous operator"); }
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
break;
case BinaryExpr.Opcode.Neq:
if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
hasSeenNeq = true; break;
case BinaryExpr.Opcode.Lt:
case BinaryExpr.Opcode.Le:
@@ -1110,13 +1117,21 @@ RelationalExpression<out Expression/*!*/ e>
if (kind == 0) { kind = 2; }
else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
break;
+ case BinaryExpr.Opcode.Disjoint:
+ if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
+ break;
default:
SemErr(x, "this operator cannot be part of a chain");
kind = 3; break;
}
.)
Term<out e1> (. ops.Add(op); chain.Add(e1);
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+ if (op == BinaryExpr.Opcode.Disjoint) {
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ }
+ else
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
.)
}
]
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f9bb0768..e12ab7e3 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1552,13 +1552,14 @@ List<Expression/*!*/>/*!*/ decreases) {
void RelationalExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken x, firstOpTok = null; Expression e0, e1; BinaryExpr.Opcode op;
+ IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
List<Expression> chain = null;
List<BinaryExpr.Opcode> ops = null;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
// 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
// 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
// 3 ("illegal") indicates illegal chain
+ // 4 ("disjoint") indicates chain of disjoint set operators
bool hasSeenNeq = false;
Term(out e0);
@@ -1567,7 +1568,10 @@ List<Expression/*!*/>/*!*/ decreases) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
- e = new BinaryExpr(x, op, e0, e1);
+ e = new BinaryExpr(x, op, e0, e1);
+ if (op == BinaryExpr.Opcode.Disjoint)
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+
while (StartOf(16)) {
if (chain == null) {
chain = new List<Expression>();
@@ -1584,6 +1588,8 @@ List<Expression/*!*/>/*!*/ decreases) {
case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge:
kind = 2; break;
+ case BinaryExpr.Opcode.Disjoint:
+ kind = 4; break;
default:
kind = 3; break;
}
@@ -1593,30 +1599,40 @@ List<Expression/*!*/>/*!*/ decreases) {
RelOp(out x, out op);
switch (op) {
case BinaryExpr.Opcode.Eq:
- if (kind == 3) { SemErr(x, "chaining not allowed from the previous operator"); }
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
break;
case BinaryExpr.Opcode.Neq:
if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
- hasSeenNeq = true; break;
- case BinaryExpr.Opcode.Lt:
- case BinaryExpr.Opcode.Le:
- if (kind == 0) { kind = 1; }
- else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
- break;
- case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- if (kind == 0) { kind = 2; }
- else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
- break;
- default:
- SemErr(x, "this operator cannot be part of a chain");
- kind = 3; break;
- }
-
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
+ hasSeenNeq = true; break;
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ if (kind == 0) { kind = 1; }
+ else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
+ break;
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge:
+ if (kind == 0) { kind = 2; }
+ else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
+ break;
+ case BinaryExpr.Opcode.Disjoint:
+ if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
+ break;
+ default:
+ SemErr(x, "this operator cannot be part of a chain");
+ kind = 3; break;
+ }
+
Term(out e1);
ops.Add(op); chain.Add(e1);
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
-
+ if (op == BinaryExpr.Opcode.Disjoint)
+ {
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ }
+ else
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+
}
}
if (chain != null) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 384037ae..e5621773 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -450,12 +450,11 @@ ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(14,18): error: this operator cannot be part of a chain
ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-9 parse errors detected in ParseErrors.dfy
+8 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -1100,3 +1099,7 @@ ReturnErrors.dfy(41,10): Error: can only have initialization methods which modif
-------------------- ReturnTests.dfy --------------------
Dafny program verifier finished with 16 verified, 0 errors
+
+-------------------- ChainingDisjointTests.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny0/ChainingDisjointTests.dfy b/Test/dafny0/ChainingDisjointTests.dfy
new file mode 100644
index 00000000..17a4fa9f
--- /dev/null
+++ b/Test/dafny0/ChainingDisjointTests.dfy
@@ -0,0 +1,33 @@
+
+method testing1()
+{
+ var a, b, c := {1,2}, {3, 4}, {5, 6};
+ assert a !! b !! c;
+ testing2(a, b, c);
+ assert !({1,2} !! {2,3});
+ assert !({1,2} !! {9} !! {2,3}); // tests the accumulation
+ assert !({1,2} !! {9} !! {2,3});
+ assert !({1,2} !! {9} !! {8} !! {2,3}); // doesn't break at 4. that seems like a good stopping place.
+ assert !({9} !! {1,2} !! {8} !! {2,3});
+ assert !({9} !! {1} + {2} !! {8} !! {2,3}); // mixing in some other operators
+ assert !({1} !! {1} + {2});
+}
+
+method testing2(a: set<int>, b: set<int>, c: set<int>)
+ requires a !! b !! c;
+{
+ assert a !! b;
+ assert a !! c;
+ assert b !! c;
+}
+
+method testing3(a: set<int>, b: set<int>, c: set<int>, d: set<int>) // again with the four.
+ requires a !! b !! c !! d;
+{
+ assert a !! b;
+ assert a !! c;
+ assert b !! c;
+ assert a !! d;
+ assert b !! d;
+ assert c !! d;
+}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index d6f3005d..41df50eb 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -11,7 +11,7 @@ method TestChaining0(j: int, k: int, m: int)
method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set<T>>)
requires s <= t <= u >= s+u; // error: cannot mix <= and >=
ensures s <= u;
- ensures s !! t !! u; // error: !! is not chaining (but it would be nice if it were)
+ ensures s !! t !! u; // valid, means pairwise disjoint
ensures x in s in SuperSet; // error: 'in' is not chaining
ensures x !in s in SuperSet; // error: 'in' is not chaining
ensures x in s !in SuperSet; // error: 'in' is not chaining
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f606c183..143a0dc5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -19,7 +19,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
Termination.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
- ReturnErrors.dfy ReturnTests.dfy) do (
+ ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 22:32:24 +0000