diff options
| author |  rustanleino <unknown> | 2010-02-04 22:14:26 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-02-04 22:14:26 +0000 |
| commit | f7250b98f91a9e81069b0dc2c7b9c16b36633dfc (patch) | |
| tree | debfee9c44a08b59528d861f550b28a9036a2b1b /Test/dafny0/Simple.dfy | |
| parent | 1f481fb44bfce9fd0684e9d59e324db248b798ff (diff) | |
Dafny: Added if-then-else expressions (replacing and extending the previous boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index a224ed91..c5599529 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -27,6 +27,14 @@ class MyClass<T,U> { assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
}
}
+
+ function F(x: int, y: int, h: WildData, k: WildData): WildData
+ {
+ if x < 0 then h else
+ if (x == 0) then
+ if if h==k then true else false then h else if y == 0 then k else h
+ else k
+ }
}
// some datatype stuff:
|