diff options
| author |  Rustan Leino <unknown> | 2014-08-12 15:31:45 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-08-12 15:31:45 -0700 |
| commit | c28ad1d1565e60dfd14164366552efb18876872f (patch) | |
| tree | 2085c0f6b014329b994a534ec9ab9f421bdb9681 | |
| parent | f09fb9edbd4e6dfb064359887c17dd3dc1630302 (diff) | |
Rewrote two tests to make triggering better (while waiting for better automatic triggering support in either Dafny or Boogie)
| -rw-r--r-- | Test/dafny3/SimpleCoinduction.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index 5be5c569..00e598c3 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -35,13 +35,13 @@ colemma {:induction false} CoUpLemma(n: int) CoUpLemma(n+1);
}
-lemma UpLemma_Auto(k: nat, n: int)
- ensures Inc(Up(n)) ==#[k] Up(n+1);
+lemma UpLemma_Auto(k: nat, n: int, nn: int)
+ ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn); // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here
{
}
-colemma CoUpLemma_Auto(n: int)
- ensures Inc(Up(n)) == Up(n+1);
+colemma CoUpLemma_Auto(n: int, nn: int)
+ ensures nn == n+1 ==> Inc(Up(n)) == Up(nn); // see comment above
{
}
|