diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
| commit | c8452b274087624140cb7f2424b321de54fcb41a (patch) | |
| tree | 6dd73ee0dc98d9c6997e39b6e109a1d5e4c02a74 /Test/dafny0/ParallelResolveErrors.dfy | |
| parent | e7bf7ffb17f0c4022c3df81b4fe33df440723c37 (diff) | |
Dafny induction:
* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)
Diffstat (limited to 'Test/dafny0/ParallelResolveErrors.dfy')
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 4e0be32e..9afa311a 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -85,3 +85,67 @@ method M1() { }
}
}
+
+// -------------------------------------------------------------------------------------
+// Some soundness considerations
+// -------------------------------------------------------------------------------------
+
+ghost static method X_M0(y: int)
+ ensures exists o: object :: o != null && fresh(o); // error: not allowed 'fresh' here
+{
+ var p := new object;
+}
+
+class X_C { ghost var data: int; }
+ghost static method X_M1(y: int)
+ ensures exists c: X_C :: c != null && c.data != old(c.data); // error: not allowed 'old' here
+{
+ var c := new X_C;
+ c.data := c.data + 1;
+}
+
+method X_Main() {
+ if (*) {
+ parallel (x) { X_M0(x); }
+ } else {
+ parallel (x) { X_M1(x); }
+ }
+ assert false;
+}
+
+
+// The following seems to be a legitimate use of a two-state predicate in the postcondition of the parallel statement
+method X_Legit(c: X_C)
+ requires c != null;
+ modifies c;
+{
+ c.data := c.data + 1;
+ parallel (x | c.data <= x)
+ ensures old(c.data) < x; // error: not allowed 'old' here
+ {
+ }
+}
+
+// X_M2 is like X_M0, but with an out-parameter
+ghost static method X_M2(y: int) returns (r: int)
+ ensures exists o: object :: o != null && fresh(o); // 'fresh' is allowed here (because there's something coming "out" of this ghost method, namely 'r'
+{
+ var p := new object;
+}
+
+// The following method exhibits a case where M2 and a two-state parallel ensures would lead to an unsoundness
+// with the current translation.
+method X_AnotherMain(c: X_C)
+ requires c != null;
+ modifies c;
+{
+ c.data := c.data + 1;
+ parallel (x: int)
+ ensures exists o: object :: o != null && fresh(o); // error: not allowed 'fresh' here
+ {
+ var s := X_M2(x);
+ }
+ assert false;
+}
+
+// -------------------------------------------------------------------------------------
|