From 70523547fb07542156e744df2123e844aa928001 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sat, 24 Nov 2012 17:40:40 -0800 Subject: Beefed up loop invariant to prove a functional postcondition in a test case. --- Test/dafny1/KatzManna.dfy | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'Test/dafny1') diff --git a/Test/dafny1/KatzManna.dfy b/Test/dafny1/KatzManna.dfy index 38b2963e..60b70c1a 100644 --- a/Test/dafny1/KatzManna.dfy +++ b/Test/dafny1/KatzManna.dfy @@ -1,10 +1,13 @@ -method NinetyOne(x: int) returns (z: int) - requires 0 <= x; -// ensures z == (if x > 101 then x-10 else 91); +method NinetyOne(x: int, ghost proveFunctionalPostcondition: bool) returns (z: int) + ensures proveFunctionalPostcondition ==> z == if x > 101 then x-10 else 91; { var y1 := x; var y2 := 1; while (true) + // the following two invariants are needed only to prove the postcondition + invariant proveFunctionalPostcondition ==> 100 < x ==> y1 == x; + invariant proveFunctionalPostcondition ==> x <= 100 < y1 && y2 == 1 ==> y1 == 101; + // the following two lines justify termination, as in the paper by Katz and Manna invariant (y1 <= 111 && y2 >= 1) || (y1 == x && y2 == 1); decreases -2*y1 + 21*y2 + 2*(if x < 111 then 111 else x); { @@ -53,15 +56,15 @@ method Determinant(X: array2, M: int) returns (z: int) var y := X[1-1,1-1]; var a := 1; while (a != M) - invariant 1 <= a && a <= M; + invariant 1 <= a <= M; { var b := a + 1; while (b != M+1) - invariant a+1 <= b && b <= M+1; + invariant a+1 <= b <= M+1; { var c := M; while (c != a) - invariant a <= c && c <= M; + invariant a <= c <= M; { assume X[a-1,a-1] != 0; X[b-1, c-1] := X[b-1,c-1] - X[b-1,a-1] / X[a-1,a-1] * X[a-1,c-1]; -- cgit v1.2.3