diff options
| author |  Rustan Leino <unknown> | 2013-02-21 18:21:17 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-02-21 18:21:17 -0800 |
| commit | a69159f8819e3355591cfa63db38d75a491e9cba (patch) | |
| tree | c485e090ec124133eb6128066b9b74a127fd0946 /Test/dafny0/FunctionSpecifications.dfy | |
| parent | d26d672bb7cfea66721d4a819477f3a7541d4631 (diff) | |
Fixed let-such-that and if-then-else encodings so that they will pass the subrange tests
Diffstat (limited to 'Test/dafny0/FunctionSpecifications.dfy')
| -rw-r--r-- | Test/dafny0/FunctionSpecifications.dfy | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy index 44709ce8..cd38d3dd 100644 --- a/Test/dafny0/FunctionSpecifications.dfy +++ b/Test/dafny0/FunctionSpecifications.dfy @@ -58,3 +58,32 @@ function HoldsAtLeastForZero(x: int): bool {
x < -2 // error: this does not hold for 0
}
+
+// ----- Some functions that deal with let-such-that and if-then-else expressions and having them pass
+// ----- the subrange test (which they didn't always do).
+
+function IncA(x: nat): nat
+ ensures x < IncA(x);
+{
+ if x == 17 then
+ 18
+ else
+ var y :| x < y;
+ y
+}
+
+ghost method M() {
+ var z := IncA(10);
+ assert z != 0;
+}
+
+function IncB(i: nat): nat
+{
+ var n :| n>i; n
+}
+
+function IncC(i: nat): int
+ ensures IncC(i)>=0;
+{
+ var n :| n>i; n
+}
|