1 files changed, 31 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/Simple.jen b/Source/Jennisys/examples/Simple.jen
new file mode 100644
index 00000000..2f5e7feb
--- /dev/null
+++ b/Source/Jennisys/examples/Simple.jen
@@ -0,0 +1,31 @@
+interface Simple {
+ var a: int
+ 
+ method Inc(p: int)
+   a := old(a) + p   
+   
+ 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   
+   
+ method MaxAll__mod__(x: seq[int])
+   ensures a in x
+   ensures forall t :: t in x ==> a >= t
+}
+
+datamodel Simple {
+ var c: int
+ invariant a = c
+}
+\ No newline at end of file