%%% %%% 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. %%% Presentation is as follows: %%% - theory of divisibility in the "int" domain. We define the following %%% relationships: %%% - "divides?" (binary relationship); %%% - "cd?", common divisor (ternary relationship); %%% - "gcd?", greatest common divisor (ternary relationship). %%% We prove a few lemmas about "divides?" and "gcd?", that will be %%% needed in the correctness proof of the imperative "gcd" program. %%% - basis: we extend the basis provided by "integer_program_verification" %%% theory by lifting the "gcd?" relationship at %%% the level of assertions: it becomes a [term -> assertion] %%% ternary operators (this is actually implicit thru "l" conversion); %%% - declaration of A, B, D variables used in the "gcd" program and its %%% specification; %%% - "gcd" termination sublemma; %%% - definition of "gcd" using the imperative constructions; %%% - "gcd" correctness lemma. %%% gcd_example: THEORY BEGIN %% %% Theory of divisibility in the "int" domain: %% ------------------------------------------ %% divides?(d, n: int): bool = (EXISTS (q: int): n = d*q) ; n_divides_0: LEMMA % just normal. (FORALL (n: int): divides?(n, 0)) ; yes_0_divides_0: COROLLARY % shocking? divides?(0, 0) ; yes_0_divides_0_only: LEMMA (FORALL (n: int): divides?(0, n) IMPLIES n=0); divides_minus: LEMMA (FORALL (a, b, d: int): divides?(d, a) AND divides?(d, b) IMPLIES divides?(d, a-b)) ; divides_plus: LEMMA (FORALL (a, b, d: int): divides?(d, a) AND divides?(d, b) IMPLIES divides?(d, a+b)) ; cd?(a, b, d: int): bool = divides?(d, a) AND divides?(d, b) ; gcd?(a, b, d: int): bool = cd?(a,b,d) AND (FORALL (dd: int): cd?(a, b, dd) IMPLIES dd <= d) ; gcd_unique: LEMMA (FORALL (a, b, d1, d2: int): a>0 AND b>0 AND gcd?(a, b, d1) AND gcd?(a, b, d2) IMPLIES d1 = d2) ; gcd_aaa: LEMMA (FORALL (a: int): a>0 IMPLIES gcd?(a, a, a)) ; gcd_equals: LEMMA (FORALL (a, b, d: int): a>0 AND a=b AND gcd?(a, b, d) IMPLIES d=a) ; gcd_minus: LEMMA (FORALL (a, b, d: int): gcd?(a, b, d) IMPLIES gcd?(a, b-a, d)) ; gcd_symmetric: LEMMA (FORALL (a, b, d: int): gcd?(a, b, d) IMPLIES gcd?(b, a, d)) ; %% %% Extend basis by lifting "divides?" and "gcd?": %% --------------------------------------------- %% IMPORTING integer_program_verification % gcd?: ternary[term, assertion] = l(gcd?) ; % by conversion! %% %% Declare gcd program variables: %% ----------------------------- %% A: variable = nv ; B: {V: variable | V /= A} = nv(A) ; D: {V: variable | V /= A & V /= B} = nv(A, B); %% %% "gcd" termination lemma: %% ----------------------- %% Proof uses "gcd_minus" and "gcd_symmetric" lemmas and "max" definition. %% gcd_termination: LEMMA % arises as a TCC in "gcd" definition % and as a subgoal in "gcd_correct" % proof. terminates?(lti % wellfounded relation. ,max(A, B) % variant. ,A>0 AND B>0 AND gcd?(A, B, D)) % invariant. (diff(A, B)) % gcd loop test. %% gcd loop body: (IF A0 AND B>0 AND gcd?(A, B, D)) % invariant. (diff(A, B), IF A0 /\ B>0 /\ gcd?(A, B, D)] gcd [A=D] %% %% Remark: proof starts with "(CORRECT*)" instead of "(HOARE)" so as to %% raise already proved "gcd_termination" subgoal, and take %% advantage of this lemma (whose proof is tricky) instead %% of erasing this "terminates?" goal as usual. %% gcd_correct: LEMMA correct?(A>0 AND B>0 AND gcd?(A, B, D), % precondition, gcd, equals(A, D)) ; % postcondition. END gcd_example