From b4fa8bffd5db8bc5a68faf8f3b1f3587ce813f23 Mon Sep 17 00:00:00 2001 From: chmaria Date: Tue, 12 Jun 2012 04:34:14 +0200 Subject: Dafny: Added tests. --- Test/dafny1/AnswerNoRuntimeChecking | 76 ++++++++++++++++++++++++++++++++ Test/dafny1/AnswerRuntimeChecking | 27 ++++++++++++ Test/dafny1/runtestNoRuntimeChecking.bat | 36 +++++++++++++++ Test/dafny1/runtestRuntimeChecking.bat | 51 +++++++++++++++++++++ 4 files changed, 190 insertions(+) create mode 100644 Test/dafny1/AnswerNoRuntimeChecking create mode 100644 Test/dafny1/AnswerRuntimeChecking create mode 100644 Test/dafny1/runtestNoRuntimeChecking.bat create mode 100644 Test/dafny1/runtestRuntimeChecking.bat (limited to 'Test/dafny1') diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking new file mode 100644 index 00000000..5472ec14 --- /dev/null +++ b/Test/dafny1/AnswerNoRuntimeChecking @@ -0,0 +1,76 @@ + +-------------------- Queue -------------------- +Compiled assembly into Queue.dll + +-------------------- PriorityQueue -------------------- +Compiled assembly into PriorityQueue.dll + +-------------------- ExtensibleArray -------------------- +Compiled assembly into ExtensibleArray.exe + +-------------------- ExtensibleArrayAuto -------------------- +Compiled assembly into ExtensibleArrayAuto.exe + +-------------------- BinaryTree -------------------- +Compiled assembly into BinaryTree.dll + +-------------------- UnboundedStack -------------------- +Compiled assembly into UnboundedStack.dll + +-------------------- ListCopy -------------------- +Compilation error: an assume statement cannot be compiled (line 14) +Compilation error: an assume statement cannot be compiled (line 15) + +-------------------- ListReverse -------------------- +Compiled assembly into ListReverse.dll + +-------------------- ListContents -------------------- +Compiled assembly into ListContents.dll + +-------------------- MatrixFun -------------------- +Compiled assembly into MatrixFun.exe + +-------------------- pow2 -------------------- +Compiled assembly into pow2.dll + +-------------------- SchorrWaite -------------------- +Compiled assembly into SchorrWaite.dll + +-------------------- Cubes -------------------- +Compiled assembly into Cubes.dll + +-------------------- SumOfCubes -------------------- +Compiled assembly into SumOfCubes.dll + +-------------------- FindZero -------------------- +Compiled assembly into FindZero.dll + +-------------------- TerminationDemos -------------------- +Compiled assembly into TerminationDemos.dll + +-------------------- Substitution -------------------- +Compiled assembly into Substitution.dll + +-------------------- KatzManna -------------------- +Compilation error: an assume statement cannot be compiled (line 66) + +-------------------- Induction -------------------- +Compiled assembly into Induction.dll + +-------------------- Rippling -------------------- +Compilation error: Arbitrary type ('FunctionValue') cannot be compiled + +-------------------- Celebrity -------------------- +Compilation error: Function _default._default.Knows has no body +Compilation error: an assume statement cannot be compiled (line 16) + +-------------------- BDD -------------------- +Compiled assembly into BDD.dll + +-------------------- UltraFilter -------------------- +Compilation error: Method _default.UltraFilter.H has no body +Compilation error: an assume statement cannot be compiled (line 42) +Compilation error: an assume statement cannot be compiled (line 45) +Compilation error: an assume statement cannot be compiled (line 76) +Compilation error: an assume statement cannot be compiled (line 97) +Compilation error: an assume statement cannot be compiled (line 98) diff --git a/Test/dafny1/AnswerRuntimeChecking b/Test/dafny1/AnswerRuntimeChecking new file mode 100644 index 00000000..1ade5aeb --- /dev/null +++ b/Test/dafny1/AnswerRuntimeChecking @@ -0,0 +1,27 @@ + +-------------------- ListReverse -------------------- +Compiled assembly into ListReverse.dll +Rewrote assembly into ListReverse.dll + +-------------------- MatrixFun -------------------- +Compiled assembly into MatrixFun.exe +Rewrote assembly into MatrixFun.exe + +-------------------- pow2 -------------------- +Compiled assembly into pow2.dll +Rewrote assembly into pow2.dll + +-------------------- Cubes -------------------- +Compiled assembly into Cubes.dll +Rewrote assembly into Cubes.dll + +-------------------- Substitution -------------------- +Compiled assembly into Substitution.dll +Rewrote assembly into Substitution.dll + +-------------------- KatzManna -------------------- +Compiled assembly into KatzManna.dll +Rewrote assembly into KatzManna.dll + +-------------------- Rippling -------------------- +Compilation error: Arbitrary type ('FunctionValue') cannot be compiled diff --git a/Test/dafny1/runtestNoRuntimeChecking.bat b/Test/dafny1/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..a4989fa1 --- /dev/null +++ b/Test/dafny1/runtestNoRuntimeChecking.bat @@ -0,0 +1,36 @@ +@echo off +setlocal + +set BOOGIEDIR=..\..\Binaries +set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe +set BPLEXE=%BOOGIEDIR%\Boogie.exe + +REM bugs: +REM SeparationLogicList +REM TreeDatatype +REM MoreInduction + +for %%f in (Queue PriorityQueue ExtensibleArray ExtensibleArrayAuto + BinaryTree UnboundedStack ListCopy ListReverse ListContents + MatrixFun pow2 SchorrWaite Cubes SumOfCubes FindZero + TerminationDemos Substitution KatzManna Induction Rippling + Celebrity BDD UltraFilter) do ( + echo. + echo -------------------- %%f -------------------- + %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy + if exist %%f.cs. ( + del %%f.cs + ) + if exist %%f.exe. ( + del %%f.exe + ) + if exist %%f.dll. ( + del %%f.dll + ) + if exist %%f.pdb. ( + del %%f.pdb + ) + if exist %%f.pdb.original. ( + del %%f.pdb.original + ) +) diff --git a/Test/dafny1/runtestRuntimeChecking.bat b/Test/dafny1/runtestRuntimeChecking.bat new file mode 100644 index 00000000..fc32fbf4 --- /dev/null +++ b/Test/dafny1/runtestRuntimeChecking.bat @@ -0,0 +1,51 @@ +@echo off +setlocal + +set BOOGIEDIR=..\..\Binaries +set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe +set BPLEXE=%BOOGIEDIR%\Boogie.exe + +REM bugs: +REM SeparationLogicList +REM TreeDatatype +REM MoreInduction + +REM to implement: +REM Queue : parallel statements +REM PriorityQueue : ghost state +REM ExtensibleArray : ghost state +REM ExtensibleArrayAuto: ghost state +REM BinaryTree : old expressions +REM UnboundedStack : ghost state +REM ListCopy : fresh expressions +REM ListContents : old expressions +REM SchorrWaite : ghost state +REM SumOfCubes : ghost state +REM FindZero : ghost state +REM TerminationDemos : ghost state +REM Induction : quantifiers +REM Celebrity : quantifiers +REM BDD : ghost state +REM UltraFilter : quantifiers + +for %%f in (ListReverse MatrixFun pow2 Cubes Substitution KatzManna + Rippling) do ( + echo. + echo -------------------- %%f -------------------- + %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy + if exist %%f.cs. ( + del %%f.cs + ) + if exist %%f.exe. ( + del %%f.exe + ) + if exist %%f.dll. ( + del %%f.dll + ) + if exist %%f.pdb. ( + del %%f.pdb + ) + if exist %%f.pdb.original. ( + del %%f.pdb.original + ) +) -- cgit v1.2.3 From 04004e1fe9a062f49406de401d917909df1063ce Mon Sep 17 00:00:00 2001 From: Unknown Date: Tue, 19 Jun 2012 17:47:37 -0700 Subject: Dafny: improved refinement features; added staged version of the proof of the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible) --- Dafny/Dafny.atg | 5 +- Dafny/DafnyAst.cs | 15 +++ Dafny/Parser.cs | 5 +- Dafny/RefinementTransformer.cs | 27 +++- Dafny/Translator.cs | 13 +- Test/dafny1/Answer | 4 + Test/dafny1/SchorrWaite-stages.dfy | 267 +++++++++++++++++++++++++++++++++++++ Test/dafny1/runtest.bat | 2 +- 8 files changed, 320 insertions(+), 18 deletions(-) create mode 100644 Test/dafny1/SchorrWaite-stages.dfy (limited to 'Test/dafny1') diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 4a99c9ee..cbdf5c79 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -925,16 +925,13 @@ WhileStmt ) (. if (guardOmitted || bodyOmitted) { - if (decreases.Count != 0) { - SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops"); - } if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); } if (body == null) { body = new BlockStmt(x, new List()); } - stmt = new WhileStmt(x, guard, invariants, new Specification(null, null), new Specification(null, null), body); + stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted); } else { stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index a57ef79d..5e6ad5c3 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -2136,6 +2136,21 @@ namespace Microsoft.Dafny { } } + /// + /// This class is really just a WhileStmt, except that it serves the purpose of remembering if the object was created as the result of a refinement + /// merge. + /// + public class RefinedWhileStmt : WhileStmt + { + public RefinedWhileStmt(IToken tok, Expression guard, + List/*!*/ invariants, Specification/*!*/ decreases, Specification/*!*/ mod, + BlockStmt/*!*/ body) + : base(tok, guard, invariants, decreases, mod, body) { + Contract.Requires(tok != null); + Contract.Requires(body != null); + } + } + public class AlternativeLoopStmt : LoopStmt { public readonly List Alternatives; diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 49e02bd8..d6ae7e93 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -1379,16 +1379,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bodyOmitted = true; } else SynErr(149); if (guardOmitted || bodyOmitted) { - if (decreases.Count != 0) { - SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops"); - } if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); } if (body == null) { body = new BlockStmt(x, new List()); } - stmt = new WhileStmt(x, guard, invariants, new Specification(null, null), new Specification(null, null), body); + stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted); } else { stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index 51b22443..56006a7f 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -865,7 +865,7 @@ namespace Microsoft.Dafny { } else { var resultingThen = MergeBlockStmt(skel.Thn, oldIf.Thn); var resultingElse = MergeElse(skel.Els, oldIf.Els); - var r = new IfStmt(skel.Tok, skel.Guard, resultingThen, resultingElse); + var r = new IfStmt(skel.Tok, CloneExpr(oldIf.Guard), resultingThen, resultingElse); body.Add(r); i++; j++; } @@ -1032,22 +1032,35 @@ namespace Microsoft.Dafny { // Note, the parser produces errors if there are any decreases or modifies clauses (and it creates // the Specification structures with a null list). - Contract.Assume(cNew.Decreases.Expressions == null); Contract.Assume(cNew.Mod.Expressions == null); + // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause. + // Any "decreases *" clause is not inherited, so if the previous loop was specified with "decreases *", then the new loop needs + // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus + // get a default "decreases" loop. + Specification decr; + if (Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) { + decr = cNew.Decreases; // take the new decreases clauses, whatever they may be (including nothing at all) + } else { + if (cNew.Decreases.Expressions.Count != 0) { + reporter.Error(cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'"); + } + decr = CloneSpecExpr(cOld.Decreases); + } + var invs = cOld.Invariants.ConvertAll(CloneMayBeFreeExpr); invs.AddRange(cNew.Invariants); - var r = new WhileStmt(cNew.Tok, guard, invs, CloneSpecExpr(cOld.Decreases), CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body)); + var r = new RefinedWhileStmt(cNew.Tok, guard, invs, decr, CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body)); return r; } Statement MergeElse(Statement skeleton, Statement oldStmt) { - Contract.Requires(skeleton == null || skeleton is BlockStmt || skeleton is IfStmt); - Contract.Requires(oldStmt == null || oldStmt is BlockStmt || oldStmt is IfStmt); + Contract.Requires(skeleton == null || skeleton is BlockStmt || skeleton is IfStmt || skeleton is SkeletonStatement); + Contract.Requires(oldStmt == null || oldStmt is BlockStmt || oldStmt is IfStmt || oldStmt is SkeletonStatement); if (skeleton == null) { return CloneStmt(oldStmt); - } else if (skeleton is IfStmt) { + } else if (skeleton is IfStmt || skeleton is SkeletonStatement) { // wrap a block statement around the if statement skeleton = new BlockStmt(skeleton.Tok, new List() { skeleton }); } @@ -1055,7 +1068,7 @@ namespace Microsoft.Dafny { if (oldStmt == null) { // make it into an empty block statement oldStmt = new BlockStmt(skeleton.Tok, new List()); - } else if (oldStmt is IfStmt) { + } else if (oldStmt is IfStmt || oldStmt is SkeletonStatement) { // wrap a block statement around the if statement oldStmt = new BlockStmt(oldStmt.Tok, new List() { oldStmt }); } diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index c05d9a38..1290f3ad 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4219,7 +4219,16 @@ namespace Microsoft.Dafny { decrs.Add(etran.TrExpr(e)); } Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false, false); - loopBodyBuilder.Add(Assert(s.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease")); + string msg; + if (inferredDecreases) { + msg = "cannot prove termination; try supplying a decreases clause for the loop"; + if (s is RefinedWhileStmt) { + msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)"; + } + } else { + msg = "decreases expression might not decrease"; + } + loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg)); } // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check // of invariant-maintenance can use the appropriate canCall predicates. @@ -4597,7 +4606,7 @@ namespace Microsoft.Dafny { if (allowance != null) { decrExpr = Bpl.Expr.Or(allowance, decrExpr); } - var msg = inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"; + string msg = inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"; if (hint != null) { msg += " (" + hint + ")"; } diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 7c7719ee..06cac03b 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -51,6 +51,10 @@ Dafny program verifier finished with 8 verified, 0 errors Dafny program verifier finished with 10 verified, 0 errors +-------------------- SchorrWaite-stages.dfy -------------------- + +Dafny program verifier finished with 16 verified, 0 errors + -------------------- Cubes.dfy -------------------- Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy new file mode 100644 index 00000000..5a4da8ce --- /dev/null +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -0,0 +1,267 @@ +// Schorr-Waite algorithms, written and verified in Dafny. +// Rustan Leino +// Original version: 7 November 2008 +// Version with proof divided into stages: June 2012. +// Copyright (c) 2008-2012 Microsoft. + +ghost module M0 { + // In this module, we declare the Node class, the definition of Reachability, and the specification + // and implementation of the Schorr-Waite algorithm. + + class Node { + var children: seq; + var marked: bool; + var childrenVisited: nat; + } + + datatype Path = Empty | Extend(Path, Node); + + function Reachable(source: Node, sink: Node, S: set): bool + requires null !in S; + reads S; + { + exists via: Path :: ReachableVia(source, via, sink, S) + } + + function ReachableVia(source: Node, p: Path, sink: Node, S: set): bool + requires null !in S; + reads S; + decreases p; + { + match p + case Empty => source == sink + case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S) + } + + method SchorrWaite(root: Node, ghost S: set) + requires root in S; + // S is closed under 'children': + requires forall n :: n in S ==> n != null && + forall ch :: ch in n.children ==> ch == null || ch in S; + // the graph starts off with nothing marked and nothing being indicated as currently being visited: + requires forall n :: n in S ==> !n.marked && n.childrenVisited == 0; + modifies S; + // nodes reachable from 'root' are marked: + ensures root.marked; + ensures forall n :: n in S && n.marked ==> + forall ch :: ch in n.children && ch != null ==> ch.marked; + // every marked node was reachable from 'root' in the pre-state: + ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S)); + // the structure of the graph has not changed: + ensures forall n :: n in S ==> + n.childrenVisited == old(n.childrenVisited) && + n.children == old(n.children); + { + root.marked := true; + var t, p := root, null; + ghost var stackNodes := []; + while (true) + // stackNodes is a sequence of nodes from S: + invariant forall n :: n in stackNodes ==> n in S; + + // The current node, t, is not included in stackNodes. Rather, t is just above the top of stackNodes. + // We say that the stack stackNodes+[t] are the "active" nodes. + invariant t in S && t !in stackNodes; + + // p points to the parent of the current node, that is, the node through which t was encountered in the + // depth-first traversal. This amounts to being the top of stackNodes, or null if stackNodes is empty. + // Note, it may seem like the variable p is redundant, since it holds a value that can be computed + // from stackNodes. But note that stackNodes is a ghost variable and won't be present at run + // time, where p is a physical variable that will be present at run time. + invariant p == if |stackNodes| == 0 then null else stackNodes[|stackNodes|-1]; + + // The .childrenVisited field is the extra information that the Schorr-Waite algorithm needs. It + // is used only for the active nodes, where it keeps track of how many of a node's children have been + // processed. For the nodes on stackNodes, .childrenVisited is less than the number of children, so + // it is an index of a child. For t, .childrenVisited may be as large as all of the children, which + // indicates that the node is ready to be popped off the stack of active nodes. For all other nodes, + // .childrenVisited is the original value, which is 0. + invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|; + invariant t.childrenVisited <= |t.children|; + invariant forall n :: n in S && n !in stackNodes && n != t ==> n.childrenVisited == 0; + + // To represent the stackNodes, the algorithm reverses children pointers. It never changes the number + // of children a node has. The only nodes with children pointers different than the original values are + // the nodes on stackNodes; moreover, only the index of the currently active child of a node is different. + invariant forall n :: n in stackNodes ==> + |n.children| == old(|n.children|) && + forall j :: 0 <= j < |n.children| ==> j == n.childrenVisited || n.children[j] == old(n.children[j]); + invariant forall n :: n in S && n !in stackNodes ==> n.children == old(n.children); + + // The children pointers that have been changed form a stack. That is, the active child of stackNodes[k] + // points to stackNodes[k-1], with the end case pointing to null. + invariant 0 < |stackNodes| ==> + stackNodes[0].children[stackNodes[0].childrenVisited] == null; + invariant forall k :: 0 < k < |stackNodes| ==> + stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1]; + // We also need to keep track of what the original values of the children pointers had been. Here, we + // have that the active child of stackNodes[k] used to be stackNodes[k+1], with the end case pointing + // to t. + invariant forall k :: 0 <= k < |stackNodes|-1 ==> + old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1]; + invariant 0 < |stackNodes| ==> + old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t; + + decreases *; // leave termination checking for a later refinement + { + if (t.childrenVisited == |t.children|) { + // pop + t.childrenVisited := 0; + if (p == null) { break; } + + t, p, p.children := p, p.children[p.childrenVisited], p.children[p.childrenVisited := t]; + stackNodes := stackNodes[..|stackNodes| - 1]; + t.childrenVisited := t.childrenVisited + 1; + + } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) { + // just advance to next child + t.childrenVisited := t.childrenVisited + 1; + + } else { + // push + stackNodes := stackNodes + [t]; + t, p, t.children := t.children[t.childrenVisited], t, t.children[t.childrenVisited := p]; + t.marked := true; + + // To prove that this "if" branch maintains the invariant "t !in stackNodes" will require + // some more properties about the loop. Therefore, we just assume the property here and + // prove it in a separate refinement. + assume t !in stackNodes; + } + } + // From the loop invariant, it now follows that all children pointers have been restored, + // and so have all .childrenVisited fields. Thus, the last postcondition (the one that says + // the structure of the graph has not been changed) has been established. + // Eventually, we also need to prove that exactly the right nodes have been marked, + // but let's just assume those properties for now and prove them in later refinements: + assume root.marked && forall n :: n in S && n.marked ==> + forall ch :: ch in n.children && ch != null ==> ch.marked; + assume forall n :: n in S && n.marked ==> old(Reachable(root, n, S)); + } +} + +ghost module M1 refines M0 { + // In this superposition, we start reasoning about the marks. In particular, we prove that the method + // marks all reachable nodes. + method SchorrWaite... + { + ...; + while ... + // The loop keeps marking nodes: The root is always marked. All children of any marked non-active + // node are marked. Active nodes are marked, and the first .childrenVisited of every active node + // are marked. + invariant root.marked; + invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==> + forall ch :: ch in n.children && ch != null ==> ch.marked; + invariant forall n :: n in stackNodes || n == t ==> + n.marked && + forall j :: 0 <= j < n.childrenVisited ==> n.children[j] == null || n.children[j].marked; + + decreases *; // keep postponing termination checking + { + if ... { // pop + } else if ... { // next child + } else { // push + ...; + // With the new loop invariants, we know that all active nodes are marked. Since the new value + // of "t" was not marked at the beginning of this iteration, we can now prove that the invariant + // "t !in stackNodes" is maintained, so we'll refine the assume from above with an assert. + assert ...; + } + } + // The new loop invariants give us a lower bound on which nodes are marked. Hence, we can now + // discharge the "everything reachable is marked" postcondition, whose proof we postponed above + // by supplying an assume statement. Here, we refine that assume statement into an assert. + assert ...; + } +} + +ghost module M2 refines M1 { + // In this superposition, we prove that only reachable nodes are marked. Essentially, we want + // to add a loop invariant that says t is reachable from root, because then the loop invariant + // that marked nodes are reachable follows. More precisely, we need to say that the node + // referenced by t is *in the initial state* reachable from root--because as we change + // children pointers during the course of the algorithm, what is reachable at some point in + // time may be different from what was reachable initially. + + // To do our proof, which involves establishing reachability between various nodes, we need + // some additional bookkeeping. In particular, we keep track of the path from root to t, + // and we associate with every marked node the path to it from root. The former is easily + // maintained in a local ghost variable; the latter is most easily represented as a ghost + // field in each node (an alternative would be to have a local variable that is a map from + // nodes to paths). So, we add a field declaration to the Node class: + class Node { + ghost var pathFromRoot: Path; + } + + method SchorrWaite... + { + ghost var path := Path.Empty; + root.pathFromRoot := path; + ...; + while ... + // There's a subtle complication when we speak of old(ReachableVia(... P ...)) for a path + // P. The expression old(...) says to evaluate the expression "..." in the pre-state of + // the method. So, old(ReachableVia(...)) says to evaluate ReachableVia(...) in the pre- + // state of the method. But in order for the "old(...)" expression to be well-formed, + // the subexpressions of the "..." must only refer to values that existed in the pre-state + // of the method. This incurs the proof obligation that any objects referenced by the + // parameters of ReachableVia(...) must have been allocated in the pre-state of the + // method. The proof obligation is easy to establish for root, t, and S (since root and + // S were given as in-parameters to the method, and we have "t in S"). But what about + // the path argument to ReachableVia? Since datatype values of type Path contain object + // references, we need to make sure we can deal with the proof obligation for the path + // argument. For this reason, we add invariants that say that "path" and the .pathFromRoot + // field of all marked nodes contain values that make sense in the pre-state. + invariant old(allocated(path)) && old(ReachableVia(root, path, t, S)); + invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot; + old(allocated(pth)) && old(ReachableVia(root, pth, n, S)); + invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S)); + + decreases *; // keep postponing termination checking + { + if ... { + // pop + ...; + path := t.pathFromRoot; + } else if ... { + // advance to next child + } else { + // push + path := Path.Extend(path, t); + ...; + t.pathFromRoot := path; + } + } + // In M0 above, we placed two assume statements here. In M1, we refined the first of these + // into an assert. We repeat that assert here: + assert ...; + // And now we we refine the second assume into an assert, proving that only reachable nodes + // have been marked. + assert ...; + } +} + +module M3 refines M2 { + // In this final superposition, we prove termination of the loop. + method SchorrWaite... + { + // The loop variant is a lexicographic triple, consisting of (0) the set of unmarked + // nodes, (1) the (length of the) stackNodes sequence, and (2) the number children of + // the current node that are still to be investigated. We introduce a ghost variable + // to keep track of the set of unmarked nodes. + ghost var unmarkedNodes := S - {root}; + ...; + while ... + invariant forall n :: n in S && !n.marked ==> n in unmarkedNodes; + decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited; + { + if ... { // pop + } else if ... { // next child + } else { // push + ...; + unmarkedNodes := unmarkedNodes - {t}; + } + } + } +} diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index d098d753..fa7f7c70 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -11,7 +11,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy - SchorrWaite.dfy + SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy -- cgit v1.2.3 From 7c6cfaa37c96349fda99823c6f98a576dba194b4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 21 Jun 2012 19:16:05 -0700 Subject: Dafny: Since it's no longer true that all types support equality at run-time (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation. --- Dafny/Dafny.atg | 17 +- Dafny/DafnyAst.cs | 151 +++++++-- Dafny/Parser.cs | 571 ++++++++++++++++++---------------- Dafny/Printer.cs | 6 + Dafny/RefinementTransformer.cs | 4 +- Dafny/Resolver.cs | 456 +++++++++++++++++++++++---- Dafny/Scanner.cs | 130 ++++---- Test/VSI-Benchmarks/b4.dfy | 2 +- Test/VSI-Benchmarks/b8.dfy | 2 +- Test/dafny0/SmallTests.dfy | 2 +- Test/dafny0/TypeParameters.dfy | 4 +- Test/dafny1/Celebrity.dfy | 2 +- Test/dafny1/UltraFilter.dfy | 2 +- Test/dafny2/MajorityVote.dfy | 12 +- Test/vstte2012/BreadthFirstSearch.dfy | 2 +- 15 files changed, 916 insertions(+), 447 deletions(-) (limited to 'Test/dafny1') diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 66756b0c..3000d348 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -290,10 +290,13 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> ArbitraryTypeDecl = (. IToken/*!*/ id; Attributes attrs = null; + var eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) "type" { Attribute } - Ident (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .) + Ident + [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) + ] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .) SYNC ";" . GIdentType @@ -356,10 +359,16 @@ TypeIdentOptional/*!*/ typeArgs.> = (. Contract.Requires(cce.NonNullElements(typeArgs)); - IToken/*!*/ id; .) + IToken/*!*/ id; + TypeParameter.EqualitySupportValue eqSupport; + .) "<" - Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .) - { "," Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .) + Ident (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) + [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) + ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .) + { "," Ident (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) + [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) + ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .) } ">" . diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 5e6ad5c3..6da3138c 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -268,9 +268,19 @@ namespace Microsoft.Dafny { } } public bool IsTypeParameter { + get { + return AsTypeParameter != null; + } + } + public TypeParameter AsTypeParameter { get { UserDefinedType ct = this as UserDefinedType; - return ct != null && ct.ResolvedParam != null; + return ct == null ? null : ct.ResolvedParam; + } + } + public virtual bool SupportsEquality { + get { + return true; } } } @@ -318,16 +328,20 @@ namespace Microsoft.Dafny { public abstract class CollectionType : NonProxyType { - public readonly Type Arg; + public readonly Type Arg; // denotes the Domain type for a Map [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Arg != null); } - public CollectionType(Type arg) { Contract.Requires(arg != null); this.Arg = arg; } + public override bool SupportsEquality { + get { + return Arg.SupportsEquality; + } + } } public class SetType : CollectionType { @@ -369,12 +383,14 @@ namespace Microsoft.Dafny { } public class MapType : CollectionType { - public Type Domain, Range; + public Type Range; public MapType(Type domain, Type range) : base(domain) { Contract.Requires(domain != null && range != null); - Domain = domain; Range = range; } + public Type Domain { + get { return Arg; } + } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); @@ -515,6 +531,23 @@ namespace Microsoft.Dafny { } return s; } + + public override bool SupportsEquality { + get { + if (ResolvedClass is ClassDecl) { + return true; + } else if (ResolvedClass is CoDatatypeDecl) { + return false; + } else if (ResolvedClass is IndDatatypeDecl) { + // TODO + return true; + } else if (ResolvedParam != null) { + return ResolvedParam.MustSupportEquality; + } + Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved + return true; + } + } } public abstract class TypeProxy : Type { @@ -529,6 +562,15 @@ namespace Microsoft.Dafny { Contract.Assume(T == null || cce.IsPeerConsistent(T)); return T == null ? "?" : T.ToString(); } + public override bool SupportsEquality { + get { + if (T != null) { + return T.SupportsEquality; + } else { + return base.SupportsEquality; + } + } + } } public abstract class UnrestrictedTypeProxy : TypeProxy { @@ -588,17 +630,6 @@ namespace Microsoft.Dafny { } } - /// - /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type. - /// - public class ObjectsTypeProxy : RestrictedTypeProxy { - public override int OrderID { - get { - return 2; - } - } - } - /// /// This proxy stands for: /// set(Arg) or seq(Arg) or map(Arg, Range) @@ -616,7 +647,7 @@ namespace Microsoft.Dafny { } public override int OrderID { get { - return 3; + return 2; } } } @@ -635,7 +666,7 @@ namespace Microsoft.Dafny { } public override int OrderID { get { - return 4; + return 3; } } } @@ -658,7 +689,7 @@ namespace Microsoft.Dafny { } public override int OrderID { get { - return 5; + return 4; } } } @@ -723,10 +754,17 @@ namespace Microsoft.Dafny { parent = value; } } - public TypeParameter(IToken tok, string name) + public enum EqualitySupportValue { Required, InferredRequired, Unspecified } + public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required) + public bool MustSupportEquality { + get { return EqualitySupport != EqualitySupportValue.Unspecified; } + } + + public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified) : base(tok, name, null) { Contract.Requires(tok != null); Contract.Requires(name != null); + EqualitySupport = equalitySupport; } } @@ -953,13 +991,15 @@ namespace Microsoft.Dafny { public abstract class MemberDecl : Declaration { public readonly bool IsStatic; + public readonly bool IsGhost; public TopLevelDecl EnclosingClass; // filled in during resolution - public MemberDecl(IToken tok, string name, bool isStatic, Attributes attributes) + public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); IsStatic = isStatic; + IsGhost = isGhost; } /// /// Returns className+"."+memberName. Available only after resolution. @@ -983,7 +1023,6 @@ namespace Microsoft.Dafny { } public class Field : MemberDecl { - public readonly bool IsGhost; public readonly bool IsMutable; public readonly Type Type; [ContractInvariantMethod] @@ -999,11 +1038,10 @@ namespace Microsoft.Dafny { } public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes) - : base(tok, name, false, attributes) { + : base(tok, name, false, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); - IsGhost = isGhost; IsMutable = isMutable; Type = type; } @@ -1043,17 +1081,23 @@ namespace Microsoft.Dafny { public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType { public readonly TypeParameter TheType; + public TypeParameter.EqualitySupportValue EqualitySupport { + get { return TheType.EqualitySupport; } + } + public bool MustSupportEquality { + get { return TheType.MustSupportEquality; } + } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(TheType != null && Name == TheType.Name); } - public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes) + public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes) : base(tok, name, module, new List(), attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); - TheType = new TypeParameter(tok, name); + TheType = new TypeParameter(tok, name, equalitySupport); } } @@ -1274,7 +1318,6 @@ namespace Microsoft.Dafny { } public class Function : MemberDecl, TypeParameter.ParentType { - public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method" public bool IsRecursive; // filled in during resolution public readonly List/*!*/ TypeArgs; public readonly IToken OpenParen; // can be null (for predicates), if there are no formals @@ -1297,11 +1340,14 @@ namespace Microsoft.Dafny { Contract.Invariant(Decreases != null); } + /// + /// Note, functions are "ghost" by default; a non-ghost function is called a "function method". + /// public Function(IToken tok, string name, bool isStatic, bool isGhost, List typeArgs, IToken openParen, List formals, Type resultType, List req, List reads, List ens, Specification decreases, Expression body, Attributes attributes, bool signatureOmitted) - : base(tok, name, isStatic, attributes) { + : base(tok, name, isStatic, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -1312,7 +1358,6 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); - this.IsGhost = isGhost; this.TypeArgs = typeArgs; this.OpenParen = openParen; this.Formals = formals; @@ -1341,7 +1386,6 @@ namespace Microsoft.Dafny { public class Method : MemberDecl, TypeParameter.ParentType { - public readonly bool IsGhost; public readonly bool SignatureIsOmitted; public readonly List/*!*/ TypeArgs; public readonly List/*!*/ Ins; @@ -1372,7 +1416,7 @@ namespace Microsoft.Dafny { [Captured] Specification/*!*/ decreases, [Captured] BlockStmt body, Attributes attributes, bool signatureOmitted) - : base(tok, name, isStatic, attributes) { + : base(tok, name, isStatic, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -1382,7 +1426,6 @@ namespace Microsoft.Dafny { Contract.Requires(mod != null); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); - this.IsGhost = isGhost; this.TypeArgs = typeArgs; this.Ins = ins; this.Outs = outs; @@ -1640,6 +1683,18 @@ namespace Microsoft.Dafny { Attributes = attrs; } public abstract bool CanAffectPreviouslyKnownExpressions { get; } + /// + /// Returns the non-null subexpressions of the AssignmentRhs. + /// + public virtual IEnumerable SubExpressions { + get { yield break; } + } + /// + /// Returns the non-null sub-statements of the AssignmentRhs. + /// + public virtual IEnumerable SubStatements{ + get { yield break; } + } } public class ExprRhs : AssignmentRhs @@ -1657,6 +1712,11 @@ namespace Microsoft.Dafny { Expr = expr; } public override bool CanAffectPreviouslyKnownExpressions { get { return false; } } + public override IEnumerable SubExpressions { + get { + yield return Expr; + } + } } public class TypeRhs : AssignmentRhs @@ -1705,6 +1765,23 @@ namespace Microsoft.Dafny { return false; } } + + public override IEnumerable SubExpressions { + get { + if (ArrayDimensions != null) { + foreach (var e in ArrayDimensions) { + yield return e; + } + } + } + } + public override IEnumerable SubStatements { + get { + if (InitCall != null) { + yield return InitCall; + } + } + } } public class CallRhs : AssignmentRhs @@ -1744,6 +1821,14 @@ namespace Microsoft.Dafny { return false; } } + public override IEnumerable SubExpressions { + get { + yield return Receiver; + foreach (var e in Args) { + yield return e; + } + } + } } public class HavocRhs : AssignmentRhs { @@ -1980,6 +2065,7 @@ namespace Microsoft.Dafny { public Expression/*!*/ Receiver; public readonly string/*!*/ MethodName; public readonly List/*!*/ Args; + public Dictionary TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done) public Method Method; // filled in by resolution public CallStmt(IToken tok, List/*!*/ lhs, Expression/*!*/ receiver, @@ -2785,6 +2871,7 @@ namespace Microsoft.Dafny { public readonly Expression/*!*/ Receiver; public readonly IToken OpenParen; // can be null if Args.Count == 0 public readonly List/*!*/ Args; + public Dictionary TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done) public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded } public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 26b98833..0c1920a6 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -315,7 +315,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 22) { + if (la.kind == 25) { GenericParameters(typeArgs); } Expect(6); @@ -351,7 +351,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 22) { + if (la.kind == 25) { GenericParameters(typeArgs); } Expect(16); @@ -376,13 +376,20 @@ bool IsAttribute() { void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) { IToken/*!*/ id; Attributes attrs = null; + var eqSupport = TypeParameter.EqualitySupportValue.Unspecified; Expect(21); while (la.kind == 6) { Attribute(ref attrs); } Ident(out id); - at = new ArbitraryTypeDecl(id, id.val, module, attrs); + if (la.kind == 22) { + Get(); + Expect(23); + Expect(24); + eqSupport = TypeParameter.EqualitySupportValue.Required; + } + at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();} Expect(18); } @@ -405,10 +412,10 @@ bool IsAttribute() { } if (la.kind == 19) { FieldDecl(mmod, mm); - } else if (la.kind == 44 || la.kind == 45) { + } else if (la.kind == 45 || la.kind == 46) { FunctionDecl(mmod, out f); mm.Add(f); - } else if (la.kind == 24 || la.kind == 25) { + } else if (la.kind == 27 || la.kind == 28) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); } else SynErr(114); @@ -416,16 +423,32 @@ bool IsAttribute() { void GenericParameters(List/*!*/ typeArgs) { Contract.Requires(cce.NonNullElements(typeArgs)); - IToken/*!*/ id; - Expect(22); + IToken/*!*/ id; + TypeParameter.EqualitySupportValue eqSupport; + + Expect(25); Ident(out id); - typeArgs.Add(new TypeParameter(id, id.val)); + eqSupport = TypeParameter.EqualitySupportValue.Unspecified; + if (la.kind == 22) { + Get(); + Expect(23); + Expect(24); + eqSupport = TypeParameter.EqualitySupportValue.Required; + } + typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); while (la.kind == 20) { Get(); Ident(out id); - typeArgs.Add(new TypeParameter(id, id.val)); + eqSupport = TypeParameter.EqualitySupportValue.Unspecified; + if (la.kind == 22) { + Get(); + Expect(23); + Expect(24); + eqSupport = TypeParameter.EqualitySupportValue.Required; + } + typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); } - Expect(23); + Expect(26); } void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { @@ -470,9 +493,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken; bool signatureOmitted = false; - if (la.kind == 44) { + if (la.kind == 45) { Get(); - if (la.kind == 24) { + if (la.kind == 27) { Get(); isFunctionMethod = true; } @@ -482,22 +505,22 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 22 || la.kind == 33) { - if (la.kind == 22) { + if (la.kind == 22 || la.kind == 25) { + if (la.kind == 25) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals, out openParen); Expect(5); Type(out returnType); - } else if (la.kind == 27) { + } else if (la.kind == 30) { Get(); signatureOmitted = true; openParen = Token.NoToken; } else SynErr(117); - } else if (la.kind == 45) { + } else if (la.kind == 46) { Get(); isPredicate = true; - if (la.kind == 24) { + if (la.kind == 27) { Get(); isFunctionMethod = true; } @@ -508,17 +531,17 @@ bool IsAttribute() { } Ident(out id); if (StartOf(4)) { - if (la.kind == 22) { + if (la.kind == 25) { GenericParameters(typeArgs); } - if (la.kind == 33) { + if (la.kind == 22) { Formals(true, isFunctionMethod, formals, out openParen); if (la.kind == 5) { Get(); SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } } - } else if (la.kind == 27) { + } else if (la.kind == 30) { Get(); signatureOmitted = true; openParen = Token.NoToken; @@ -562,10 +585,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();} - if (la.kind == 24) { + while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(120); Get();} + if (la.kind == 27) { Get(); - } else if (la.kind == 25) { + } else if (la.kind == 28) { Get(); if (allowConstructor) { isConstructor = true; @@ -587,17 +610,17 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 22 || la.kind == 33) { - if (la.kind == 22) { + if (la.kind == 22 || la.kind == 25) { + if (la.kind == 25) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins, out openParen); - if (la.kind == 26) { + if (la.kind == 29) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs, out openParen); } - } else if (la.kind == 27) { + } else if (la.kind == 30) { Get(); signatureOmitted = true; openParen = Token.NoToken; } else SynErr(122); @@ -629,7 +652,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 33) { + if (la.kind == 22) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -637,7 +660,7 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(33); + Expect(22); if (StartOf(7)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); @@ -647,7 +670,7 @@ bool IsAttribute() { formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(34); + Expect(24); } void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) { @@ -731,22 +754,22 @@ bool IsAttribute() { List/*!*/ gt; switch (la.kind) { - case 35: { + case 36: { Get(); tok = t; break; } - case 36: { + case 37: { Get(); tok = t; ty = new NatType(); break; } - case 37: { + case 38: { Get(); tok = t; ty = new IntType(); break; } - case 38: { + case 39: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -757,7 +780,7 @@ bool IsAttribute() { break; } - case 39: { + case 40: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -768,7 +791,7 @@ bool IsAttribute() { break; } - case 40: { + case 41: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -779,7 +802,7 @@ bool IsAttribute() { break; } - case 41: { + case 42: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -790,7 +813,7 @@ bool IsAttribute() { break; } - case 1: case 3: case 42: { + case 1: case 3: case 43: { ReferenceType(out tok, out ty); break; } @@ -800,7 +823,7 @@ bool IsAttribute() { void Formals(bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; - Expect(33); + Expect(22); openParen = t; if (la.kind == 1 || la.kind == 8) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); @@ -811,7 +834,7 @@ bool IsAttribute() { formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(34); + Expect(24); } void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens, @@ -820,7 +843,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; while (!(StartOf(8))) {SynErr(124); Get();} - if (la.kind == 28) { + if (la.kind == 31) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -836,18 +859,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();} Expect(18); - } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { - if (la.kind == 29) { + } else if (la.kind == 32 || la.kind == 33 || la.kind == 34) { + if (la.kind == 32) { Get(); isFree = true; } - if (la.kind == 30) { + if (la.kind == 33) { Get(); Expression(out e); while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} Expect(18); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 31) { + } else if (la.kind == 34) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -857,7 +880,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else SynErr(128); - } else if (la.kind == 32) { + } else if (la.kind == 35) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); @@ -885,7 +908,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; Expression(out e); - if (la.kind == 48) { + if (la.kind == 49) { Get(); Ident(out id); fieldName = id.val; @@ -920,7 +943,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(22); + Expect(25); Type(out ty); gt.Add(ty); while (la.kind == 20) { @@ -928,7 +951,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Type(out ty); gt.Add(ty); } - Expect(23); + Expect(26); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -937,7 +960,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken moduleName = null; List/*!*/ gt; - if (la.kind == 42) { + if (la.kind == 43) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -956,12 +979,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) { Ident(out tok); gt = new List(); - if (la.kind == 43) { + if (la.kind == 44) { moduleName = tok; Get(); Ident(out tok); } - if (la.kind == 22) { + if (la.kind == 25) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, moduleName); @@ -971,14 +994,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - if (la.kind == 30) { - while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();} + if (la.kind == 33) { + while (!(la.kind == 0 || la.kind == 33)) {SynErr(132); Get();} Get(); Expression(out e); while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();} Expect(18); reqs.Add(e); - } else if (la.kind == 46) { + } else if (la.kind == 47) { Get(); if (StartOf(11)) { PossiblyWildFrameExpression(out fe); @@ -991,13 +1014,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();} Expect(18); - } else if (la.kind == 31) { + } else if (la.kind == 34) { Get(); Expression(out e); while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();} Expect(18); ens.Add(e); - } else if (la.kind == 32) { + } else if (la.kind == 35) { Get(); DecreasesList(decreases, false); while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();} @@ -1016,7 +1039,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 47) { + if (la.kind == 48) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(9)) { @@ -1027,7 +1050,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 47) { + if (la.kind == 48) { Get(); e = new WildcardExpr(t); } else if (StartOf(9)) { @@ -1056,19 +1079,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = bs; break; } - case 66: { + case 67: { AssertStmt(out s); break; } - case 54: { + case 55: { AssumeStmt(out s); break; } - case 67: { + case 68: { PrintStmt(out s); break; } - case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { + case 1: case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { UpdateStmt(out s); break; } @@ -1076,23 +1099,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s); break; } - case 59: { + case 60: { IfStmt(out s); break; } - case 63: { + case 64: { WhileStmt(out s); break; } - case 65: { + case 66: { MatchStmt(out s); break; } - case 68: { + case 69: { ParallelStmt(out s); break; } - case 49: { + case 50: { Get(); x = t; Ident(out id); @@ -1101,14 +1124,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList