summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2013-01-16 19:33:15 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2013-01-16 19:33:15 -0800
commit678f36ea920b1be7c7633b9ab7a50672ad54c7b4 (patch)
treebccb63f1141697ca3fb57654bafef704eaf0b54f /Test
parentb47707c222e2d68fb27d4ace45f106e34b2b9f7f (diff)
Removed the syntactic form copredicate #-form with the implicit argument.
Added syntactic support for codatatype #-form equalities.
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/Answer30
-rw-r--r--Test/dafny0/CoResolution.dfy42
-rw-r--r--Test/dafny0/CoinductiveProofs.dfy25
-rw-r--r--Test/dafny3/Answer2
-rw-r--r--Test/dafny3/Streams.dfy187
5 files changed, 201 insertions, 85 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 964b69a4..87e6e93f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1327,20 +1327,12 @@ Execution trace:
Dafny program verifier finished with 5 verified, 2 errors
-------------------- CoResolution.dfy --------------------
-CoResolution.dfy(22,8): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(23,3): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(24,7): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(25,7): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(26,2): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(26,12): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(27,2): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(30,2): Error: wrong number of function arguments (got 3, expected 2)
-CoResolution.dfy(31,5): Error: unresolved identifier: _k
-CoResolution.dfy(37,30): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(38,20): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-13 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(43,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
+CoResolution.dfy(54,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+CoResolution.dfy(22,7): Error: member Undeclared# does not exist in class _default
+CoResolution.dfy(23,2): Error: unresolved identifier: Undeclared#
+CoResolution.dfy(26,5): Error: unresolved identifier: _k
+5 resolution/type errors detected in CoResolution.dfy
-------------------- CoPrefix.dfy --------------------
CoPrefix.dfy(61,7): Error: failure to decrease termination measure
@@ -1348,7 +1340,7 @@ Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-CoPrefix.dfy(74,7): Error: failure to decrease termination measure
+CoPrefix.dfy(74,7): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -1358,8 +1350,12 @@ CoPrefix.dfy(111,11): Related location: This is the postcondition that might not
CoPrefix.dfy(99,17): Related location: Related location
Execution trace:
(0,0): anon0
+CoPrefix.dfy(136,25): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Then
-Dafny program verifier finished with 17 verified, 3 errors
+Dafny program verifier finished with 23 verified, 4 errors
-------------------- CoinductiveProofs.dfy --------------------
CoinductiveProofs.dfy(26,12): Error: assertion violation
@@ -1401,7 +1397,7 @@ CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 32 verified, 8 errors
+Dafny program verifier finished with 35 verified, 8 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 233a818b..3146147e 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -19,25 +19,49 @@ copredicate D()
copredicate S(d: set<int>)
{
- this.S#(d) && // error: the call to S# must give an explicit depth argument
- S#(d) && // error: the call to S# must give an explicit depth argument
- this.Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
this.S#[5](d) &&
S#[5](d) &&
- S#(5, d) && // error: the '5' here does not give the depth argument
S#[_k](d) // error: _k is not an identifier in scope
}
comethod CM(d: set<int>)
{
var b;
- b := this.S#[5](d) && this.S#(d + d); // error: cannot rely on implicit depth argument here
- b := S#[5](d) && S#(d + d); // error: cannot rely on implicit depth argument here
+ b := this.S#[5](d);
+ b := S#[5](d);
this.CM#[5](d);
CM#[5](d);
- this.CM#(d + d); // error: must give an explicit depth argument
- CM#(d + d); // error: must give an explicit depth argument
+}
+
+module GhostCheck0 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ method UseStream0(s: Stream)
+ {
+ var x := 3;
+ if (s == s.tail) { // error: this operation is allowed only in ghost contexts
+ x := x + 2;
+ }
+ }
+}
+module GhostCheck1 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ method UseStream1(s: Stream)
+ {
+ var x := 3;
+ if (s ==#[20] s.tail) { // this seems innocent enough, but it's currently not supported by the compiler, so...
+ x := x + 7; // error: therefore, this is an error
+ }
+ }
+}
+module GhostCheck2 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ ghost method UseStreamGhost(s: Stream)
+ {
+ var x := 3;
+ if (s == s.tail) { // fine
+ x := x + 2;
+ }
+ }
}
diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index ddb23b5b..47c5f262 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -153,3 +153,28 @@ comethod BadEquality1(n: int)
{ // error: postcondition does not hold
BadEquality1(n+1);
}
+
+// test that match statements/expressions get the correct assumption (which wasn't always the case)
+
+codatatype IList<T> = INil | ICons(head: T, tail: IList<T>);
+
+ghost method M(s: IList)
+{
+ match (s) {
+ case INil =>
+ assert s == INil;
+ case ICons(a, b) =>
+ assert s == ICons(a, b);
+ }
+}
+
+function G(s: IList): int
+{
+ match s
+ case INil =>
+ assert s == INil;
+ 0
+ case ICons(a, b) =>
+ assert s == ICons(a, b);
+ 0
+}
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 5ab835e7..9cd8fc82 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 15 verified, 0 errors
-------------------- Streams.dfy --------------------
-Dafny program verifier finished with 38 verified, 0 errors
+Dafny program verifier finished with 50 verified, 0 errors
-------------------- Dijkstra.dfy --------------------
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1369e584..757d6a37 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -49,13 +49,35 @@ comethod Theorem0(M: Stream<X>)
Theorem0(N);
}
}
-comethod Theorem0_alt(M: Stream<X>)
+comethod Theorem0_Alt(M: Stream<X>)
ensures map_fg(M) == map_f(map_g(M));
{
if (M.Cons?) {
- Theorem0(M.tail);
+ Theorem0_Alt(M.tail);
}
}
+ghost method Theorem0_Par(M: Stream<X>)
+ ensures map_fg(M) == map_f(map_g(M));
+{
+ parallel (k: nat) {
+ Theorem0_Ind(k, M);
+ }
+}
+ghost method Theorem0_Ind(k: nat, M: Stream<X>)
+ ensures map_fg(M) ==#[k] map_f(map_g(M));
+{
+ if (k != 0) {
+ match (M) {
+ case Nil =>
+ case Cons(x, N) =>
+ Theorem0_Ind(k-1, N);
+ }
+ }
+}
+ghost method Theorem0_AutoInd(k: nat, M: Stream<X>)
+ ensures map_fg(M) ==#[k] map_f(map_g(M));
+// { // TODO: this is not working yet, apparently
+// }
// map f (append M N) = append (map f M) (map f N)
comethod Theorem1(M: Stream<X>, N: Stream<X>)
@@ -67,13 +89,40 @@ comethod Theorem1(M: Stream<X>, N: Stream<X>)
Theorem1(M', N);
}
}
-comethod Theorem1_alt(M: Stream<X>, N: Stream<X>)
+comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)
ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
{
if (M.Cons?) {
- Theorem1(M.tail, N);
+ Theorem1_Alt(M.tail, N);
}
}
+ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
+{
+ parallel (k: nat) {
+ Theorem1_Ind(k, M, N);
+ }
+}
+ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));
+{
+ // this time, try doing the 'if' inside the 'match' (instead of the other way around)
+ match (M) {
+ case Nil =>
+ case Cons(x, M') =>
+ if (k != 0) {
+ Theorem1_Ind(k-1, M', N);
+ }
+ }
+}
+ghost method Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));
+// { // TODO: this is not working yet, apparently
+// }
+ghost method Theorem1_AutoForall()
+{
+// assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N)); // TODO: this is not working yet, apparently
+}
// append NIL M = M
ghost method Theorem2(M: Stream<X>)
@@ -92,11 +141,11 @@ comethod Theorem3(M: Stream<X>)
Theorem3(N);
}
}
-comethod Theorem3_alt(M: Stream<X>)
+comethod Theorem3_Alt(M: Stream<X>)
ensures append(M, Nil) == M;
{
if (M.Cons?) {
- Theorem3(M.tail);
+ Theorem3_Alt(M.tail);
}
}
@@ -110,11 +159,11 @@ comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)
Theorem4(M', N, P);
}
}
-comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
+comethod Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
ensures append(M, append(N, P)) == append(append(M, N), P);
{
if (M.Cons?) {
- Theorem4(M.tail, N, P);
+ Theorem4_Alt(M.tail, N, P);
}
}
@@ -122,7 +171,7 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
// Flatten can't be written as just:
//
-// function SimpleFlatten<T>(M: Stream<Stream>): Stream
+// function SimpleFlatten(M: Stream<Stream>): Stream
// {
// match M
// case Nil => Nil
@@ -130,9 +179,9 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
// }
//
// because this function fails to be productive given an infinite stream of Nil's.
-// Instead, here are two variations SimpleFlatten. The first variation (FlattenStartMarker)
+// Instead, here are two variations of 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
+// insists that "M" contain 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
@@ -140,18 +189,18 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
function FlattenStartMarker<T>(M: Stream<Stream>, startMarker: T): Stream
{
- FlattenStartMarkerAcc(Nil, M, startMarker)
+ PrependThenFlattenStartMarker(Nil, M, startMarker)
}
-function FlattenStartMarkerAcc<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T): Stream
+function PrependThenFlattenStartMarker<T>(prefix: Stream, M: Stream<Stream>, startMarker: T): Stream
{
- match accumulator
+ match prefix
case Cons(hd, tl) =>
- Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker))
+ Cons(hd, PrependThenFlattenStartMarker(tl, M, startMarker))
case Nil =>
match M
case Nil => Nil
- case Cons(s, N) => Cons(startMarker, FlattenStartMarkerAcc(s, N, startMarker))
+ case Cons(s, N) => Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker))
}
// The next variation of Flatten requires M to contain no empty streams.
@@ -166,26 +215,24 @@ copredicate StreamOfNonEmpties(M: Stream<Stream>)
function FlattenNonEmpties(M: Stream<Stream>): Stream
requires StreamOfNonEmpties(M);
{
- FlattenNonEmptiesAcc(Nil, M)
+ PrependThenFlattenNonEmpties(Nil, M)
}
-function FlattenNonEmptiesAcc(accumulator: Stream, M: Stream<Stream>): Stream
+function PrependThenFlattenNonEmpties(prefix: Stream, M: Stream<Stream>): Stream
requires StreamOfNonEmpties(M);
{
- match accumulator
+ match prefix
case Cons(hd, tl) =>
- Cons(hd, FlattenNonEmptiesAcc(tl, M))
+ Cons(hd, PrependThenFlattenNonEmpties(tl, M))
case Nil =>
match M
case Nil => Nil
- case Cons(s, N) => Cons(s.head, FlattenNonEmptiesAcc(s.tail, N))
+ case Cons(s, N) => Cons(s.head, PrependThenFlattenNonEmpties(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<T>(x: T, M: Stream<Stream>): Stream<Stream>
ensures StreamOfNonEmpties(Prepend(x, M));
@@ -201,58 +248,82 @@ ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
Lemma_Flatten(Nil, M, startMarker);
}
-comethod Lemma_Flatten<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T)
- ensures FlattenStartMarkerAcc(accumulator, M, startMarker) == FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));
+comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)
+ ensures PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, 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));
+ match (prefix) {
+ case Cons(hd, tl) =>
+ Lemma_Flatten(tl, M, startMarker);
+ case Nil =>
+ match (M) {
+ case Nil =>
+ case Cons(s, N) =>
+ if (*) {
+ // This is all that's needed for the proof
+ Lemma_Flatten(s, N, startMarker);
+ } else {
+ // ...but here are some calculations that try to show more of what's going on
+ // (It would be nice to have ==#[...] available as an operator in calculations.)
+
+ // massage the LHS:
+ calc {
+ PrependThenFlattenStartMarker(prefix, M, startMarker);
+ == // def. PrependThenFlattenStartMarker
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker));
+ }
+ // massage the RHS:
+ calc {
+ PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ == // M == Cons(s, N)
+ PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, Cons(s, N)));
+ == // def. Prepend
+ PrependThenFlattenNonEmpties(prefix, Cons(Cons(startMarker, s), Prepend(startMarker, N)));
+ == // def. PrependThenFlattenNonEmpties
+ Cons(Cons(startMarker, s).head, PrependThenFlattenNonEmpties(Cons(startMarker, s).tail, Prepend(startMarker, N)));
+ == // Cons, head, tail
+ Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));
+ }
+
+ // all together now:
+ calc {
+ PrependThenFlattenStartMarker(prefix, M, startMarker) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ { // by the calculation above, we have:
+ assert PrependThenFlattenStartMarker(prefix, M, startMarker) == Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)); }
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ { // and by the other calculation above, we have:
+ assert PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M)) == Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N))); }
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));
+ == // def. of ==#[_k] for _k != 0
+ startMarker == startMarker &&
+ PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));
+ { Lemma_Flatten(s, N, startMarker);
+ // the postcondition of the call we just made (which invokes the co-induction hypothesis) is:
+ assert PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));
+ }
+ true;
+ }
+ }
+ }
}
}
comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)
- ensures FlattenStartMarkerAcc(s, M, startMarker) == append(s, FlattenStartMarkerAcc(Nil, M, startMarker));
+ ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(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));
- }
+ Lemma_FlattenAppend0(tl, M, startMarker);
}
}
comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)
requires StreamOfNonEmpties(M);
- ensures FlattenNonEmptiesAcc(s, M) == append(s, FlattenNonEmptiesAcc(Nil, M));
+ ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(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));
- }
+ Lemma_FlattenAppend1(tl, M);
}
}