diff options
Diffstat (limited to 'Source/Jennisys/examples/oopsla12/Math.jen')
-rw-r--r-- | Source/Jennisys/examples/oopsla12/Math.jen | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/oopsla12/Math.jen b/Source/Jennisys/examples/oopsla12/Math.jen new file mode 100644 index 00000000..0cc772b3 --- /dev/null +++ b/Source/Jennisys/examples/oopsla12/Math.jen @@ -0,0 +1,20 @@ +interface Math {
+ method Min2(a: int, b: int) returns (ret: int)
+ ensures a < b ==> ret = a
+ ensures a >= b ==> ret = b
+
+ method Min3Sum(a: int, b: int, c: int)
+ returns (ret: int)
+ ensures ret in {a+b a+c b+c}
+ ensures forall x :: x in {a+b a+c b+c} ==> ret <= x
+
+ method Min4(a: int, b: int, c: int, d: int)
+ returns (ret: int)
+ ensures ret in {a b c d}
+ ensures forall x :: x in {a b c d} ==> ret <= x
+
+ method Abs(a: int) returns (ret: int)
+ ensures ret in {a (-a)} && ret >= 0
+}
+
+datamodel Math {}
\ No newline at end of file |