From e51b347511f11ea1bda810b843e5d61fdf088832 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Sat, 5 Jun 2010 02:00:33 +0000 Subject: Dafny: * Fixed bug in translation of well-formedness conditions * Added Test/dafny0/Celebrity.dfy * Added a harness to Test/vacid0/Composite.dfy --- Source/Dafny/Translator.ssc | 3 +- Test/dafny0/Answer | 6 ++- Test/dafny0/Celebrity.dfy | 95 ++++++++++++++++++++++++++++++++++++++++++ Test/dafny0/TypeParameters.dfy | 16 +++++++ Test/dafny0/runtest.bat | 2 +- Test/vacid0/Answer | 2 +- Test/vacid0/Composite.dfy | 17 ++++++++ 7 files changed, 137 insertions(+), 4 deletions(-) create mode 100644 Test/dafny0/Celebrity.dfy diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index eea9d91b..092ee146 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1303,7 +1303,8 @@ namespace Microsoft.Dafny { substMap.Add(p, ie); locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type)))); Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(e.Args[i])); + Expression ee = e.Args[i]; + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), (!)ee.Type, p.Type)); builder.Add(cmd); } // check that the preconditions for the call hold diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 59582de8..e1b83c87 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -418,7 +418,7 @@ TypeParameters.dfy(63,27): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 20 verified, 2 errors +Dafny program verifier finished with 24 verified, 2 errors -------------------- Datatypes.dfy -------------------- @@ -443,3 +443,7 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- Tree.dfy -------------------- Dafny program verifier finished with 6 verified, 0 errors + +-------------------- Celebrity.dfy -------------------- + +Dafny program verifier finished with 11 verified, 0 errors diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny0/Celebrity.dfy new file mode 100644 index 00000000..fd267c71 --- /dev/null +++ b/Test/dafny0/Celebrity.dfy @@ -0,0 +1,95 @@ +// Celebrity example, inspired by the Rodin tutorial + +method Pick(S: set) returns (t: T); + requires S != {}; + ensures t in S; + +static function Knows(a: Person, b: Person): bool; + requires a != b; // forbid asking about the reflexive case + +static function IsCelebrity(c: Person, people: set): bool +{ + c in people && + (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)) +} + +method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) + requires (exists c :: IsCelebrity(c, people)); + ensures r == c; +{ + var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc + r := cc; +} + +method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) + requires IsCelebrity(c, people); + ensures r == c; +{ + var Q := people; + call x := Pick(Q); + while (Q != {x}) + //invariant Q <= people; // inv1 in Rodin's Celebrity_1, but it's not needed here + invariant IsCelebrity(c, Q); // inv2 + invariant x in Q; + decreases Q; + { + call y := Pick(Q - {x}); + if (Knows(x, y)) { + Q := Q - {x}; // remove_1 + } else { + Q := Q - {y}; assert x in Q; // remove_2 + } + call x := Pick(Q); + } + r := x; +} + +method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) + requires IsCelebrity(c, people); + ensures r == c; +{ + call b := Pick(people); + var R := people - {b}; + while (R != {}) + invariant R <= people; // inv1 + invariant b in people; // inv2 + invariant b !in R; // inv3 + invariant IsCelebrity(c, R + {b}); // my non-refinement way of saying inv4 + + decreases R; + { + call x := Pick(R); + if (Knows(x, b)) { + R := R - {x}; + } else { + b := x; + R := R - {x}; + } + } + r := b; +} + +method FindCelebrity3(n: int, people: set, ghost c: int) returns (r: int) + requires 0 < n; + requires (forall p :: p in people <==> 0 <= p && p < n); + // requires IsCelebrity(c, people); // see next line: + requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator + ensures r == c; +{ + r := 0; + var a := 1; + var b := 0; + while (a < n) + invariant a <= n; + invariant b < a; // Celebrity_2/inv3 and Celebrity_3/inv2 + invariant c == b || (a <= c && c < n); + { + if (Knows(a, b)) { + a := a + 1; + } else { + b := a; + a := a + 1; + } + } + r := b; +} diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 614c2185..e199a386 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -96,3 +96,19 @@ class CClient { assert z == c.x; } } + +// ------------------------- + +static function IsCelebrity(c: Person, people: set): bool; + requires c == c || c in people; + +method FindCelebrity3(people: set, ghost c: int) + requires IsCelebrity(c, people); +{ + ghost var b: bool; + b := IsCelebrity(c, people); + b := F(c, people); +} + +static function F(c: int, people: set): bool; + requires IsCelebrity(c, people); diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index c43ea782..eb7ea4f7 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -23,7 +23,7 @@ for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy - Tree.dfy) do ( + Tree.dfy Celebrity.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 %* %%f diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer index 6f270f92..90bbcc78 100644 --- a/Test/vacid0/Answer +++ b/Test/vacid0/Answer @@ -9,4 +9,4 @@ Dafny program verifier finished with 9 verified, 0 errors -------------------- Composite.dfy -------------------- -Dafny program verifier finished with 14 verified, 0 errors +Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index 28074c7b..ca5f206b 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -83,6 +83,7 @@ class Composite { ensures (forall c :: c in S ==> c.Valid(S)); ensures (forall c :: c in S ==> c.val == old(c.val)); ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent)); + ensures parent == null; ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null)); ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null)); ensures Acyclic({this}); @@ -158,3 +159,19 @@ method Main() call c2.Update(496, S); call c0.Update(0, S); } + +method Harness() { + var a := new Composite; call a.Init(5); + var b := new Composite; call b.Init(7); + call a.Add({a}, b, {b}); + assert a.sum == 12; + + call b.Update(17, {a,b}); + assert a.sum == 22; + + var c := new Composite; call c.Init(10); + call b.Add({a,b}, c, {c}); + call b.Dislodge({a,b,c}); + assert b.sum == 27; +} + -- cgit v1.2.3