summaryrefslogtreecommitdiff
path: root/Jennisys/examples/List3.jen
diff options
context:
space:
mode:
authorGravatar Unknown <t-alekm@A3479878.redmond.corp.microsoft.com>2011-07-19 20:14:38 -0700
committerGravatar Unknown <t-alekm@A3479878.redmond.corp.microsoft.com>2011-07-19 20:14:38 -0700
commit52bf54c844b89716258239649f56d87db33cbdc6 (patch)
treed91f257ffafb6fbae8f5c0cdfa0e1b08bc08c011 /Jennisys/examples/List3.jen
parent88fd8c7c8ddbcc89a56c45f017c842bda0e6a8ce (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.jen4
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