diff options
Diffstat (limited to 'Jennisys/examples/List.jen')
| -rw-r--r-- | Jennisys/examples/List.jen | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index bb36c2bb..7fa04fc4 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -46,6 +46,11 @@ class 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| + requires idx != 0 && next != null + ensures ret = list[idx] } model Node[T] { |