From 5cf9650688fab9e5b04a60d94724de0287780217 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Sat, 19 Jun 2010 21:00:58 +0000 Subject: Dafny: * Improved design and implementation of SplitExpr * Fixed some tests in dafny0/Use.dfy * Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms --- Test/dafny0/Answer | 17 ++++++++++---- Test/dafny0/SplitExpr.dfy | 56 +++++++++++++++++++++++++++++++++++++++++++++ Test/dafny0/Termination.dfy | 19 +++++++++++++++ Test/dafny0/Use.dfy | 37 +++++++++++++++++------------- Test/dafny0/runtest.bat | 2 +- 5 files changed, 109 insertions(+), 22 deletions(-) create mode 100644 Test/dafny0/SplitExpr.dfy (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7456ffaa..34b15b8a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -372,7 +372,7 @@ Execution trace: Termination.dfy(119,16): anon9_Else (0,0): anon5 -Dafny program verifier finished with 22 verified, 4 errors +Dafny program verifier finished with 23 verified, 4 errors -------------------- Use.dfy -------------------- Use.dfy(16,18): Error: assertion violation @@ -393,17 +393,20 @@ Execution trace: Use.dfy(126,23): Error: assertion violation Execution trace: (0,0): anon0 -Use.dfy(138,5): Error: assertion violation +Use.dfy(143,5): Error: assertion violation Execution trace: (0,0): anon0 -Use.dfy(138,5): Error: assertion violation +Use.dfy(143,5): Error: assertion violation Execution trace: (0,0): anon0 -Use.dfy(208,19): Error: assertion violation +Use.dfy(143,5): Error: assertion violation +Execution trace: + (0,0): anon0 +Use.dfy(213,19): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 39 verified, 9 errors +Dafny program verifier finished with 39 verified, 10 errors -------------------- DTypes.dfy -------------------- DTypes.dfy(15,14): Error: assertion violation @@ -440,3 +443,7 @@ Dafny program verifier finished with 27 verified, 4 errors -------------------- Datatypes.dfy -------------------- Dafny program verifier finished with 10 verified, 0 errors + +-------------------- SplitExpr.dfy -------------------- + +Dafny program verifier finished with 5 verified, 0 errors diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy new file mode 100644 index 00000000..80b67c10 --- /dev/null +++ b/Test/dafny0/SplitExpr.dfy @@ -0,0 +1,56 @@ +class UnboundedStack { + var top: Node; + ghost var footprint: set; + ghost var content: seq; + + function IsUnboundedStack(): bool + reads {this} + footprint; + { + this in footprint && + (top == null ==> content == []) && + (top != null ==> top in footprint && top.footprint <= footprint && + top.prev == null && content == top.content && top.Valid()) + } + + function IsEmpty(): bool + reads {this}; + { content == [] } + + method Pop() returns (result: T) + requires IsUnboundedStack() && !IsEmpty(); + modifies footprint; + ensures IsUnboundedStack() && content == old(content)[1..]; + { + result := top.val; + // The following assert does the trick, because it gets inlined and thus + // exposes top.next.Valid() (if top.next != null): + footprint := footprint - top.footprint; top := top.next; + // In a previous version of the implementation of the SplitExpr transformation, the + // following assert did not have the intended effect of being used as a lemma: + assert top != null ==> top.Valid(); + if (top != null) { + footprint := footprint + top.footprint; top.prev := null; + } + content := content[1..]; +} } + +class Node { + var val: T; + var next: Node; + var prev: Node; + var footprint: set>; + var content: seq; + + function Valid(): bool + reads this, footprint; + { + this in footprint && !(null in footprint) && + (next == null ==> content == [val]) && + (next != null ==> next in footprint && + next.footprint < footprint && + !(this in next.footprint) && + next.prev == this && + content == [val] + next.content && + next.Valid()) + } +} diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 27004653..974dadab 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -151,3 +151,22 @@ method FailureToProveTermination5(b: bool, N: int) n := n + 1; } } + +class Node { + var next: Node; + var footprint: set; + + function Valid(): bool + reads this, footprint; + // In a previous (and weaker) axiomatization of sets, there had been two problems + // with trying to prove the termination of this function. First, the default + // decreases clause (derived from the reads clause) had been done incorrectly for + // a list of expressions. Second, the set axiomatization had not been strong enough. + { + this in footprint && !(null in footprint) && + (next != null ==> next in footprint && + next.footprint < footprint && + this !in next.footprint && + next.Valid()) + } +} diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy index 20928f41..7a963382 100644 --- a/Test/dafny0/Use.dfy +++ b/Test/dafny0/Use.dfy @@ -128,50 +128,55 @@ class T { } function K(): bool - reads this; decreases false; + reads this; decreases 0; { - x <= 100 || (1 < 0 && KK()) + x <= 100 || (1 < 0 && KKK()) } - unlimited function KK(): bool - reads this; decreases true; + function KK(): bool + reads this; decreases 1; { K() } + unlimited function KKK(): bool + reads this; decreases 2; + { + KK() + } method R0() - requires KK(); + requires KKK(); // this expands to both KKK() and KK(); the def. of KK() expands to K#limited modifies this; { x := x - 1; - assert KK(); // error (does not know exact definition of K from the initial state) + assert KKK(); // error (does not know exact definition of K from the initial state) } method R1() - requires KK(); + requires KKK(); // this expands to both KKK() and KK(); the def. of KK() expands to K#limited modifies this; { - use K(); // KK in the precondition and KK's definition give K#limited, which this use expands + use K(); // this equates K#limited and K, so the exact value of K() in the pre-state is now known x := x - 1; - assert KK(); // the assert expands KK to K, definition of K expands K + assert KKK(); // error: the assert expands KKK to KK, definition of KK expands K#limited (but not to K) } method R2() - requires KK(); + requires KKK(); // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K) modifies this; { x := x - 1; - use K(); - assert KK(); // error (does not know exact definition of K in the pre-state) + use K(); // this equates K#limited and K in the present state + assert KKK(); // error: the connection with the pre-state K is not known } method R3() - requires KK(); + requires KKK(); // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K) modifies this; { - use K(); + use K(); // this equates K#limited and K, so the pre-state K() is known x := x - 1; - use K(); - assert KK(); // thar it is + use K(); // this equates K#limited and K in the present state + assert KKK(); // thar it is: this expands to both KKK and KK, and the def. of KK expands to K#limited } } diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index aa45ca05..0e8146c0 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do ( for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy Modules0.dfy Modules1.dfy BadFunction.dfy Termination.dfy Use.dfy DTypes.dfy - TypeParameters.dfy Datatypes.dfy) do ( + TypeParameters.dfy Datatypes.dfy SplitExpr.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 %* %%f -- cgit v1.2.3