summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-08-12 15:31:45 -0700
committerGravatar Rustan Leino <unknown>2014-08-12 15:31:45 -0700
commitc28ad1d1565e60dfd14164366552efb18876872f (patch)
tree2085c0f6b014329b994a534ec9ab9f421bdb9681
parentf09fb9edbd4e6dfb064359887c17dd3dc1630302 (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.dfy8
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
{
}