From d1584d0b1f393c0e1514c0b85171fb5643c7889f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 18 Mar 2013 14:44:56 -0700 Subject: Added a coinductive/inductive Filter example to the test suite --- Test/dafny3/Answer | 4 + Test/dafny3/Filter.dfy | 259 +++++++++++++++++++++++++++++++++ Test/dafny3/InductionVsCoinduction.dfy | 6 +- Test/dafny3/runtest.bat | 2 +- 4 files changed, 267 insertions(+), 4 deletions(-) create mode 100644 Test/dafny3/Filter.dfy (limited to 'Test/dafny3') diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index fe3b762e..b258fe3d 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -42,3 +42,7 @@ Dafny program verifier finished with 13 verified, 0 errors -------------------- Paulson.dfy -------------------- Dafny program verifier finished with 28 verified, 0 errors + +-------------------- Filter.dfy -------------------- + +Dafny program verifier finished with 43 verified, 0 errors diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy new file mode 100644 index 00000000..d45f4acc --- /dev/null +++ b/Test/dafny3/Filter.dfy @@ -0,0 +1,259 @@ +codatatype Stream = Cons(head: T, tail: Stream); + +function Tail(s: Stream, n: nat): Stream +{ + if n == 0 then s else Tail(s.tail, n-1) +} +predicate In(x: T, s: Stream) +{ + exists n :: 0 <= n && Tail(s, n).head == x +} +copredicate IsSubStream(s: Stream, u: Stream) +{ + In(s.head, u) && IsSubStream(s.tail, u) +} + +ghost method Lemma_InTail(x: T, s: Stream) + requires In(x, s.tail); + ensures In(x, s); +{ + var n :| 0 <= n && Tail(s.tail, n).head == x; + assert Tail(s, n+1).head == x; +} +comethod Lemma_TailSubStream(s: Stream, u: Stream) + requires IsSubStream(s, u.tail); + ensures IsSubStream(s, u); +{ + Lemma_InTail(s.head, u); +} +ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat) // this lemma could have been used to prove the previous one + requires IsSubStream#[k](s, u.tail); + ensures IsSubStream#[k](s, u); +{ + if k != 0 { + Lemma_InTail(s.head, u); + Lemma_TailSubStreamK(s.tail, u, k-1); + } +} +ghost method Lemma_InSubStream(x: T, s: Stream, u: Stream) + requires In(x, s) && IsSubStream(s, u); + ensures In(x, u); +{ + var n :| 0 <= n && Tail(s, n).head == x; + var t := s; + while n != 0 + invariant 0 <= n; + invariant Tail(t, n).head == x; + invariant IsSubStream(t, u); + { + t, n := t.tail, n - 1; + } +} + +type PredicateHandle; +predicate P(x: T, h: PredicateHandle) + +copredicate AllP(s: Stream, h: PredicateHandle) +{ + P(s.head, h) && AllP(s.tail, h) +} +ghost method Lemma_InAllP(x: T, s: Stream, h: PredicateHandle) + requires In(x, s) && AllP(s, h); + ensures P(x, h); +{ + var n :| 0 <= n && Tail(s, n).head == x; + var t := s; + while n != 0 + invariant 0 <= n; + invariant Tail(t, n).head == x; + invariant AllP(t, h); + { + t, n := t.tail, n - 1; + } +} + +predicate IsAnother(s: Stream, h: PredicateHandle) +{ + exists n :: 0 <= n && P(Tail(s, n).head, h) +} +copredicate AlwaysAnother(s: Stream, h: PredicateHandle) +{ + IsAnother(s, h) && AlwaysAnother(s.tail, h) +} +comethod Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle) + requires AllP(s, h); + ensures AlwaysAnother(s, h); +{ + assert Tail(s, 0) == s; +} + +function Next(s: Stream, h: PredicateHandle): nat + requires AlwaysAnother(s, h); + ensures P(Tail(s, Next(s, h)).head, h); + ensures forall i :: 0 <= i < Next(s, h) ==> !P(Tail(s, i).head, h); +{ + var n :| 0 <= n && P(Tail(s, n).head, h); + NextMinimizer(s, h, n) +} +// the following is an auxiliary function of the definition of Next +function NextMinimizer(s: Stream, h: PredicateHandle, n: nat): nat + requires P(Tail(s, n).head, h); + ensures P(Tail(s, NextMinimizer(s, h, n)).head, h); + ensures forall i :: 0 <= i < NextMinimizer(s, h, n) ==> !P(Tail(s, i).head, h); +{ + if forall i :: 0 <= i < n ==> !P(Tail(s, i).head, h) then + n + else + var k :| 0 <= k < n && P(Tail(s, k).head, h); + NextMinimizer(s, h, k) +} + +function Filter(s: Stream, h: PredicateHandle): Stream + requires AlwaysAnother(s, h); + decreases Next(s, h); +{ + if P(s.head, h) then + Cons(s.head, Filter(s.tail, h)) + else + Filter(s.tail, h) +} +// properties about Filter +comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle) + requires AlwaysAnother(s, h); + ensures AllP(Filter(s, h), h); + decreases Next(s, h); +{ + if P(s.head, h) { + Filter_AlwaysAnother(s.tail, h); + } else { + Filter_AlwaysAnother#[_k](s.tail, h); + } +} +comethod Filter_IsSubStream(s: Stream, h: PredicateHandle) + requires AlwaysAnother(s, h); + ensures IsSubStream(Filter(s, h), s); + decreases Next(s, h); +{ + if P(s.head, h) { + // To prove IsSubStream#[_k](Filter(s, h), s), we prove the two conjuncts from the definition + calc { + true; + == { Filter_IsSubStream(s.tail, h); } // induction hypothesis + IsSubStream#[_k-1](Filter(s.tail, h), s.tail); + == // { assert Filter(s.tail, h) == Filter(s, h).tail; } + IsSubStream#[_k-1](Filter(s, h).tail, s.tail); + ==> { Lemma_TailSubStreamK(Filter(s, h).tail, s, _k-1); } + IsSubStream#[_k-1](Filter(s, h).tail, s); + } + calc { + In(Filter(s, h).head, s); + == { assert Filter(s, h) == Cons(s.head, Filter(s.tail, h)); } + In(s.head, s); + == { assert Tail(s, 0) == s; + assert exists n :: 0 <= n && Tail(s, n).head == s.head; + } + true; + } + } else { + Lemma_TailSubStreamK(Filter(s.tail, h), s, _k); + } +} + +// The following says nothing about the order of the elements in the stream +ghost method Theorem_Filter(s: Stream, h: PredicateHandle) + requires AlwaysAnother(s, h); + ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h); +{ + forall (x) + ensures In(x, Filter(s, h)) <==> In(x, s) && P(x, h); + { + if In(x, Filter(s, h)) { + FS_Ping(s, h, x); + } + if In(x, s) && P(x, h) { + var k :| 0 <= k && Tail(s, k).head == x; + FS_Pong(s, h, x, k); + } + } +} + +ghost method FS_Ping(s: Stream, h: PredicateHandle, x: T) + requires AlwaysAnother(s, h) && In(x, Filter(s, h)); + ensures In(x, s) && P(x, h); +{ + Filter_IsSubStream(s, h); + Lemma_InSubStream(x, Filter(s, h), s); + + Filter_AlwaysAnother(s, h); + assert AllP(Filter(s, h), h); + Lemma_InAllP(x, Filter(s, h), h); +} + +ghost method FS_Pong(s: Stream, h: PredicateHandle, x: T, k: nat) + requires AlwaysAnother(s, h) && In(x, s) && P(x, h); + requires Tail(s, k).head == x; + ensures In(x, Filter(s, h)); + decreases k; +{ + var fs := Filter(s, h); + if s.head == x { + assert Tail(fs, 0) == fs; + } else if P(s.head, h) { + assert fs == Cons(s.head, Filter(s.tail, h)); // reminder of where we are + calc { + true; + == { FS_Pong(s.tail, h, x, k-1); } + In(x, Filter(s.tail, h)); + ==> { assert fs.head != x; Lemma_InTail(x, fs); } + In(x, fs); + } + } else { + assert fs == Filter(s.tail, h); // reminder of where we are + FS_Pong(s.tail, h, x, k-1); + } +} + +// ----- orderings ------ + +function Ord(x: T, ord: PredicateHandle): int + +copredicate Increasing(s: Stream, ord: PredicateHandle) +{ + Ord(s.head, ord) < Ord(s.tail.head, ord) && Increasing(s.tail, ord) +} +copredicate IncrFrom(s: Stream, low: int, ord: PredicateHandle) +{ + low <= Ord(s.head, ord) && IncrFrom(s.tail, Ord(s.head, ord) + 1, ord) +} + +comethod Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle) + requires IncrFrom(s, low, ord); + ensures Increasing(s, ord); +{ +} +comethod Lemma_Incr1(s: Stream, ord: PredicateHandle) + requires Increasing(s, ord); + ensures IncrFrom(s, Ord(s.head, ord), ord); +{ + Lemma_Incr1(s.tail, ord); +} + +ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle) + requires Increasing(s, ord) && AlwaysAnother(s, h); + ensures Increasing(Filter(s, h), ord); +{ + Lemma_Incr1(s, ord); + Lemma_FilterPreservesIncrFrom(s, h, Ord(s.head, ord), ord); + Lemma_Incr0(Filter(s, h), Ord(s.head, ord), ord); +} +comethod Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle) + requires IncrFrom(s, low, ord) && AlwaysAnother(s, h) && low <= Ord(s.head, ord); + ensures IncrFrom(Filter(s, h), low, ord); + decreases Next(s, h); +{ + if P(s.head, h) { + Lemma_FilterPreservesIncrFrom(s.tail, h, Ord(s.head, ord)+1, ord); + } else { + Lemma_FilterPreservesIncrFrom#[_k](s.tail, h, low, ord); + } +} diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 2f8c2a9e..8709a6d8 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -25,7 +25,7 @@ function Up(n: int): Stream */ function FivesUp(n: int): Stream - decreases (n + 4) / 5 * 5 - n; + decreases 4 - (n-1) % 5; { if n % 5 == 0 then SCons(n, FivesUp(n+1)) else FivesUp(n+1) @@ -113,7 +113,7 @@ comethod UpPos_Auto(n:int) comethod {:induction false} FivesUpPos(n:int) requires n > 0; ensures Pos(FivesUp(n)); - decreases (n + 4) / 5 * 5 - n; + decreases 4 - (n-1) % 5; { if (n % 5 == 0) { FivesUpPos#[_k - 1](n + 1); @@ -127,7 +127,7 @@ comethod {:induction false} FivesUpPos(n:int) comethod FivesUpPos_Auto(n:int) requires n > 0; ensures Pos(FivesUp(n)); - decreases (n + 4) / 5 * 5 - n; + decreases 4 - (n-1) % 5; { } diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index 3bcae386..c2182d6c 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -8,7 +8,7 @@ for %%f in ( Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy - Paulson.dfy + Paulson.dfy Filter.dfy ) do ( echo. echo -------------------- %%f -------------------- -- cgit v1.2.3