diff options
author | 2011-07-19 20:14:38 -0700 | |
---|---|---|
committer | 2011-07-19 20:14:38 -0700 | |
commit | 52bf54c844b89716258239649f56d87db33cbdc6 (patch) | |
tree | d91f257ffafb6fbae8f5c0cdfa0e1b08bc08c011 /Jennisys/examples/List3.jen | |
parent | 88fd8c7c8ddbcc89a56c45f017c842bda0e6a8ce (diff) |
- added synthesis of Repr stuff (it generates Repr invariants,
and updates the Repr fields at the end of every constructor)
- refactoring:
- removed ExprConst
- change the implementation to use HeapModel and HeapInstance
(as opposed to propagating heap/env/ctx)
Diffstat (limited to 'Jennisys/examples/List3.jen')
-rw-r--r-- | Jennisys/examples/List3.jen | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen index acb10ad5..776bd43d 100644 --- a/Jennisys/examples/List3.jen +++ b/Jennisys/examples/List3.jen @@ -27,7 +27,7 @@ model IntList { var root: IntNode frame - root * root.list[*] + root invariant root = null ==> |list| = 0 @@ -63,7 +63,7 @@ model IntNode { var next: IntNode frame - data * next + next invariant next = null ==> |succ| = 0 |