%%% %%% Author: Paul Y Gloess %%% http://dept-info.labri.u-bordeaux.fr/~gloess/ %%% %%% LaBRI, ENSERB & Universite Bordeaux I %%% 351, Cours de la Liberation %%% 33405 Talence Cedex %%% France %%% %%% This example serves as an illustration of the Hoare proof %%% techniques for imperative programming in PVS. %%% Source: Examples 3.10 Page 50 and 6.3 Page 115 and 7.3 Page 134 in book: %%% The Foundations of Program Verification, Second Edition %%% Jacques Loeckx and Kurt Sieber %%% sqrt_example: THEORY BEGIN IMPORTING integer_program_verification X: variable = nv ; Y1: {V: variable | V /= X} = nv(X) ; Y2: {V: variable | V /= X & V /= Y1} = nv(X, Y1) ; Y3: {V: variable | V /= X & V /= Y1 & V /= Y2} = nv(X, Y1, Y2) ; A: {V: variable | V /= X & V /= Y1 & V /= Y2 & V /= Y3} = nv(X, Y1, Y2, Y3) ; %% %% This subgoal arises both as a TCC for "sqrt" program and in the course %% of "sqrt_correct" proof: %% sqrt_termination: LEMMA terminates?(lti % wellfounded relation, ,X-Y1 % variant, ,equals(X, A) AND Y1**2<=X % invariant. AND equals(Y3, (Y1+1)**2) AND equals(Y2, 2*Y1+1)) (Y3<=X) % "sqrt" loop test %% "sqrt" loop body: ( set(Y1, Y1+1) @@ set(Y2, Y2+2) @@ set(Y3, Y3+Y2)) ; %% %% sqrt imperative program: %% ----------------------- %% %% y1 := 0; %% y2 := 1; %% y3 := 1; %% while y3<=x %% do y1 := y1+1; %% y2 := y2+2; %% y3 := y3+y2 %% od %% sqrt: program = set(Y1, 0) @@ set(Y2, 1) @@ set(Y3, 1) @@ while(lti, X-Y1, % wellfounded relation, variant, equals(X, A) % invariant starts here. AND (Y1**2<=X) AND equals(Y3, (Y1+1)**2) AND equals(Y2, 2*Y1+1)) (Y3<=X, % test. set(Y1, Y1+1) @@ set(Y2, Y2+2) @@ set(Y3, Y3+Y2)) ; %% %% sqrt specification: [x>=0 & x=a] sqrt [y1**2<=a<(y1+1)**2] %% ------------------ %% sqrt_correct: LEMMA correct?(X>=0 AND equals(X, A), sqrt, Y1**2 <= A AND A < (Y1+1)**2) ; END sqrt_example