From 5a83f112c46196e2a48cb88796751d1a131df122 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 19 Oct 2012 22:55:54 -0700 Subject: Test cases for co-inductive proofs, and an axiom that makes some of them possible --- Test/dafny3/Answer | 4 + Test/dafny3/Streams.dfy | 258 ++++++++++++++++++++++++++++++++++++++++++++++++ Test/dafny3/runtest.bat | 2 +- 3 files changed, 263 insertions(+), 1 deletion(-) create mode 100644 Test/dafny3/Streams.dfy (limited to 'Test/dafny3') diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index 3c339054..ae65e2d9 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -2,3 +2,7 @@ -------------------- Iter.dfy -------------------- Dafny program verifier finished with 15 verified, 0 errors + +-------------------- Streams.dfy -------------------- + +Dafny program verifier finished with 38 verified, 0 errors diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy new file mode 100644 index 00000000..1369e584 --- /dev/null +++ b/Test/dafny3/Streams.dfy @@ -0,0 +1,258 @@ +// ----- Stream + +codatatype Stream = Nil | Cons(head: T, tail: Stream); + +function append(M: Stream, N: Stream): Stream +{ + match M + case Nil => N + case Cons(t, M') => Cons(t, append(M', N)) +} + +// ----- f, g, and maps + +type X; + +function f(x: X): X +function g(x: X): X + +function map_f(M: Stream): Stream +{ + match M + case Nil => Nil + case Cons(x, N) => Cons(f(x), map_f(N)) +} + +function map_g(M: Stream): Stream +{ + match M + case Nil => Nil + case Cons(x, N) => Cons(g(x), map_g(N)) +} + +function map_fg(M: Stream): Stream +{ + match M + case Nil => Nil + case Cons(x, N) => Cons(f(g(x)), map_fg(N)) +} + +// ----- Theorems + +// map (f * g) M = map f (map g M) +comethod Theorem0(M: Stream) + ensures map_fg(M) == map_f(map_g(M)); +{ + match (M) { + case Nil => + case Cons(x, N) => + Theorem0(N); + } +} +comethod Theorem0_alt(M: Stream) + ensures map_fg(M) == map_f(map_g(M)); +{ + if (M.Cons?) { + Theorem0(M.tail); + } +} + +// map f (append M N) = append (map f M) (map f N) +comethod Theorem1(M: Stream, N: Stream) + ensures map_f(append(M, N)) == append(map_f(M), map_f(N)); +{ + match (M) { + case Nil => + case Cons(x, M') => + Theorem1(M', N); + } +} +comethod Theorem1_alt(M: Stream, N: Stream) + ensures map_f(append(M, N)) == append(map_f(M), map_f(N)); +{ + if (M.Cons?) { + Theorem1(M.tail, N); + } +} + +// append NIL M = M +ghost method Theorem2(M: Stream) + ensures append(Nil, M) == M; +{ + // trivial +} + +// append M NIL = M +comethod Theorem3(M: Stream) + ensures append(M, Nil) == M; +{ + match (M) { + case Nil => + case Cons(x, N) => + Theorem3(N); + } +} +comethod Theorem3_alt(M: Stream) + ensures append(M, Nil) == M; +{ + if (M.Cons?) { + Theorem3(M.tail); + } +} + +// append M (append N P) = append (append M N) P +comethod Theorem4(M: Stream, N: Stream, P: Stream) + ensures append(M, append(N, P)) == append(append(M, N), P); +{ + match (M) { + case Nil => + case Cons(x, M') => + Theorem4(M', N, P); + } +} +comethod Theorem4_alt(M: Stream, N: Stream, P: Stream) + ensures append(M, append(N, P)) == append(append(M, N), P); +{ + if (M.Cons?) { + Theorem4(M.tail, N, P); + } +} + +// ----- Flatten + +// Flatten can't be written as just: +// +// function SimpleFlatten(M: Stream): Stream +// { +// match M +// case Nil => Nil +// case Cons(s, N) => append(s, SimpleFlatten(N)) +// } +// +// because this function fails to be productive given an infinite stream of Nil's. +// Instead, here are two variations SimpleFlatten. The first variation (FlattenStartMarker) +// prepends a "startMarker" to each of the streams in "M". The other (FlattenNonEmpties) +// insists that "M" contains no empty streams. One can prove a theorem that relates these +// two versions. + +// This first variation of Flatten returns a stream of the streams in M, each preceded with +// "startMarker". + +function FlattenStartMarker(M: Stream, startMarker: T): Stream +{ + FlattenStartMarkerAcc(Nil, M, startMarker) +} + +function FlattenStartMarkerAcc(accumulator: Stream, M: Stream, startMarker: T): Stream +{ + match accumulator + case Cons(hd, tl) => + Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker)) + case Nil => + match M + case Nil => Nil + case Cons(s, N) => Cons(startMarker, FlattenStartMarkerAcc(s, N, startMarker)) +} + +// The next variation of Flatten requires M to contain no empty streams. + +copredicate StreamOfNonEmpties(M: Stream) +{ + match M + case Nil => true + case Cons(s, N) => s.Cons? && StreamOfNonEmpties(N) +} + +function FlattenNonEmpties(M: Stream): Stream + requires StreamOfNonEmpties(M); +{ + FlattenNonEmptiesAcc(Nil, M) +} + +function FlattenNonEmptiesAcc(accumulator: Stream, M: Stream): Stream + requires StreamOfNonEmpties(M); +{ + match accumulator + case Cons(hd, tl) => + Cons(hd, FlattenNonEmptiesAcc(tl, M)) + case Nil => + match M + case Nil => Nil + case Cons(s, N) => Cons(s.head, FlattenNonEmptiesAcc(s.tail, N)) +} + +// We can prove a theorem that links the previous two variations of flatten. To +// do that, we first define a function that prepends an element to each stream +// of a given stream of streams. +// The "assume" statements below are temporary workaround. They make the proofs +// unsound, but, as a temporary measure, they express the intent of the proofs. + +function Prepend(x: T, M: Stream): Stream + ensures StreamOfNonEmpties(Prepend(x, M)); +{ + match M + case Nil => Nil + case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N)) +} + +ghost method Theorem_Flatten(M: Stream, startMarker: T) + ensures FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M)); +{ + Lemma_Flatten(Nil, M, startMarker); +} + +comethod Lemma_Flatten(accumulator: Stream, M: Stream, startMarker: T) + ensures FlattenStartMarkerAcc(accumulator, M, startMarker) == FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M)); +{ + calc { + FlattenStartMarkerAcc(accumulator, M, startMarker); + { Lemma_FlattenAppend0(accumulator, M, startMarker); } + append(accumulator, FlattenStartMarkerAcc(Nil, M, startMarker)); + { Lemma_Flatten(Nil, M, startMarker); + assume FlattenStartMarkerAcc(Nil, M, startMarker) == FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M)); // postcondition of the co-recursive call + } + append(accumulator, FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M))); + { Lemma_FlattenAppend1(accumulator, Prepend(startMarker, M)); } + FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M)); + } +} + +comethod Lemma_FlattenAppend0(s: Stream, M: Stream, startMarker: T) + ensures FlattenStartMarkerAcc(s, M, startMarker) == append(s, FlattenStartMarkerAcc(Nil, M, startMarker)); +{ + match (s) { + case Nil => + case Cons(hd, tl) => + calc { + FlattenStartMarkerAcc(Cons(hd, tl), M, startMarker); + Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker)); + { Lemma_FlattenAppend0(tl, M, startMarker); + assume FlattenStartMarkerAcc(tl, M, startMarker) == append(tl, FlattenStartMarkerAcc(Nil, M, startMarker)); // this is the postcondition of the co-recursive call + } + Cons(hd, append(tl, FlattenStartMarkerAcc(Nil, M, startMarker))); + // def. append + append(Cons(hd, tl), FlattenStartMarkerAcc(Nil, M, startMarker)); + } + } +} + +comethod Lemma_FlattenAppend1(s: Stream, M: Stream) + requires StreamOfNonEmpties(M); + ensures FlattenNonEmptiesAcc(s, M) == append(s, FlattenNonEmptiesAcc(Nil, M)); +{ + match (s) { + case Nil => + case Cons(hd, tl) => + calc { + FlattenNonEmptiesAcc(Cons(hd, tl), M); + // def. FlattenNonEmptiesAcc + Cons(hd, FlattenNonEmptiesAcc(tl, M)); + { Lemma_FlattenAppend1(tl, M); + assume FlattenNonEmptiesAcc(tl, M) == append(tl, FlattenNonEmptiesAcc(Nil, M)); // postcondition of the co-recursive call + } + Cons(hd, append(tl, FlattenNonEmptiesAcc(Nil, M))); + // def. append + append(Cons(hd, tl), FlattenNonEmptiesAcc(Nil, M)); + } + } +} diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index 35d8cc60..9265dcd0 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -4,7 +4,7 @@ setlocal set BINARIES=..\..\Binaries set DAFNY_EXE=%BINARIES%\Dafny.exe -for %%f in (Iter.dfy) do ( +for %%f in (Iter.dfy Streams.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -- cgit v1.2.3