diff options
| author |  Aleksandar Milicevic <unknown> | 2011-08-16 18:17:37 -0700 |
|---|---|---|
| committer | Aleksandar Milicevic <unknown> | 2011-08-16 18:17:37 -0700 |
| commit | f0989291edf82f7548d6146632269473c32b9286 (patch) | |
| tree | 2cb085b9d4e79095eac52e7aabfbc6b82544c936 /Jennisys/examples | |
| parent | e68494fba6e0b6f419bbfa109f877e794928c832 (diff) | |
Jennisys:
- changed the way candidate conditions are discovered; now it simply uses
all sub-expressions found in the spec that evaluate to TrueLiteral
- changed the implementation so that when trying to infer a precondition,
try out several different possibilities (and see which one works)
- added some very basic (and incomplete) type inference
- fixed a bug in the Modularizer (it didn't fix the solution after trying
out the spec infered from the solution)
- fixed a bug in DafnyModelUtils so that now when reading from the boogie
model file it keeps getting information from Seq# functions until
reaching a fixpoint (that's needed because the order or reads is important)
Diffstat (limited to 'Jennisys/examples')
| -rw-r--r-- | Jennisys/examples/List.jen | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index 7fa04fc4..e056bcfa 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -49,7 +49,6 @@ class Node[T] { method Get(idx: int) returns (ret: T) requires idx >= 0 && idx < |list| - requires idx != 0 && next != null ensures ret = list[idx] } @@ -61,6 +60,6 @@ model Node[T] { next invariant - next = null <==> list = [data] + next = null ==> list = [data] next != null ==> list = [data] + next.list } |