diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 00:02:43 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 00:02:43 -0700 |
| commit | 86da04e8be269d13874191c81cee0e2110d6373e (patch) | |
| tree | 3e179711e6f621ff10bbea22fbcaa9f0e9d62e47 | |
| parent | 0cf1c052a1b3f89384a6c859fc8680851b6edce0 (diff) | |
| parent | 17a14997cbcdad8bb0a435cf48dfb783ea21f3ac (diff) | |
Merge
29 files changed, 750 insertions, 67 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index e6d05bea..fafc9484 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -647,18 +647,3 @@ type TickType; var $Tick: TickType;
// ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// the connection between % and /
-axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
-
-// remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
-axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y);
-
-// the following axiom has some unfortunate matching, but it does state a property about % that
-// is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
-
-// ---------------------------------------------------------------
diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs index 095534e6..38c793c5 100644 --- a/Dafny/Cloner.cs +++ b/Dafny/Cloner.cs @@ -444,6 +444,10 @@ namespace Microsoft.Dafny var s = (ParallelStmt)stmt;
r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));
+
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source),
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index bc972495..4c425497 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -863,6 +863,7 @@ OneStmt<out Statement/*!*/ s> | WhileStmt<out s>
| MatchStmt<out s>
| ParallelStmt<out s>
+ | CalcStmt<out s>
| "label" (. x = t; .)
NoUSIdent<out id> ":"
OneStmt<out s> (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)
@@ -1315,6 +1316,82 @@ ParallelStmt<out Statement/*!*/ s> BlockStmt<out block, out bodyStart, out bodyEnd>
(. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
.
+
+CalcStmt<out Statement/*!*/ s>
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ Token x;
+ BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
+ var lines = new List<Expression/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
+ var customOps = new List<BinaryExpr.Opcode?>();
+ BinaryExpr.Opcode? maybeOp;
+ Expression/*!*/ e;
+ BlockStmt/*!*/ h;
+ IToken opTok;
+ .)
+ "calc" (. x = t; .)
+ [ CalcOp<out opTok, out calcOp> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
+ if (maybeOp == null) {
+ SemErr(opTok, "the main operator of a calculation must be transitive");
+ }
+ resOp = calcOp;
+ .)
+ ]
+ "{"
+ [ Expression<out e> (. lines.Add(e); .)
+ ";"
+ {
+ Hint<out h> (. hints.Add(h); .)
+ ( CalcOp<out opTok, out op> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
+ if (maybeOp == null) {
+ customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor
+ SemErr(opTok, "this operator cannot continue this calculation");
+ } else {
+ customOps.Add(op);
+ resOp = (BinaryExpr.Opcode)maybeOp;
+ }
+ .)
+ | (. customOps.Add(null); .)
+ )
+ Expression<out e> (. lines.Add(e); .)
+ ";"
+ }
+ ]
+ "}"
+ (. s = new CalcStmt(x, calcOp, lines, hints, customOps); .)
+ .
+CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
+= (. Contract.Ensures(Microsoft.Dafny.CalcStmt.ValidOp(Contract.ValueAtReturn(out op)));
+ op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
+ x = null;
+ .)
+ ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
+ | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
+ | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
+ | "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
+ | "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
+ | EquivOp (. x = t; op = BinaryExpr.Opcode.Iff; .)
+ | ImpliesOp (. x = t; op = BinaryExpr.Opcode.Imp; .)
+ )
+ .
+Hint<out BlockStmt s>
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
+ var subhints = new List<Statement/*!*/>();
+ IToken bodyStart, bodyEnd;
+ BlockStmt/*!*/ block;
+ Statement/*!*/ calc;
+ Token x = la;
+ .)
+ { BlockStmt<out block, out bodyStart, out bodyEnd> (. subhints.Add(block); .)
+ | CalcStmt<out calc> (. subhints.Add(calc); .)
+ }
+ (. s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+ .)
+ .
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
@@ -1600,7 +1677,7 @@ MapDisplayExpr<IToken/*!*/ mapToken, out Expression e> .
MapLiteralExpressions<.out List<ExpressionPair> elements.>
= (. Expression/*!*/ d, r;
- elements = new List<ExpressionPair/*!*/>(); .)
+ elements = new List<ExpressionPair/*!*/>(); .)
Expression<out d> ":=" Expression<out r> (. elements.Add(new ExpressionPair(d,r)); .)
{ "," Expression<out d> ":=" Expression<out r>(. elements.Add(new ExpressionPair(d,r)); .)
}
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index ccf96486..345fc6fa 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -2801,6 +2801,113 @@ namespace Microsoft.Dafny { }
}
+ public class CalcStmt : Statement
+ {
+ public readonly BinaryExpr.Opcode/*!*/ Op; // main operator of the calculation
+ public readonly List<Expression/*!*/> Lines;
+ public readonly List<BlockStmt/*!*/> Hints; // Hints[i] comes after line i; block statement is used as a container for multiple sub-hints
+ public readonly List<BinaryExpr.Opcode?> CustomOps; // CustomOps[i] comes after line i; null denotes the absence of a custom operator
+ public readonly List<BinaryExpr/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution in order to get the correct op
+ public BinaryExpr Result; // expression l0 op ln, filled in during resolution in order to get the correct op
+
+ public static readonly BinaryExpr.Opcode/*!*/ DefaultOp = BinaryExpr.Opcode.Eq;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(ValidOp(Op));
+ Contract.Invariant(Lines != null);
+ Contract.Invariant(Hints != null);
+ Contract.Invariant(CustomOps != null);
+ Contract.Invariant(Steps != null);
+ Contract.Invariant(Hints.Count == Math.Max(Lines.Count - 1, 0));
+ Contract.Invariant(CustomOps.Count == Hints.Count);
+ }
+
+ public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<BlockStmt/*!*/> hints, List<BinaryExpr.Opcode?> customOps)
+ : base(tok)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(ValidOp(op));
+ Contract.Requires(lines != null);
+ Contract.Requires(hints != null);
+ Contract.Requires(customOps != null);
+ Contract.Requires(cce.NonNullElements(lines));
+ Contract.Requires(cce.NonNullElements(hints));
+ Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));
+ Contract.Requires(customOps.Count == hints.Count);
+ this.Op = op;
+ this.Lines = lines;
+ this.Hints = hints;
+ this.CustomOps = customOps;
+ this.Steps = new List<BinaryExpr>();
+ this.Result = null;
+ }
+
+ public override IEnumerable<Statement> SubStatements
+ {
+ get {
+ foreach (var h in Hints) {
+ yield return h;
+ }
+ }
+ }
+ public override IEnumerable<Expression> SubExpressions
+ {
+ get {
+ foreach (var l in Lines) {
+ yield return l;
+ }
+ }
+ }
+
+ /// <summary>
+ /// Is op a valid calculation operator (i.e. a transitive relational 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;
+ }
+
+ /// <summary>
+ /// Does op1 subsume op2 (i.e. forall x, y, z :: (x op1 y op2 z) || (x op2 y op1 z) ==> x op1 z)?
+ /// </summary>
+ [Pure]
+ private static bool Subsumes(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {
+ Contract.Requires(ValidOp(op1) && ValidOp(op2));
+ if (op1 == BinaryExpr.Opcode.Neq || op2 == BinaryExpr.Opcode.Neq)
+ 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)
+ return op2 == BinaryExpr.Opcode.Eq ||
+ (op1 == BinaryExpr.Opcode.Imp && 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) ||
+ (op1 == BinaryExpr.Opcode.Gt && op2 == BinaryExpr.Opcode.Ge);
+ }
+
+ /// <summary>
+ /// Resulting operator x op z if x op1 y op2 z.
+ /// (Least upper bound in the Subsumes order).
+ /// Returns null if neither of op1 or op2 subsumes the other.
+ /// </summary>
+ [Pure]
+ public static BinaryExpr.Opcode? ResultOp(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {
+ Contract.Requires(ValidOp(op1) && ValidOp(op2));
+ Contract.Ensures(Contract.Result<BinaryExpr.Opcode?>() == null || ValidOp((BinaryExpr.Opcode)Contract.Result<BinaryExpr.Opcode?>()));
+ if (Subsumes(op1, op2)) {
+ return op1;
+ } else if (Subsumes(op2, op1)) {
+ return op2;
+ }
+ return null;
+ }
+ }
+
public class MatchStmt : Statement
{
[ContractInvariantMethod]
diff --git a/Dafny/DafnyPipeline.csproj b/Dafny/DafnyPipeline.csproj index f572f419..b4c2ae1e 100644 --- a/Dafny/DafnyPipeline.csproj +++ b/Dafny/DafnyPipeline.csproj @@ -127,10 +127,6 @@ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<ItemGroup>
- <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\Binaries\AIFramework.dll</HintPath>
- </Reference>
<Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\Binaries\Basetypes.dll</HintPath>
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index fe602f86..36658e2f 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -8,6 +8,7 @@ using System.IO; using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Numerics;
+using System.Linq;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny {
@@ -620,6 +621,40 @@ namespace Microsoft.Dafny { }
PrintStatement(s.Body, indent);
+ } else if (stmt is CalcStmt) {
+ CalcStmt s = (CalcStmt)stmt;
+ wr.Write("calc ");
+ if (s.Op != CalcStmt.DefaultOp) {
+ wr.Write(BinaryExpr.OpcodeString(s.Op));
+ wr.Write(" ");
+ }
+ wr.WriteLine("{");
+ int lineInd = indent + IndentAmount;
+ if (s.Lines.Count > 0) {
+ Indent(lineInd);
+ PrintExpression(s.Lines.First(), lineInd);
+ wr.WriteLine(";");
+ }
+ for (var i = 1; i < s.Lines.Count; i++){
+ var e = s.Lines[i];
+ var h = s.Hints[i - 1];
+ var op = s.CustomOps[i - 1];
+ foreach (var st in h.Body) {
+ Indent(lineInd);
+ PrintStatement(st, lineInd);
+ wr.WriteLine();
+ }
+ Indent(lineInd);
+ if (op != null && (BinaryExpr.Opcode)op != s.Op) {
+ wr.Write(BinaryExpr.OpcodeString((BinaryExpr.Opcode)op));
+ wr.Write(" ");
+ }
+ PrintExpression(e, lineInd);
+ wr.WriteLine(";");
+ }
+ Indent(indent);
+ wr.Write("}");
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
wr.Write("match ");
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index ae43dae4..61c5800f 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -8,6 +8,7 @@ using System.Collections.Generic; using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
+using System.Linq;
using Microsoft.Boogie;
namespace Microsoft.Dafny
@@ -1886,6 +1887,11 @@ namespace Microsoft.Dafny var s = (ParallelStmt)stmt;
CheckTypeInference(s.Range);
CheckTypeInference(s.Body);
+ } else if (stmt is CalcStmt) {
+ // NadiaToDo: is this correct?
+ var s = (CalcStmt)stmt;
+ s.SubExpressions.Iter(e => CheckTypeInference(e));
+ s.SubStatements.Iter(CheckTypeInference);
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
CheckTypeInference(s.Source);
@@ -3546,6 +3552,48 @@ namespace Microsoft.Dafny }
CheckParallelBodyRestrictions(s.Body, s.Kind);
}
+
+ } else if (stmt is CalcStmt) {
+ var prevErrorCount = ErrorCount;
+ CalcStmt s = (CalcStmt)stmt;
+ s.IsGhost = true;
+ if (s.Lines.Count > 0) {
+ var resOp = s.Op;
+ var e0 = s.Lines.First();
+ ResolveExpression(e0, true);
+ Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
+ for (int i = 1; i < s.Lines.Count; i++) {
+ var e1 = s.Lines[i];
+ ResolveExpression(e1, true);
+ Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e0.Type, e1.Type)) {
+ Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
+ } else {
+ BinaryExpr step;
+ var op = s.CustomOps[i - 1];
+ if (op == null) {
+ step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator
+ } else {
+ step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator
+ Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing
+ resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);
+ }
+ ResolveExpression(step, true);
+ s.Steps.Add(step);
+ }
+ e0 = e1;
+ }
+ foreach (var h in s.Hints) {
+ ResolveStatement(h, true, method);
+ }
+ if (prevErrorCount == ErrorCount && s.Steps.Count > 0) {
+ // do not build Result if there were errors, as it might be ill-typed and produce unnecessary resolution errors
+ s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());
+ ResolveExpression(s.Result, true);
+ }
+ }
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == 0 || s.Result != null);
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
@@ -4147,6 +4195,10 @@ namespace Microsoft.Dafny Contract.Assert(false); // unexpected kind
break;
}
+
+ } else if (stmt is CalcStmt) {
+ // cool
+ // NadiaTodo: ...I assume because it's always ghost
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 5d3d359a..40795129 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4384,6 +4384,61 @@ namespace Microsoft.Dafny { Contract.Assert(false); // unexpected kind
}
+ } else if (stmt is CalcStmt) {
+ /* Translate into:
+ if (*) {
+ // line well-formedness checks;
+ } else if (*) {
+ hint0;
+ assert t0 op t1;
+ assume false;
+ } else if (*) { ...
+ } else if (*) {
+ hint<n-1>;
+ assert t<n-1> op tn;
+ assume false;
+ }
+ assume t0 op tn;
+ */
+ var s = (CalcStmt)stmt;
+ Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver
+ AddComment(builder, stmt, "calc statement");
+ if (s.Lines.Count > 0) {
+ Bpl.IfCmd ifCmd = null;
+ Bpl.StmtListBuilder b;
+ // check steps:
+ for (int i = s.Steps.Count; 0 <= --i; ) {
+ b = new Bpl.StmtListBuilder();
+ TrStmt(s.Hints[i], b, locals, etran);
+ bool splitHappened;
+ var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);
+ if (!splitHappened) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
+ } else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));
+ }
+ }
+ }
+ b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+ ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
+ }
+ // check well-formedness of lines:
+ b = new Bpl.StmtListBuilder();
+ foreach (var e in s.Lines) {
+ TrStmt_CheckWellformed(e, 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);
+ // assume result:
+ if (s.Steps.Count > 0) {
+ Contract.Assert(s.Result != null); // established by the resolver
+ builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));
+ }
+ }
+
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 64f5fbbb..80f78d16 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -22,7 +22,6 @@ namespace Microsoft.Dafny using System.Diagnostics;
using VC;
using System.CodeDom.Compiler;
- using AI = Microsoft.AbstractInterpretationFramework;
public class DafnyDriver
{
@@ -536,9 +535,6 @@ namespace Microsoft.Dafny if (CommandLineOptions.Clo.UseAbstractInterpretation) {
if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {
Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
- } else if (CommandLineOptions.Clo.Ai.AnySet) {
- // run one of the old domains
- Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
} else {
// use /infer:j as the default
CommandLineOptions.Clo.Ai.J_Intervals = true;
@@ -575,13 +571,7 @@ namespace Microsoft.Dafny ConditionGeneration vcgen = null;
try
{
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}
catch (ProverException e)
{
diff --git a/DafnyDriver/DafnyDriver.csproj b/DafnyDriver/DafnyDriver.csproj index 5dac8f59..6f32302d 100644 --- a/DafnyDriver/DafnyDriver.csproj +++ b/DafnyDriver/DafnyDriver.csproj @@ -127,9 +127,6 @@ <Reference Include="AbsInt">
<HintPath>..\..\Binaries\AbsInt.dll</HintPath>
</Reference>
- <Reference Include="AIFramework">
- <HintPath>..\..\Binaries\AIFramework.dll</HintPath>
- </Reference>
<Reference Include="Core">
<HintPath>..\..\Binaries\Core.dll</HintPath>
</Reference>
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 2a262d70..0f7c50c1 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -43,6 +43,7 @@ method M(N: int, A: array<int>, B: array<int>) assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i])); // the elements of A were not changed by the loop
// it now follows from the surjectivity of A that A is the inverse of B:
assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);
+ assert (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);
}
static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 671c7c91..140f642f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -332,10 +332,10 @@ Execution trace: Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
Definedness.dfy(87,10): Error: possible violation of function precondition
@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-48 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+57 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +562,13 @@ 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
-8 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+14 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
@@ -857,19 +872,19 @@ Execution trace: Dafny program verifier finished with 32 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ (0,0): anon8_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Then
+ (0,0): anon8_Else
+ (0,0): anon9_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
@@ -1305,7 +1320,7 @@ CoPredicates.dfy(30,22): Related location: Related location Execution trace:
(0,0): anon0
-Dafny program verifier finished with 14 verified, 1 error
+Dafny program verifier finished with 12 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1615,6 +1630,25 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- Calculations.dfy --------------------
+Calculations.dfy(3,4): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Calculations.dfy(8,13): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(8,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(36,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Calculations.dfy(31,2): anon5_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
-------------------- IteratorResolution.dfy --------------------
IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy new file mode 100644 index 00000000..9e44f62e --- /dev/null +++ b/Test/dafny0/Calculations.dfy @@ -0,0 +1,37 @@ +method CalcTest0(s: seq<int>) { + calc { + s[0]; // error: ill-formed line + } + + calc { + 2; + { assert s[0] == 1; } // error: ill-formed hint + 1 + 1; + } + + if (|s| > 0) { + calc { + s[0]; // OK: well-formed in this context + { assert s[0] == s[0]; } + <= s[0]; + } + } +} + +method CalcTest1(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y; + } + assert x == 0; // OK: follows from x + y == y; +} + +method CalcTest2(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y + x; + } + assert x == 0; // error: even though assumed above, is not exported by the calculation +}
\ No newline at end of file diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy index 67dff91b..c5651c90 100644 --- a/Test/dafny0/CoPredicates.dfy +++ b/Test/dafny0/CoPredicates.dfy @@ -51,8 +51,9 @@ function U2(n: int): Stream<int> UpwardBy2(n)
}
-ghost method Lemma2(n: int)
- ensures Even(UpwardBy2(2*n)); // this is true, but Dafny can't prove it
-{
- assert Even(U2(2*n)); // ... thanks to this lemma
-}
+// Postponed:
+//ghost method Lemma2(n: int)
+// ensures Even(UpwardBy2(2*n)); // this is true, and Dafny can prove it
+//{
+// assert Even(U2(2*n)); // ... thanks to this lemma
+//}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index 41df50eb..9a3cc18b 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set ensures x in s == t; // error: 'in' is not chaining
{
}
+
+// ---------------------- calc statements -----------------------------------
+
+method TestCalc()
+{
+ calc {} // OK, empty calculations are allowed
+ calc {
+ 2 + 3; // OK, single-line calculations are allowed
+ }
+ calc {
+ 2 + 3;
+ calc { // OK: a calc statement is allowed as a sub-hint
+ 2;
+ 1 + 1;
+ }
+ calc {
+ 3;
+ 1 + 2;
+ }
+ { assert true; } // OK: multiple subhints are allowed between two lines
+ 1 + 1 + 1 + 2;
+ { assert 1 + 1 + 1 == 3; }
+ { assert true; }
+ 3 + 2;
+ }
+ calc != { // error: != is not allowed as the main operator of a calculation
+ 2 + 3;
+ 4;
+ }
+ calc { // OK, these operators are compatible
+ 2 + 3;
+ > 4;
+ >= 2 + 2;
+ }
+ calc < { // OK, these operators are compatible
+ 2 + 3;
+ == 5;
+ <= 3 + 3;
+ }
+ calc < { // error: cannot mix < and >= or >
+ 2 + 3;
+ >= 5;
+ > 2 + 2;
+ 6;
+ }
+ calc >= { // error: cannot mix >= and <= or !=
+ 2 + 3;
+ <= 5;
+ != 2 + 2;
+ 3;
+ }
+ calc { // error: cannot have more than one != per calc
+ 2 + 3;
+ != 4;
+ != 1 + 2;
+ 3;
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 274cc95a..c615c5ec 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -354,3 +354,32 @@ method MG1(l: GList, n: nat) var t := GCons(100, GNil);
t := GCons(120, l); // error: types don't match up (List<T$0> versus List<int>)
}
+
+// ------------------- calc statements ------------------------------
+
+method TestCalc(m: int, n: int, a: bool, b: bool)
+{
+ calc {
+ a + b; // error: invalid line
+ n + m;
+ }
+ calc {
+ a && b;
+ n + m; // error: all lines must have the same type
+ }
+ calc ==> {
+ n + m; // error: ==> operator requires boolean lines
+ n + m + 1;
+ n + m + 2;
+ }
+ calc {
+ n + m;
+ n + m + 1;
+ ==> n + m + 2; // error: ==> operator requires boolean lines
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 9789e7d7..9118e388 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- IteratorResolution.dfy Iterators.dfy) do (
+ Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 447f4365..2feaf6f7 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -54,3 +54,7 @@ Dafny program verifier finished with 3 verified, 0 errors -------------------- MonotonicHeapstate.dfy --------------------
Dafny program verifier finished with 36 verified, 0 errors
+
+-------------------- Calculations.dfy --------------------
+
+Dafny program verifier finished with 26 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy new file mode 100644 index 00000000..8c13457b --- /dev/null +++ b/Test/dafny2/Calculations.dfy @@ -0,0 +1,209 @@ +/* Lists */
+// Here are some standard definitions of List and functions on Lists
+
+datatype List<T> = Nil | Cons(T, List);
+
+function length(l: List): nat
+{
+ match l
+ case Nil => 0
+ case Cons(x, xs) => 1 + length(xs)
+}
+
+function concat(l: List, ys: List): List
+{
+ match l
+ case Nil => ys
+ case Cons(x, xs) => Cons(x, concat(xs, ys))
+}
+
+function reverse(l: List): List
+{
+ match l
+ case Nil => Nil
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))
+}
+
+function revacc(l: List, acc: List): List
+{
+ match l
+ case Nil => acc
+ case Cons(x, xs) => revacc(xs, Cons(x, acc))
+}
+
+function qreverse(l: List): List
+{
+ revacc(l, Nil)
+}
+
+// Here are two lemmas about the List functions.
+
+ghost method Lemma_ConcatNil()
+ ensures forall xs :: concat(xs, Nil) == xs;
+{
+}
+
+ghost method Lemma_RevCatCommute()
+ ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
+{
+}
+
+// Here is a theorem that says "qreverse" and "reverse" calculate the same result. The proof
+// is given in a calculational style. The proof is not minimal--some lines can be omitted
+// and Dafny will still fill in the details.
+
+ghost method Theorem_QReverseIsCorrect_Calc(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ calc {
+ qreverse(l);
+ // def. qreverse
+ revacc(l, Nil);
+ { Lemma_Revacc_calc(l, Nil); }
+ concat(reverse(l), Nil);
+ { Lemma_ConcatNil(); }
+ reverse(l);
+ }
+}
+
+ghost method Lemma_Revacc_calc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ concat(reverse(xs), ys);
+ // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys);
+ // induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ revacc(xrest, concat(Cons(x, Nil), ys));
+ // def. concat (x2)
+ revacc(xrest, Cons(x, ys));
+ // def. revacc
+ revacc(xs, ys);
+ }
+ }
+}
+
+// Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.
+
+ghost method Theorem_QReverseIsCorrect(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ assert qreverse(l)
+ == // def. qreverse
+ revacc(l, Nil);
+ Lemma_Revacc(l, Nil);
+ assert revacc(l, Nil)
+ == concat(reverse(l), Nil);
+ Lemma_ConcatNil();
+}
+
+ghost method Lemma_Revacc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ assert revacc(xs, ys)
+ == // def. revacc
+ revacc(xrest, Cons(x, ys));
+
+ assert concat(reverse(xs), ys)
+ == // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys)
+ == // induction hypothesis: Lemma3a(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ Lemma_RevCatCommute(); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ assert concat(revacc(xrest, Cons(x, Nil)), ys)
+ == revacc(xrest, concat(Cons(x, Nil), ys));
+
+ assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+
+ assert revacc(xrest, concat(Cons(x, Nil), ys))
+ == // the assert lemma just above
+ revacc(xrest, Cons(x, ys));
+ }
+}
+
+/* Fibonacci */
+// To further demonstrate what the "calc" construct can do, here are some proofs about the Fibonacci function.
+
+function Fib(n: nat): nat
+{
+ if n < 2 then n else Fib(n - 2) + Fib(n - 1)
+}
+
+ghost method Lemma_Fib()
+ ensures Fib(5) < 6;
+{
+ calc {
+ Fib(5);
+ Fib(4) + Fib(3);
+ calc {
+ Fib(2);
+ Fib(0) + Fib(1);
+ 0 + 1;
+ 1;
+ }
+ < 6;
+ }
+}
+
+/* List length */
+// Here are some proofs that show the use of nested calculations.
+
+ghost method Lemma_Concat_Length(xs: List, ys: List)
+ ensures length(concat(xs, ys)) == length(xs) + length(ys);
+{}
+
+ghost method Lemma_Reverse_Length(xs: List)
+ ensures length(xs) == length(reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ length(reverse(xs));
+ // def. reverse
+ length(concat(reverse(xrest), Cons(x, Nil)));
+ { Lemma_Concat_Length(reverse(xrest), Cons(x, Nil)); }
+ length(reverse(xrest)) + length(Cons(x, Nil));
+ // induction hypothesis
+ length(xrest) + length(Cons(x, Nil));
+ calc {
+ length(Cons(x, Nil));
+ // def. length
+ 1 + length(Nil);
+ // def. length
+ 1 + 0;
+ 1;
+ }
+ length(xrest) + 1;
+ // def. length
+ length(xs);
+ }
+ }
+}
+
+ghost method Window(xs: List, ys: List)
+ ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+{
+ calc {
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+ { if (length(xs) == length(ys)) {
+ calc {
+ length(reverse(xs));
+ { Lemma_Reverse_Length(xs); }
+ length(xs);
+ length(ys);
+ { Lemma_Reverse_Length(ys); }
+ length(reverse(ys));
+ } } }
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
+ true;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 909f67f5..72959830 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -16,7 +16,7 @@ for %%f in ( StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
- MonotonicHeapstate.dfy
+ MonotonicHeapstate.dfy Calculations.dfy
) do (
echo.
echo -------------------- %%f --------------------
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 4f437d23..1ba6186b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -40,7 +40,7 @@ `(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
"while" "print" "where"
- "old" "forall" "exists" "new" "parallel" "in" "this" "fresh"
+ "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 9d6f0882..ac1b755c 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -29,7 +29,7 @@ namespace Demo "in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
- "fresh", "old", "choose", "where"
+ "fresh", "old", "choose", "where", "calc"
);
StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
@@ -292,6 +292,7 @@ namespace Demo | "return"
| "yield"
| "parallel"
+ | "calc"
| "print"
| "returns"
| "yields"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln index e7391254..fd450cc8 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension.sln +++ b/Util/VS2010/DafnyExtension/DafnyExtension.sln @@ -1,6 +1,6 @@
-Microsoft Visual Studio Solution File, Format Version 11.00
-# Visual Studio 2010
+Microsoft Visual Studio Solution File, Format Version 12.00
+# Visual Studio 2012
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}"
EndProject
Global
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 9f22b887..39829bb0 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -231,9 +231,6 @@ namespace DafnyLanguage if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {
if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {
Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
- } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {
- // run one of the old domains
- Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
} else {
// use /infer:j as the default
Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;
@@ -258,11 +255,7 @@ namespace DafnyLanguage ConditionGeneration vcgen = null;
try {
- if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {
- vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else {
- vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
} catch (Bpl.ProverException) {
return PipelineOutcome.FatalError;
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index 66370dec..2580c396 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -1,5 +1,6 @@ <?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
@@ -14,6 +15,12 @@ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<GeneratePkgDefFile>false</GeneratePkgDefFile>
+ <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>
+ <FileUpgradeFlags>
+ </FileUpgradeFlags>
+ <UpgradeBackupLocation>
+ </UpgradeBackupLocation>
+ <OldToolsVersion>4.0</OldToolsVersion>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -158,8 +165,13 @@ <ItemGroup>
<WCFMetadata Include="Service References\" />
</ItemGroup>
+ <PropertyGroup>
+ <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>
+ <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>
+ </PropertyGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />
+ <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />
+ <Import Project="$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" Condition="false" />
<PropertyGroup>
<PostBuildEvent>cd</PostBuildEvent>
<PostBuildEvent>
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 22388704..2f295429 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -227,10 +227,12 @@ namespace DafnyLanguage #region keywords
case "allocated":
case "array":
+ case "as":
case "assert":
case "assume":
case "bool":
case "break":
+ case "calc":
case "case":
case "choose":
case "class":
@@ -249,7 +251,7 @@ namespace DafnyLanguage case "function":
case "ghost":
case "if":
- case "imports":
+ case "import":
case "in":
case "int":
case "invariant":
@@ -265,6 +267,7 @@ namespace DafnyLanguage case "null":
case "object":
case "old":
+ case "opened":
case "parallel":
case "predicate":
case "print":
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest index d822fbfc..ef5c1cf5 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest +++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest @@ -10,6 +10,9 @@ <VisualStudio Version="10.0">
<Edition>Pro</Edition>
</VisualStudio>
+ <VisualStudio Version="11.0">
+ <Edition>Pro</Edition>
+ </VisualStudio>
</SupportedProducts>
<SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />
</Identifier>
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 88f9c2a2..879b90cb 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -15,7 +15,7 @@ match,case,false,true,null,old,fresh,choose,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
- parallel,where
+ parallel,where,calc
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index d67d275a..45afbcf0 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -10,7 +10,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel -syntax keyword dafnyStatement assume assert return yield new print break label where +syntax keyword dafnyStatement assume assert return yield new print break label where calc syntax keyword dafnyKeyword var ghost returns yields null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant |