diff options
Diffstat (limited to 'Source/Jennisys/examples/List.jen')
-rw-r--r-- | Source/Jennisys/examples/List.jen | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/List.jen b/Source/Jennisys/examples/List.jen new file mode 100644 index 00000000..85a3b692 --- /dev/null +++ b/Source/Jennisys/examples/List.jen @@ -0,0 +1,77 @@ +interface List[T] { + var list: seq[T] + + constructor Empty() + ensures list = [] + + constructor Singleton(t: T) + ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] +} + +datamodel List[T] { + var root: Node[T] + + frame + root + + invariant + root = null ==> |list| = 0 + root != null ==> list = root.list +} + +interface Node[T] { + var list: seq[T] + + invariant + |list| > 0 + + constructor Init(t: T) + ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] + + method List() returns (ret: seq[T]) + ensures ret = list + + method Tail() returns (tail: Node[T]) + ensures |list| = 1 ==> tail = null + ensures |list| > 1 ==> tail != null && tail.list = list[1..] + + method Size() returns (ret: int) + ensures ret = |list| + + method SkipFew(num: int) returns (ret: Node[T]) + requires num >= 0 + ensures num >= |list| ==> ret = null + ensures num < |list| ==> ret != null && ret.list = list[num..] + + method Get(idx: int) returns (ret: T) + requires idx >= 0 && idx < |list| + ensures ret = list[idx] + + method Index(n: T) returns (ret: int) + ensures n !in list ==> ret = -1 + ensures n in list ==> ret >= 0 && ret < |list| && list[ret] = n + + method Find(n: T) returns (ret: bool) + ensures ret = (n in list) + + method Insert(n: T) + ensures list = old(list) + [n] +} + +datamodel Node[T] { + var data: T + var next: Node[T] + + frame + next + + invariant + next = null ==> list = [data] + next != null ==> list = [data] + next.list +} |