summaryrefslogtreecommitdiff
path: root/Jennisys/examples/List3.jen
diff options
context:
space:
mode:
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