%%% %%% 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: %%% - basis: the functions or predicates used in the "factorial" imperative %%% program or its specification: these include a functional %%% version of the factorial, denoted "fac", which is recursively %%% defined; %%% - declaration of variables used in the "factorial" program; %%% - definition of "factorial" using the imperative constructions. %%% %%% Notes November 17, 1999: %%% a) we first used type coercion with PVS 2.3, because in %%% "factorial.correct?" lemma PVS can nolonger determine %%% "equals" intended type, although there is only one possibility. %%% Is this a bug? %%% "PVS error: Could not determine the full theory instance %%% for equals" %%% Secondly, we decide not to overload "equals" in %%% "folfhl@expressions" theory. %%% b) (SUBTYPE-TCC) strategy nolonger solves TCCs related to %%% declaration of variables, e.g., N0_TCC1 here: we use %%% (GROUND) instead. It seems that (SUBTYPE-TCC) does not %%% use as much type information as it used to do. %%% factorial_example: THEORY BEGIN IMPORTING integer_program_verification %% %% Extend integer function basis: %% fac(n: int): RECURSIVE int = (IF n <= 0 THEN 1 ELSE n*fac(n - 1) ENDIF) MEASURE (LAMBDA(n: int): (IF n>=0 THEN n ELSE 0 ENDIF)) ; fac: unary[term] = l(fac) ; %% %% Declaration of variables: %% N: variable = nv ; R: {V: variable | V /= N} = nv(N) ; N0: {V: variable | V /= N & V /= R} = nv(N, R) ; R0: {V: variable | V /= N & V /= R & V /= N0} = nv(N, R, N0) ; %% %% Factorial termination proof boils down to a partial correctness proof! %% Note: this is the same as "factorial_TCC1: OBLIGATION" generated by %% PVS while type checking the "while" instruction in the %% "factorial" program; for some reason, this same TCC arises %% in the course of the proof of "factorial_correct: LEMMA", %% probably through application of the "cw" rule: apparently PVS %% does not capitalize on global TCCs. %% factorial_termination: SUBLEMMA terminates?(lti, N, equals(R*fac(N),R0*fac(N0))) (N > 0) ( set(R, R*N) % factorial loop body. @@ set(N, N-1)) ; %% %% Imperative factorial: %% factorial: program = %% %% while n>0 do r:=r*n; n:=n-1 od %% while(lti, N, % termination reason. equals(R*fac(N),R0*fac(N0))) % well chosen invariant! (N > 0, % N>0. set(R, R*N) % R := R*N; @@ set(N, N-1)) ; % N := N-1. factorial_correct: LEMMA %% %% [n=n0 /\ r=r0] while n>0 do r:=r*n; n:=n-1 od [r=r0*n0!] %% correct?(equals(N,N0) AND equals(R,R0), factorial, equals(R, R0*fac(N0))) ; END factorial_example