%%% %%% 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: Exercise 8.4-1 Page 172-173 in book: %%% The Foundations of Program Verification, Second Edition %%% Jacques Loeckx and Kurt Sieber %%% %%% Note November 26, 1999: %%% We had to reorder "eveni_equals_even" proof because it seems that %%% PVS 2.3 does not yield three cases, but only two: it seems to %%% simplify the "n=2" case without displaying it. %%% power_example: THEORY BEGIN eveni?(n: int): INDUCTIVE bool = ( n = 2 OR (EXISTS (i, j: int): eveni?(i) AND eveni?(j) AND n = i+j) OR (EXISTS (i, j: int): eveni?(i) AND eveni?(j) AND n = i-j)) ; zero_eveni: LEMMA eveni?(0) ; opposite_eveni: LEMMA (FORALL (n: int): eveni?(n) IMPLIES eveni?(-n)) ; eveni_opposite: COROLLARY (FORALL (n: int): eveni?(-n) IMPLIES eveni?(n)) ; eveni_or_succ: LEMMA (FORALL (n: int): eveni?(n) OR eveni?(n+1)) ; eveni_equals_even: LEMMA eveni? = even? ; %% %% This proof is tricky! It relies upon "eveni?" inductive definition %% and the "eveni_or_succ" lemma which claims that either "n" or "n+1" %% is even (which does not seem provable directly with "even?" %% definition). %% odd_not_even: LEMMA (FORALL (n: int): odd?(n) = NOT even?(n)) ; half(n: int): {h: int | (NOT odd?(n)) IMPLIES n = 2*h} even_half_double: LEMMA (FORALL (n: (even?)): n = 2*half(n)) ; twice_not_odd_half: COROLLARY (FORALL (i: int): (NOT odd?(i)) IMPLIES 2*half(i) = i) ; zero_lt_half: LEMMA (FORALL (i: int): (i > 0 AND NOT odd?(i)) IMPLIES 0 < half(i)) ; half_ge_zero: LEMMA (FORALL (i: int): (i>=0 AND NOT odd?(i)) IMPLIES half(i)>=0) ; zero_le_half: COROLLARY (FORALL (i: int): (i>=0 AND NOT odd?(i)) IMPLIES 0<=half(i)) ; half_lt: LEMMA (FORALL (i: int): (i > 0 AND NOT odd?(i)) IMPLIES half(i) < i) ; half_lt2: COROLLARY (FORALL (i, j: int): (i > 0 AND NOT odd?(i) AND i = j) IMPLIES half(i) < j) ; IMPORTING integer_program_verification square_power_half: LEMMA (FORALL (i: int, n: nat): NOT odd?(n) IMPLIES (i*i)**half(n) = i**n) ; % half: unary[term] = l(half) ; % by CONVERSION! % odd?: unary[term, assertion] = l(odd?) ; % by CONVERSION! %% %% Declaration of variables used in "power" imperative program: %% ----------------------------------------------------------- %% X: variable = nv ; Y: {V: variable | V /= X} = nv(X) ; Z: {V: variable | V /= X & V /= Y} = nv(X, Y) ; A: {V: variable | V /= X & V /= Y & V /= Z} = nv(X, Y, Z) ; B: {V: variable | V /= X & V /= Y & V /= Z & V /= A } = nv(X, Y, Z, A) ; power_termination: LEMMA % helps TCC proof for "power" program. terminates?(lti ,Y ,Y>=0 AND equals(Z*(X**Y), A**B)) (Y>0) (IF odd?(Y) THEN set(Y, Y-1) @@ set(Z, X*Z) ELSE set(X, X*X) @@ set(Y, half(Y)) ENDIF) ; %% %% "power" imperative program definition: %% ------------------------------------- %% %% Z := 1; %% while Y>0 %% do if odd?(Y) %% then Y := Y-1; Z := X*Z %% else Z := Z*Z; Y := Y/2 %% fi %% od %% power: program = set(Z, 1) @@ while(lti, Y, Y>=0 AND equals(Z*(X**Y), A**B)) (Y>0, IF odd?(Y) THEN set(Y, Y-1) @@ set(Z, X*Z) ELSE set(X, X*X) @@ set(Y, half(Y)) ENDIF) ; %% %% "power" specification: [b>=0 & x=a] power [z=a**b] %% --------------------- %% power_correct: LEMMA correct?(B>=0 AND equals(X, A) AND equals(Y, B), power, equals(Z, A**B)) ; END power_example