%%% %%% 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.10 Page 139 in book: %%% The Foundations of Program Verification, Second Edition %%% Jacques Loeckx and Kurt Sieber %%% Note: We use a "while" version of "f91" derived from the %%% flowchart version presented in the book. %%% f91_example: THEORY BEGIN IMPORTING integer_program_verification %% %% Declaration of variables: %% X: variable = nv ; Y1: {V: variable | V /= X} = nv(X) ; Y2: {V: variable | V /= X & V /= Y1} = nv(X, Y1) ; Z: {V: variable | V /= X & V /= Y1 & V /= Y2} = nv(X, Y1, Y2) ; %% %% This lemma arises as a TCC, and also as a subgoal of "f91_correct" %% lemma, in the course of its proof: %% f91_termination: LEMMA % helps TCC proof for "f91" program. terminates?(lti ,201+21*Y2-2*Y1 ,Y1<=111 AND Y2>=1 AND ((Y1>=101 AND equals(Y2, 1)) IMPLIES equals(Y1, 101))) %% f91 while test: (Y1<=100 OR (Y1>100 AND diff(Y2,1))) %% f91 loop body: (IF Y1>100 THEN set(Y1, Y1-10) @@ set(Y2, Y2-1) ELSE set(Y1, Y1+11) @@ set(Y2, Y2+1) ENDIF) ; %% %% Imperative f91 program: %% %% y1 := x; %% y2 := 1; %% while y1<=100 OR (y1>100 AND y2 /= 1) %% do %% if y1>100 %% then y1 := y1-10; y2 := y2-1 %% else y1 := y1+11; y2 := y2+1 %% fi %% od; %% z := y1-10 %% f91: program = set(Y1, X) @@ set(Y2, 1) @@ while(lti, 201+21*Y2-2*Y1, % wellfounded relation and variant. %% Invariant: Y1<=111 AND Y2>=1 AND ((Y1>=101 AND equals(Y2, 1)) IMPLIES equals(Y1, 101))) %% Test: (Y1<=100 OR (Y1>100 AND diff(Y2,1)), %% Loop body: IF Y1>100 THEN set(Y1, Y1-10) @@ set(Y2, Y2-1) ELSE set(Y1, Y1+11) @@ set(Y2, Y2+1) ENDIF) @@ set(Z, Y1-10) ; %% %% f91 program specification: %% [x<=100] f91 [z=91] %% %% Note: Proof is the simplest one (most automatic): %% ("" (EXPAND "f91") (HFA)) %% It takes quite a long time, and does not use "f91_termination" %% lemma, whose proof is thus repeated. %% f91_correct: LEMMA correct?(X<=100, f91, equals(Z, 91)) ; END f91_example