summaryrefslogtreecommitdiff
path: root/Jennisys/examples/List2.jen
diff options
context:
space:
mode:
Diffstat (limited to 'Jennisys/examples/List2.jen')
-rw-r--r--Jennisys/examples/List2.jen3
1 files changed, 3 insertions, 0 deletions
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index b7ceaec0..e99cf342 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -18,6 +18,9 @@ class IntList {
constructor Double(p: int, q: int)
ensures list = [p] + [q]
+
+ constructor Sum(p: int, q: int)
+ ensures list = [p + q]
}
model IntList {