%%% %%% 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: Example 7.2-3 Page 147 in book: %%% The Foundations of Program Verification, Second Edition %%% Jacques Loeckx and Kurt Sieber %%% Note: We use a "while" version of "two_power" derived from the %%% flowchart version presented in the book; we have switched %%% the roles of X and Y variables so that X is the input and %%% Y the output. %%% Note November 26, 1999: %%% PVS 2.3 forced us to add "::assertion" in order to avoid %%% misinterpretation due to automatic K_conversion: the problem %%% is that AND and IMPLIES are too ambiguous (we should probably %%% remove some overloading, such as the definitions using HOLDS, %%% which is equivalent to K_conversion, and actually this will %%% probably render HOLDS unnecessary. %%% two_power_example: THEORY BEGIN IMPORTING integer_program_verification %% %% Declaration of variables: %% X: variable = nv ; Y: {V: variable | V /= X} = nv(X) ; U: {V: variable | V /= X & V /= Y} = nv(X, Y) ; A: {V: variable | V /= X & V /= Y & V /= U} = nv(X, Y, U) ; two_power_termination: LEMMA % helps "two_power" TCC proof! terminates?(lti % wellfounded relation, ,2**A - Y + X % variant, ,equals((2**X)*(Y+U), 2**(1+A)) % invariant. AND X<=A AND X>=0 AND (equals(X, 0) IMPLIES equals(Y, U))::assertion AND U>=0 AND Y>0 AND Y<=2**A) (diff(X, 0)) % "two_power" loop test. (IF equals(U, 0) % "two_power" loop body. THEN set(U, Y) @@ set(X, X-1) ELSE set(Y, Y+1) @@ set(U, U-1) ENDIF) ; %% %% Imperative program for computing 2**A %% ------------------------------------- %% %% y := 1; %% u := 1; %% while x/=0 %% do %% if u=0 %% then u := y; %% x := x-1; %% else y := y+1; %% u := u-1 %% endif %% od %% two_power: program = set(Y, 1) @@ set(U, 1) @@ while(lti, 2**A - Y + X, % relation, variant. %% %% Invariant: equals((2**X)*(Y+U), 2**(1+A)) AND X<=A AND X>=0 AND (equals(X, 0) IMPLIES equals(Y, U))::assertion AND U>=0 AND Y>0 AND Y<=2**A) (diff(X, 0), % loop test. IF equals(U, 0) THEN set(U, Y) @@ set(X, X-1) ELSE set(Y, Y+1) @@ set(U, U-1) ENDIF) ; %% %% "two_power" specification: [x=a & a>=0] two_power [y=2**a] %% ------------------------- %% two_power_correct: LEMMA correct?(equals(X, A) AND A>=0, two_power, equals(Y, 2**A)) ; END two_power_example