1 files changed, 44 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/Number.jen b/Source/Jennisys/examples/Number.jen
new file mode 100644
index 00000000..e31613bd
--- /dev/null
+++ b/Source/Jennisys/examples/Number.jen
@@ -0,0 +1,44 @@
+interface Number { 
+  var num: int
+ 
+  constructor Init(p: int)
+    ensures num = p
+
+  constructor Double(p: int)
+    ensures num = 2*p
+
+  constructor Sum(a: int, b: int)
+    ensures num = a + b
+
+  constructor Min2(a: int, b: int)
+    ensures a < b ==> num = a
+    ensures a >= b ==> num = b
+
+  constructor Min22(a: int, b: int)
+    ensures num in {a b}
+    ensures num <= a && num <= b
+
+  constructor Min3(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures num <= a && num <= b && num <= c
+
+  constructor Min32(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures forall x :: x in {a b c} ==> num <= x
+
+  constructor MinSum(a: int, b: int, c: int)
+    ensures num in {a+b a+c b+c}
+    ensures num <= a+b && num <= b+c && num <= a+c
+
+  constructor Min4(a: int, b: int, c: int, d: int)
+    ensures num in {a b c d}
+    ensures forall x :: x in {a b c d} ==> num <= x
+
+  constructor Abs(a: int)  
+    ensures num in {a (-a)} && num >= 0
+
+}
+
+datamodel Number {
+
+}
+\ No newline at end of file