diff options
| author |  Unknown <aleks@aleks-PC.csail.mit.edu> | 2011-10-08 20:28:16 -0400 |
|---|---|---|
| committer | Unknown <aleks@aleks-PC.csail.mit.edu> | 2011-10-08 20:28:16 -0400 |
| commit | 8e04cd792ec754798974e112dedfc7131f3aedb3 (patch) | |
| tree | 9f9ec9bba9049241afb92281243f430e0084f0b2 /Jennisys/examples | |
| parent | e654a8563982eab5980835de1d95c4e975b5e753 (diff) | |
Jennisys: added some more simple methods in Simple.jen, implemented a couple of
optimiations/exensions
Diffstat (limited to 'Jennisys/examples')
| -rw-r--r-- | Jennisys/examples/List.jen | 6 | ||||
| -rw-r--r-- | Jennisys/examples/Simple.jen | 16 |
2 files changed, 22 insertions, 0 deletions
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index 9d29aeee..cba09f46 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -59,6 +59,12 @@ interface Node[T] { method Find(n: T) returns (ret: bool) ensures ret = (n in list) + + method SetZ(n: T) + ensures list = old(list[0 := n]) + + method Insert(n: T) + ensures list = old(list) + [n] } datamodel Node[T] { diff --git a/Jennisys/examples/Simple.jen b/Jennisys/examples/Simple.jen index bd2e2993..12b2cdf0 100644 --- a/Jennisys/examples/Simple.jen +++ b/Jennisys/examples/Simple.jen @@ -3,6 +3,22 @@ interface Simple { method Inc()
a := old(a) + 1
+
+ method Init(n: int)
+ a := n
+
+ method Max(x: int, y: int)
+ ensures x < y ==> a = y
+ ensures x >= y ==> a = x
+
+
+ method Max2(x: int, y: int)
+ ensures a = x || a = y
+ ensures forall t :: t in {x y} ==> a >= t
+
+ method Max3__mod__(x: int, y: int)
+ ensures a in {x y}
+ ensures forall t :: t in {x y} ==> a >= t
}
datamodel Simple {
|