diff options
author | Rustan Leino <unknown> | 2013-03-05 17:01:25 -0800 |
---|---|---|
committer | Rustan Leino <unknown> | 2013-03-05 17:01:25 -0800 |
commit | 9f7c11c0a12a9b802f23d613abeee91a2fb47743 (patch) | |
tree | ff0c5ffd982094c5d03828f1332be03a4d66b4ea /Test/dafny0/PredExpr.dfy | |
parent | c819fabbb8da669952cb7e2e5937c73ff6dcfabe (diff) |
Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.
Diffstat (limited to 'Test/dafny0/PredExpr.dfy')
-rw-r--r-- | Test/dafny0/PredExpr.dfy | 79 |
1 files changed, 0 insertions, 79 deletions
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy deleted file mode 100644 index 96561ebd..00000000 --- a/Test/dafny0/PredExpr.dfy +++ /dev/null @@ -1,79 +0,0 @@ -function SimpleAssert(n: int): int
- ensures n < 100;
-{
- assert n == 58; // error: assert violation
- n // but postcondition is fine
-}
-
-function SimpleAssume(n: int): int
- ensures n < 100;
-{
- assume n == 58; n // all is fine
-}
-
-function Subonacci(n: nat): nat
-{
- if 2 <= n then
- // proving that this case is a nat requires more information,
- // which is here supplied by an assume expression
- assume Subonacci(n-2) <= Subonacci(n-1);
- Subonacci(n-1) - Subonacci(n-2)
- else
- n
-}
-
-function F(n: int): nat
-{
- Subonacci(assume 0 <= n; n) -
- Subonacci(n)
-}
-
-function G(n: int, b: bool): nat
-{
- if b then
- Subonacci(assume 0 <= n; n) + n // the last n is also affected by the assume
- else
- Subonacci(n) // error: n may not be a nat
-}
-
-ghost method M(m: nat, n: int)
-{
- var k := F(m);
- assert k == 0;
- k := F(n);
- assert k == 0; // this is still known
-}
-
-method M0(j: int) returns (n: nat)
-{
- n := assert 0 <= j; j; // error: j may be negative
-}
-
-method M1(j: int) returns (n: nat)
-{
- n := (assume 0 <= j; j) + (assert 0 <= j; j);
- assert n == 2*j;
-}
-
-function SpecOnly(): bool { true }
-
-function method FuncMeth(): int {
- assert SpecOnly(); // this call is allowed, because the .Guard of a
- // PredicateExpr is not included in compilation
- 15
-}
-
-method M5(a: int, b: int)
-{
- var k := if a < 0 then
- assume b < 0; 5
- else
- 5;
- if (*) {
- assert a == -7 ==> b < 0;
- assert b < 0; // error: this condition does not hold on every path here
- } else {
- assert assume a == -7; b < 0; // note, this is different than the ==> above
- assert b < 0; // this condition does hold on all paths to here
- }
-}
|