summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg5
-rw-r--r--Source/Dafny/DafnyAst.cs43
-rw-r--r--Source/Dafny/Parser.cs29
-rw-r--r--Source/Dafny/Translator.cs8
-rw-r--r--Test/dafny0/Answer10
-rw-r--r--Test/dafny0/Calculations.dfy8
6 files changed, 74 insertions, 29 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 6b77d4a6..f67ae73f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1396,6 +1396,7 @@ CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
| '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
| EquivOp (. x = t; op = BinaryExpr.Opcode.Iff; .)
| ImpliesOp (. x = t; op = BinaryExpr.Opcode.Imp; .)
+ | ExpliesOp (. x = t; op = BinaryExpr.Opcode.Exp; .)
)
.
Hint<out BlockStmt s>
@@ -1433,9 +1434,9 @@ ImpliesExpliesExpression<out Expression/*!*/ e0>
[ ImpliesOp (. x = t; .)
ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
| ExpliesOp (. x = t; .)
- LogicalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)
+ LogicalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
{ ExpliesOp (. x = t; .)
- LogicalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)
+ LogicalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)
}
]
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b0450d7a..c5bd0abb 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -8,6 +8,7 @@ using System.Text;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Numerics;
+using System.Linq;
using Microsoft.Boogie;
namespace Microsoft.Dafny {
@@ -3107,13 +3108,36 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// Is op a valid calculation operator (i.e. a transitive relational operator)?
+ /// The line whose well-formedness is independant from other lines.
+ /// (Last line in case of explies-calculation, first line otherwise).
+ /// </summary>
+ public Expression InitalLine()
+ {
+ Contract.Requires(Lines.Count > 0);
+ Contract.Requires(Result != null); // Available after resolution
+ if (Result.Op == BinaryExpr.Opcode.Exp) {
+ return Lines.Last();
+ } else {
+ return Lines.First();
+ }
+ }
+
+ /// <summary>
+ /// Is op a valid calculation operator?
/// </summary>
[Pure]
public static bool ValidOp(BinaryExpr.Opcode op) {
return op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Lt || op == BinaryExpr.Opcode.Le || op == BinaryExpr.Opcode.Gt || op == BinaryExpr.Opcode.Ge
|| op == BinaryExpr.Opcode.Neq
- || op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp;
+ || LogicOp(op);
+ }
+
+ /// <summary>
+ /// Is op a valid operator only for Boolean lines?
+ /// </summary>
+ [Pure]
+ public static bool LogicOp(BinaryExpr.Opcode op) {
+ return op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp || op == BinaryExpr.Opcode.Exp;
}
/// <summary>
@@ -3126,9 +3150,10 @@ namespace Microsoft.Dafny {
return op2 == BinaryExpr.Opcode.Eq;
if (op1 == op2)
return true;
- if (op1 == BinaryExpr.Opcode.Iff || op1 == BinaryExpr.Opcode.Imp || op2 == BinaryExpr.Opcode.Iff || op2 == BinaryExpr.Opcode.Imp)
+ if (LogicOp(op1) || LogicOp(op2))
return op2 == BinaryExpr.Opcode.Eq ||
(op1 == BinaryExpr.Opcode.Imp && op2 == BinaryExpr.Opcode.Iff) ||
+ (op1 == BinaryExpr.Opcode.Exp && op2 == BinaryExpr.Opcode.Iff) ||
(op1 == BinaryExpr.Opcode.Eq && op2 == BinaryExpr.Opcode.Iff);
return op2 == BinaryExpr.Opcode.Eq ||
(op1 == BinaryExpr.Opcode.Lt && op2 == BinaryExpr.Opcode.Le) ||
@@ -3833,7 +3858,7 @@ namespace Microsoft.Dafny {
public enum Opcode {
Iff,
Imp,
- Exp, // turned into Imp during resolution; the order of subexpressions is reversed
+ Exp, // turned into Imp during resolution
And,
Or,
Eq,
@@ -4068,8 +4093,14 @@ namespace Microsoft.Dafny {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
this.Op = op;
- this.E0 = e0;
- this.E1 = e1;
+ if (op == Opcode.Exp) {
+ // The order of operands is reversed so that it can be turned into implication during resolution
+ this.E0 = e1;
+ this.E1 = e0;
+ } else {
+ this.E0 = e0;
+ this.E1 = e1;
+ }
}
public override IEnumerable<Expression> SubExpressions {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 17d4b0b9..d79ef23c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2270,6 +2270,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Imp;
break;
}
+ case 93: case 94: {
+ ExpliesOp();
+ x = t; op = BinaryExpr.Opcode.Exp;
+ break;
+ }
default: SynErr(192); break;
}
}
@@ -2311,6 +2316,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else SynErr(194);
}
+ void ExpliesOp() {
+ if (la.kind == 93) {
+ Get();
+ } else if (la.kind == 94) {
+ Get();
+ } else SynErr(195);
+ }
+
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0);
@@ -2335,12 +2348,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ExpliesOp();
x = t;
LogicalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
while (la.kind == 93 || la.kind == 94) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
}
}
}
@@ -2387,14 +2400,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- void ExpliesOp() {
- if (la.kind == 93) {
- Get();
- } else if (la.kind == 94) {
- Get();
- } else SynErr(195);
- }
-
void RelationalExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
@@ -3315,8 +3320,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,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, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,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,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
{x,T,T,x, x,x,T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
{x,T,T,x, x,x,T,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,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,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,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,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,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,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, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},
{x,T,T,x, x,x,T,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,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,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, T,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,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, 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,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},
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 03cee979..b73fad1e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4872,19 +4872,19 @@ namespace Microsoft.Dafny {
// assume wf[line<i>]:
AddComment(b, stmt, "assume wf[line" + i.ToString() + "]");
assertAsAssume = true;
- TrStmt_CheckWellformed(s.Lines[i], b, locals, etran, false);
+ TrStmt_CheckWellformed(s.Steps[i].E0, b, locals, etran, false);
assertAsAssume = false;
if (s.Steps[i].ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
// assume line<i>:
AddComment(b, stmt, "assume line" + i.ToString());
- b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Lines[i])));
+ b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Steps[i].E0)));
}
// hint:
AddComment(b, stmt, "Hint" + i.ToString());
TrStmt(s.Hints[i], b, locals, etran);
// check well formedness of the goal line:
AddComment(b, stmt, "assert wf[line" + (i + 1).ToString() + "]");
- TrStmt_CheckWellformed(s.Lines[i + 1], b, locals, etran, false);
+ TrStmt_CheckWellformed(s.Steps[i].E1, b, locals, etran, false);
bool splitHappened;
var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);
// assert step:
@@ -4904,7 +4904,7 @@ namespace Microsoft.Dafny {
// check well formedness of the first line:
b = new Bpl.StmtListBuilder();
AddComment(b, stmt, "assume wf[line0]");
- TrStmt_CheckWellformed(s.Lines.First(), b, locals, etran, false);
+ TrStmt_CheckWellformed(s.InitalLine(), b, locals, etran, false);
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
builder.Add(ifCmd);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 26d4de73..cdb63528 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1800,19 +1800,19 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
Calculations.dfy(3,4): Error: index out of range
Execution trace:
(0,0): anon0
- (0,0): anon20_Then
+ (0,0): anon24_Then
Calculations.dfy(8,13): Error: index out of range
Execution trace:
(0,0): anon0
- (0,0): anon22_Then
+ (0,0): anon26_Then
Calculations.dfy(8,17): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon22_Then
-Calculations.dfy(44,11): Error: assertion violation
+ (0,0): anon26_Then
+Calculations.dfy(52,11): Error: assertion violation
Execution trace:
(0,0): anon0
- Calculations.dfy(39,2): anon5_Else
+ Calculations.dfy(47,2): anon5_Else
Dafny program verifier finished with 5 verified, 4 errors
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 8ef36139..54a9a3d4 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -24,6 +24,14 @@ method CalcTest0(s: seq<int>) {
<==> { assert s[0] >= 0; } // OK: well-formed when the previous line is well-formed
s[0] > 0 || s[0] == 0; // OK: well-formed when the previous line is well-formed
}
+
+ calc { // same as the last one, but well-formedness is checked in reverse order
+ s[0] + 1 > 0;
+ <==>
+ s[0] >= 0;
+ <== { assert s[0] >= 0; }
+ 0 < |s|;
+ }
}
method CalcTest1(x: int, y: int) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 19:13:27 +0000