diff options
Diffstat (limited to 'Jennisys/Jennisys/examples/List.jen')
-rw-r--r-- | Jennisys/Jennisys/examples/List.jen | 77 |
1 files changed, 0 insertions, 77 deletions
diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen deleted file mode 100644 index 85a3b692..00000000 --- a/Jennisys/Jennisys/examples/List.jen +++ /dev/null @@ -1,77 +0,0 @@ -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 -} |