diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
| commit | b0b61083adb4b427974c772658cdc744da23f42b (patch) | |
| tree | ca08e2f2f4d9b62583177e8a0a0691eb8f353dee /Test/dafny0/CoinductiveProofs.dfy | |
| parent | 8eb077dfd8515f26dc58754334d52f9c44a73e0c (diff) | |
Support for copredicates and prefix predicates in comethods.
(Missing from the co support are (prefix) equalities of codatatypes,
various restrictions on the use of co/prefix-predicates, and tactic
support for applying the (prefix-)induction automatically.)
Diffstat (limited to 'Test/dafny0/CoinductiveProofs.dfy')
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index c56f9b36..ddb23b5b 100644 --- a/Test/dafny0/CoinductiveProofs.dfy +++ b/Test/dafny0/CoinductiveProofs.dfy @@ -23,18 +23,18 @@ comethod PosLemma1(n: int) {
PosLemma1(n + 1);
if (*) {
- assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have a certificate
+ assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates
}
}
comethod Outside_CoMethod_Caller_PosLemma(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
-{ // error: this comethod is supposed to produce a certificate, but instead it establishes the real deal
- // (which currently produces a complaint from Dafny)
+{
assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward
PosLemma0(n + 1);
assert Pos(Upward(n+1)); // this follows directly from the previous line, because it isn't a recursive call
+ // ... and it implies the prefix predicate we're supposed to establish
}
method Outside_Method_Caller_PosLemma(n: int)
|