diff options
Diffstat (limited to 'contrib/correctness/examples/Handbook.v')
| -rw-r--r-- | contrib/correctness/examples/Handbook.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v index dae2873996..26b2af4cfd 100644 --- a/contrib/correctness/examples/Handbook.v +++ b/contrib/correctness/examples/Handbook.v @@ -25,7 +25,7 @@ * Programs are refered to by numbers and pages. *) -Require Programs. +Require Correctness. Require Sumbool. Require Omega. @@ -49,34 +49,34 @@ Axiom axiom3 : (x,y:Z) `y>=0` -> `(Zpower (x*x) (Zdiv2 y)) = (Zpower x y)`. Global Variable X : Z ref. Global Variable Y : Z ref. -Global Variable Z : Z ref. +Global Variable Z_ : Z ref. Correctness pgm25 { `Y >= 0` } begin - Z := 1; + Z_ := 1; while !Y <> 0 do - { invariant `Y >= 0` /\ `Z * (Zpower X Y) = (Zpower X@0 Y@0)` + { invariant `Y >= 0` /\ `Z_ * (Zpower X Y) = (Zpower X@0 Y@0)` variant Y } if (Zodd_bool !Y) then begin Y := (Zpred !Y); - Z := (Zmult !Z !X) + Z_ := (Zmult !Z_ !X) end else begin Y := (Zdiv2 !Y); X := (Zmult !X !X) end done end - { Z = (Zpower X@ Y@) }. + { Z_ = (Zpower X@ Y@) }. Proof. Split. Unfold Zpred; Unfold Zwf; Omega. Split. Unfold Zpred; Omega. Decompose [and] Pre2. -Rewrite <- H1. -Replace `Z1*X0*(Zpower X0 (Zpred Y0))` with `Z1*(X0*(Zpower X0 (Zpred Y0)))`. -Apply f_equal with f := (Zmult Z1). +Rewrite <- H0. +Replace `Z_1*X0*(Zpower X0 (Zpred Y0))` with `Z_1*(X0*(Zpower X0 (Zpred Y0)))`. +Apply f_equal with f := (Zmult Z_1). Apply axiom1. Omega. @@ -97,15 +97,15 @@ Split. Omega. Decompose [and] Pre2. -Rewrite <- H1. -Apply f_equal with f:=(Zmult Z1). +Rewrite <- H0. +Apply f_equal with f:=(Zmult Z_1). Apply axiom3. Omega. Omega. Decompose [and] Post6. Rewrite <- H2. -Rewrite H1. +Rewrite H0. Simpl. Omega. @@ -143,9 +143,9 @@ Unfold Zpred. Omega. Unfold Zs. Unfold Zpred in Post3. Split. Omega. Decompose [and] Post3. -Rewrite H0. +Rewrite H. Replace `X0+(-1)+1` with X0. -Rewrite H1. +Rewrite H0. Replace `X0+(-1)` with `X0-1`. Apply axiom5. Omega. @@ -176,12 +176,12 @@ let rec F (u:unit) : unit { variant N } = Proof. Unfold Zwf. Unfold Zpred. Omega. Unfold Zpred. Omega. -Decompose [and] Post5. Rewrite H0. Unfold Zwf. Unfold Zpred. Omega. -Decompose [and] Post5. Rewrite H0. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zwf. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zpred. Omega. Split. Unfold Zpred in Post5. Omega. -Decompose [and] Post4. Rewrite H1. -Decompose [and] Post5. Rewrite H3. Rewrite H2. +Decompose [and] Post4. Rewrite H0. +Decompose [and] Post5. Rewrite H2. Rewrite H1. Replace `(Zpower 2 N0)` with `2*(Zpower 2 (Zpred N0))`. Omega. Symmetry. Replace `(Zpower 2 N0)` with `(Zpower 2 (1+(Zpred N0)))`. |