diff options
Diffstat (limited to 'Jennisys/examples/List2.jen')
| -rw-r--r-- | Jennisys/examples/List2.jen | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen index ae8a2845..3bd527fb 100644 --- a/Jennisys/examples/List2.jen +++ b/Jennisys/examples/List2.jen @@ -48,6 +48,11 @@ interface IntNode { constructor Double(x: int, y: int) ensures list = [x y] + + method Max() returns (ret: int) + ensures ret in list + ensures forall t :: t in list ==> ret >= t + } datamodel IntNode { |