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