diff options
| author |  rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
| commit | 9f2be05e55c8fcb8e753afb965ff242d79327691 (patch) | |
| tree | e5418c4c1217e763542dfdf36c0f26a059b5393f /Test/dafny0/Definedness.dfy | |
| parent | 9d24f5281d326d92b3cc738bcc6e870ee43f1653 (diff) | |
Dafny: added ensures clauses to functions
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index d557de21..1cb74b1d 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -213,3 +213,45 @@ class StatementTwoShoes { }
}
}
+
+// ----------------- function postconditions ----------------------
+
+class Mountain { var x: int; }
+
+function Postie0(c: Mountain): Mountain
+ requires c != null;
+ ensures Postie0(c) != null && Postie0(c).x <= Postie0(c).x;
+ ensures Postie0(c).x == Postie0(c).x;
+{
+ c
+}
+
+function Postie1(c: Mountain): Mountain
+ requires c != null;
+ ensures Postie1(c) != null && Postie1(c).x == 5; // error: postcondition violation (but no well-formedness problem)
+{
+ c
+}
+
+function Postie2(c: Mountain): Mountain
+ requires c != null && c.x == 5;
+ ensures Postie2(c).x == 5; // well-formedness error (null dereference)
+{
+ c
+}
+
+function Postie3(c: Mountain): Mountain // all is cool
+ requires c != null && c.x == 5;
+ ensures Postie3(c) != null && Postie3(c).x < 10;
+ ensures Postie3(c).x == 5;
+{
+ c
+}
+
+function Postie4(c: Mountain): Mountain
+ requires c != null && c.x <= 5;
+ ensures Postie4(c) != null && Postie4(c).x < 10;
+ ensures Postie4(c).x == 5; // error: postcondition might not hold
+{
+ c
+}
|