Imperative Program Verification in PVS

Paul Y Gloess

E.N.S.E.R.B. & LaBRI [C.N.R.S. UMR 5800]

june 14, 1999, last modified november 29, 1999

Jacques Loeckx and Kurt Sieber, in their book entitled "The Foundations of Program Verification, Second Edition", define two equivalent imperative programming languages:

The book covers two classical verification techniques for proving the partial correctness of imperative programs: the Floyd assertion method, well suited to L1, and the Hoare calcalus, designed for L2. It also addresses program termination through methods based on well founded sets.

We have modelled L2 into PVS functions, and developed a collection of PVS theories and strategies that help a user mechanically prove the total correctness of imperative programs. We have applied this collection to the proof of six simple programs presented in the book, which all deal with integers: "n!", "f91", "gcd", "a**b", "sqrt", "2**a".

The main difference between our approach and that of H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß in their paper entitled "Mechanized Semantics of Imperative Programming Constructs" is that they consider programs as binary relations of type "[env, env -> bool]" (thus allowing non deterministic programs) with emphasis on partial correctness, whereas we consider programs as total functions of type "[env -> env]" and focus on total correctness.

Contents

Modelling imperative programs into PVS functions

According to the terminology of Loeckx and Sieber, L2 is a family of languages whose each instance corresponds to the choice of a logical basis B, for the syntax, and an interpretation of B in some domain D, for its semantics. Typically, when D is Int (the domain of integers), the basis will consists of "+", "*", "-", ..., function symbols, and "<", ">", "=", ..., predicate symbols. A function symbol of arity n is interpreted by a function of type [D^n -> D] and a predicate symbol of arity n is interpreted by a function of type [D^n -> bool].

Let us call Dom the domain of interpretation, and derive from it all the types we need:

Consider L2 instruction set and its translation into PVS syntax:
 
L2 syntax
PVS syntax
X:= t
set(X, t)
if e then S1 else S2 fi 
IF e THEN S1 ELSE S2 ENDIF
while e do S od
while(r, v, i)(e, S)
S1; S2
S1 @@ S2
[| comment , S |]

with the implicit type declarations:

The correspondance is straightforward, except for the "while" statement: the PVS user must provide a well founded relation "r" in the domain Dom, a variant "v" and an invariant "i". The "[| comment , S |]" which does not exists in L2 is simply an "active comment" statement, which allows the user to govern the proof strategy by suggesting a program invariant that should hold before S is executed.

A variable is a projection pi(i), for some i: nat, which maps each sigma: env into sigma(i): Dom. Note that "variable" is precisely defined as a "term" subtype:

The following table is a summary of our program constructors, with their respective PVS types:
 
imperative program constructor:
PVS type
set:
[variable, term -> program]
IF_THEN_ELSE:
[assertion, program, program -> program]
while:
[(wellfounded?[Dom]), term, assertion
    -> [assertion, program -> program]]
@@:
[program, program -> program]

The type of "while" is actually more sophisticated than (and a subtype of) the above, because "while" is defined as a PVS recursive function, and like all PVS functions, must be proved total (see "Theoretical background" for more details).

In addition to program constructors, we provide term constructors and assertion constructors. These are derived from the logical basis B under consideration, by using the (highly overloaded) "l" so-called "lifting function". Thus "l" lifts each domain operator o (such as "+", "*", ...) into a term operator "l(o)" of same arity; "l" lifts each domain predicate p (such as "=", "<", ">") into a more abstract version "l(o)"; the boolean operators "NOT", "AND", "OR", ..., become assertion constructors. Note that "l" is limited to operators or predicates of arity up to 3.

In practice, we take advantage of overloading, supported by PVS, to make PVS imperative programs look as much as possible like imperative programs. The table below summarizes the "lifting rules" in general and specific cases, showing where overloading is possible or not.
 

concrete level

o

abstract level

l(o)

c: Dom
l(c): term
o1: [Dom -> Dom]
l(o1): [term -> term]
o2: [Dom, Dom -> Dom]
l(o2): [term, term -> term]
o3: [Dom, Dom, Dom -> Dom]
l(o3): [term, term, term -> term]
p: [Dom -> bool]
l(p): [Dom -> bool]
r: [Dom, Dom -> bool]
l(r): [term, term -> assertion]
p3: [Dom, Dom, Dom -> bool]
l(p3): [term, term, term -> assertion]
NOT: [bool -> bool]
NOT: [assertion -> assertion]
AND, OR, IMPLIES: [bool, bool -> bool]
AND, OR, IMPLIES: [assertion, assertion-> assertion]
=: [Dom, Dom -> bool]
equals: [term, term -> assertion]
/=: [Dom, Dom -> bool]
diff: [term, term -> assertion]
+, -, *: [int, int -> int]
+, -, *: [term, term-> term]
<, <=, >, >=: [int, int -> bool]
<, <=, >, >=: [term, term -> assertion]
..., -2, -1, 0, 1, 2, ...: int
..., -2, -1, 0, 1, 2, ...: term

Note that equality and disequality cannot be overloaded, as it would yield ambiguous expressions; numbers are not really overloaded, but automatic "l" conversion is used instead for constants. Relying solely on automatic conversion for all arities yields ambiguities, so that we use a compromise.

Syntactic sugar: A nice PVS feature is that by overloading boolean operators such as IMPLIES, AND, ..., and arithmetic operators +, -, *, or comparators <, >, ..., we take advantage of their infix syntax. The same remark holds for the "IF ... THEN ... ELSE ... ENDIF" special syntax which gets carried over the abstract program constructor; unfortunately, we were not able to overload ":=" for the assignment because it is a special notation reserved by PVS to records or the like: we had to use "set(X, t)" instead; likewise, we could not use ";" for sequential composition, since this would be incoompatible with PVS syntax: we chose "@@" infix notation instead.

Back to Contents or top.

Example of a PVS imperative program

Example 7.10, Page 139 of Loeckx and Sieber book gives a flowchart version of the famous "f91" program: translated from L1 into L2, this program looks like: Written in PVS, this program becomes: assuming that variables X, Y1, Y2, Z have been previously declared. The reader may look at "f91_example" theory for a complete view of this example.

Back to Contents or top.

Proving imperative program total correctness

Partial correctness of a program S with respect to input assertion p and output assertion q is usually denoted whereas total correctness is sometimes denoted Our "correct?" PVS predicate of type "[assertion, program, assertion -> bool]" represents total correctness. Assuming "f91" denotes the above program, a specification of "f91" is: We have actually proved this formula (named "f91_correct: LEMMA" in our "f91_example" theory). The PVS proof script only takes two commands: Back to Contents or top.

Six certified programs

We have currently applied our system to the "int" domain, and treated six examples of classical programs:
 
program
source
PVS proof script
comments
PVS theory
n!
?
(EXPAND "factorial") (AUTO-REWRITE "fac") (HFA)
->
factorial_example
f91
Loeckx & Sieber 

fig. 7.10, p. 139

(EXPAND "f91") (HFA)
->
f91_example
gcd
?
(EXPAND "gcd") (CORRECT*) 
    ("1" (FG))

    ("2" (FG) (REWRITE "gcd_equals" :FNUMS + :TARGET_FNUMS + :SUBST ("a" "A(s)" "b" "B(s)" "d" "D(s)")))

    ("3" (LEMMA "gcd_termination"))

->
gcd_example
a**b
Loeckx & Sieber

exercise 8.4-1, pp. 172-173

(EXPAND "power") 

(AUTO-REWRITE "twice_not_odd" "zero_lt_half" "half_ge_zero" "zero_le_half" "half_lt2" "square_power_half" "power_minus_1"))

(HFA)

->
power_example
sqrt
Loeckx & Sieber

example 3.10 p. 50, 6.3 p. 115, 7.3 p. 134

(EXPAND "sqrt") (HFA)
->
sqrt_example
2**a
Loeckx & Sieber

example 7.2-3

p. 147

(EXPAND "two_power") (CORRECT*) 
    ("1" (FA))

    ("2" (FA))

    ("3" (REWRITE "two_power_termination"))

->
two_power_example

Back to Contents or top.

Factorial example

Here is the "factorial" program as defined in PVS: It computes R0*N0! into R, where R0 and N0 are the initial values of R and N, according to the specification: Note that both the invariant in the "while" statement, and the output assertion in the specification, refer to the "fac" function. To make "fac" part of L2 basis, since our domain is "int", we have defined it as a recursive PVS function of type [int -> int]: and lifted it into a "term" unary operator: The proof of "factorial_correct" lemma requires three steps: The reader of the factorial_example PVS theory will notice the The syntax of this "terminates?" goal directly follows that of the "while" statement: a well founded relation, a variant, an invariant; then the loop test; then the loop body. The intuitive meaning of this formula is that the variant N should decrease according to the lti relation, each time the loop body is executed. Note that lti is simply defined by: Precisely, expanding the "terminates?" predicate yields two subgoals:(using L2 rather than PVS syntax for easier reading):
  1. [R*fac(N)=R0*fac(N0) ^ N>0] R := R*N; N := N-1 [R*fac(N)=R0*fac(N0)],
  2. [R*fac(N)=R0*fac(N0) ^ N>0 ^ N=d] R := R*N; N := N-1 [0<=N<d]
Proving the first goal amounts to proving that the invariant is indeed an invariant; the second goal is "pure termination": the variant N should strictly decrease after executing both assignments, which is obviously true (the invariant does not help in this simple case).

Both goals are actually partial correctness goals, so that curly brackets could be used in lieu of square brackets here, since the program fragment does not contain any "while" statement. Our proof technique ultimately transforms "total correctness" goals into "partial correctness" goals.

The reason for introducing "factorial_termination" sublemma in "factorial_example" theory is twofold:

Back to Six certified programs or Contents or top.

F91 example

Since we used "f91" as an introductory example, we will just recall the specification: whose proof requires two commands: The only difficulty was to provide a suitable variant (201+21*Y2-2*Y1) but it was given in Loeckx and Sieber book. PVS decision procedures do a very good job on these linear arithmetics (see "f91_example" PVS theory).

Back to Six certified programs or Contents or top.

Gcd example

Please check "gcd_example" PVS theory until I write some comments!

Back to Six certified programs or Contents or top.

Power example

Please check "power_example" PVS theory until I write some comments!

Back to Six certified programs or Contents or top.

Sqrt example

Please check "sqrt_example" PVS theory until I write some comments!

Back to Six certified programs or Contents or top.

Two_power example

Please check "two_power_example" PVS theory until I write some comments!

Back to Six certified programs or Contents or top.

Proof strategies

We have designed strategies at different levels so that a user can either try to do it all at once, and see nothing, or stop after application of Hoare rules, and look at the conditions to be verified. The latter is especially useful when one is not sure about his (her) variants or invariants. Remember that both of these have to be provided with each "while" statement. Note that if we have no idea whatsoever regarding these, we can always provide the declarations: and use them.

The general idea is that the proof of a specification "[p] S [q]" (or "correct?(p, S, q)" in PVS) involves three steps:

  1. Apply Hoare rules until nomore rule is applicable: each Hoare rule application decreases the size of program fragments S occurring in "correct?" subgoals; "while" Hoare rules generate "correct?" and "terminates?" subgoals, but "terminates?" subgoals are turned into "correct?" goals to which Hoare rules may again apply. The "assignment" Hoare rules trigger application of formal substitution. When nomore Hoare rule is applicable, we are left with a number of subgoals corresponding to "first order logic" conditions (all program fragments have disappeared): this phase acts as a "verification condition generator". Technically, each condition is presented as an assertion "a" (precisely of our type "assertion") which is implicitely universally quantified over "s: env". [We have overloaded "IMPLIES" to achieve this.] Thus, except for this top level universal quantifier, each condition is an assertion written with the abstract term or assertion constructors (such as IMPLIES, AND, equals, diff, +, -, *, ...);
  2. Go down from this abstract level of assertions to the concrete level of PVS, by skolemizing the "s: env" universal variable, and turning each abstract constructor into its concrete counterpart. As a result of this phase, the overall structure of each condition looks unchanged, but the formula is really ground: variables such as "X" have been turned into Dom constants of the form "X(s)" (or "X(s!1)", "X(s!2)", ..., if "s" constant was already around and renaming was necessary); abstract term or assertion constructors have been turned into concrete Dom or bool constructors, so that decision procedures or other classical PVS proof techniques can apply;
  3. Prove concrete goals using PVS decision procedures, augmented with lemmas in the concrete domain, when necessary.
Step 1 is fully automatic. This is possible, because we force the user to provide variant and invariants with the while statements. We have transformed Hoare calculus (which requires user assistance) into a set of rewrite rules that can be applied automatically.

In general, a PVS lemma has the form:

here [= TRUE] is assumed when the conclusion is reduced to "lhs" of type bool. If the "lhs" pattern contains all the variables "x1, ..., xk", the lemma is automatically applicable using REWRITE and providing no substitution. Furthermore, if the assumptions are sufficiently simple for PVS, the rule can be usefully declared as "AUTO-REWRITE" within a strategy, which tells PVS to apply it whenever possible.

Our PVS version of Hoare calculus requires explicit REWRITEs which are triggered by relevant strategies. These strategies simulate the Floyd assertion method which starts from the "end" of the program, rewriting the output assertion into a weakest liberal precondition. We base our calculus on the simple remark that correctness goals fall in two categories:

To tell the truth, the "if then else" statement does not exactly map this pattern: the first case actually yields two subgoals; the second case does not work! The user is invited to wrap his statement "s" in a comment statement which provides an intermediate assertion to be used: this is not totally satisfactory. The interested reader may check the "standard_verification" PVS theory for more information.

Formal substitution triggered by applying assignment Hoare rule is achieved by means of AUTO-REWRITE rules. The "alt" function denotes substitution. Substitution is defined semantically rather than syntactically in our framework: rewrite rules simulating formal substitution classical rules have been established as lemmas visible in "standard_verification" theory, which are specific instances of he general theorem:

with "f: [Source, ..., Source -> Range]", and suitable instantiations of type parameters Source and Range into Dom and bool. Note that x is a variable, t a term, and e1, ..., ek are expressions, that is, either terms or assertions, depending on Source and Range values. This general theorem has been established 4 times, once for each arity k=0, 1, 2, 3. Two other lemmas are used: Step 2 is also fully automatic, as it just amounts to applying skolemization, expanding abstract constructors, the "l" lifting function, and applying beta-reduction.

Note that step 1 and 2 do not depend on the domain.

Step 3 is not automatic in general, and may require user assistance, and proof of lemmas about the concrete domain Dom. For the "int" domain, we have extended PVS decision procedures by providing some lemmas about non linear arithmetics. However, this was not our main concern and clearly does not suffice: human help is a must with proof assistants!

Strategy User's Manual Summary

(see "pvs-strategies" source code for details)


proof command
effect
(HFA)
Most automatic. Applies Hoare rules to "correct?" goals, transforms "terminates?" goals into "correct?" goals, yielding conditions to be verified, then applies first order logic and arithmetics decision procedures to prove them. This is equivalent to: 
    (then (HOARE) (FOL) (ARITHMETICS)) .
    (HOARE)
Applies Hoare rules to "correct?" goals, and turns "terminates?" goals into "correct?" goals, and iterates until nomore rule is applicable, thus yielding conditions to be verified, represented at the "abstract level". Combines CORRECT* and TERMINATES strategies.
(FOL)
Transforms abstract conditions to be verified (as generated by HOARE) into their concrete form: this involves skolemization of "s:env" implicit universal quantification, beta-reduction and expansion of abstract term or assertion constructors.
(ARITHMETICS)
Declares a certain number of arithmetic rules as AUTO-REWRITE rules, then repeatedly applies PVS arithmetics and boolean decision procedures (GROUND*).
(CORRECT*)
Like HOARE, but leaves "terminates?" goals raised by "while" loops unchanged. This is useful if the proof of a termination goal is complex or lengthy: the proof does not have to be repeated.
(HF)
Like (HFA), but stops before trying to prove verification conditions. Equivalent to: 
    (then (HOARE) (FOL)) .
(FA)
Equivalent to 
    (then (FOL) (ARITHMETICS)) .
(GROUND*)
Repeatedly applies PVS linear arithmetics and boolean decision procedures. Equivalent to 
    (repeat* (GROUND)) .

Back to Contents or top.

Theoretical background

Our theories of imperative program verification are grouped in two PVS libraries called "fol" and "imperative": the latter uses the foremost, actually a small part of it. We follow this separation in the present outline: Imperative programs use assertions which are quantifier free formulas in the test of "if then else" and "while" statements; assertions are also used in program specifications. Terms are used is assignment statements.

Thus, there is a need for at least that part of first order logic consisting of "quantifier free formulas".

However, we have studied and represented full first order logic, including quantifiers. It would therefore be possible to write specifications, or even programs, containing quantified formulas, although we have avoided quantifiers in our six examples because our strategies currently do not support them (e.g., we have not yet automatized formal substitution within quantified formulas), and also because quanifiers do not seem terribly useful in this context.

Consider, for instance, the "gcd" specification, as stated in one of our six examples:

The "gcd?" used here is the abstraction "l(gcd?)" of the concrete "gcd?" defined in PVS by: with Hence it is possible in practice to hide quantifiers from the program and its specification, at the cost of extending the logical basis of L2.

First order logic

We study "full first order logic" and represent it in PVS.

Because PVS language is a "higher order logic", and therefore already contains "first order logic", it may not be clear to the reader why we need to represent "first order logic" in PVS .

We cannot directly use PVS formulas in the context of programs or specifications, because PVS formulas are of type "bool" whereas the type "assertion" defined as "[env -> bool]" is expected.

Here is an outline:

semantic approach

We take a semantic approach to first order logic, rather than a syntactic one. Each first order logic feature or concept must be represented or explained in term of PVS functions of appropriate types. The universal quantifier, for instance, will be represented by a function whose actual definition is available in "fol" library "quantifiers" theory.

The notion of formal substitution of a term for a variable into an expression (whether a term or an assertion) will be implemented as a function

where the "expr" parameter stands for either "term" or "assertion".

Back to First order logic or Contents or top.

Environment modifiability and determinism

In our introduction to PVS imperative programs, we started with the "Dom" type, and defined the "env" type as "[nat -> Dom]", "term" as "[env -> Dom]", and "variable" as a quite specific "term" subtype. In the context of first order logic, we need not be specific.

Here we take "env" as a type (sometimes assumed non empty), and "variable" as a subtype of "term", and "Dom" as a type. In some theories, we make the assumption that there exists a one to one mapping between "nat" and "variable".

In Loeckx and Sieber book, and other classical frameworks, the value of a variable "X" in an environment "sigma" is denoted "sigma(X)", because "env" is defined as "[variable -> Dom]". Then, for each "d: Dom", the mathematical notation "sigma[X/d]" denotes the function identical to "sigma" except maybe at point "X" where the value is "d".

In our setting, he value of variable "X" in environment "sigma" is written "X(sigma)", because "X" is the function, not "sigma". The advantage of this convention is that variables and other terms are treated in a uniform manner. The drawback is that the notation "sigma[X/d]" is not immediately available. It needs to be defined. This requires two assumptions:

In other words, modifiability means that we can always change the value of just one variable; determinism means that an environment is entirely determined by the values of all variables.

In PVS, making assumptions does not mean "adding axioms": theorems proved in the context of these assumptions should be understood as logical consequences of these assumptions. These theorems are useless if these assumptions have no model. It is clear that these assumptions have a model, and we were actually forced by PVS type checker to prove it (see "imperative" library "standard_environments" theory): the correctness of our six programs is established in the context of no assumption.

On the basis of these assumptions, we were able to define "sigma[X/d]" actually denoted "alt(X,d)(sigma)" in PVS, with

but we shall keep the "sigma[X/d]" notation for clarity.

Back to First order logic or Contents or top.

Formal substitution and lambda abstraction

Our next problem was to define formal substitution of a term t for a variable X into an expression e, which we shall also denote "e[X/t]" for clarity and truely denote "alt(X,t)(e)" in our PVS theories. Again "alt" is overloaded: Our definition of substitution is: which is exactly the "substitution theorem" (Theorem 2.10 p.24 in Loeckx & Sieber book): hence, we get this theorem for free, with added generality, since it holds for assertions (and terms) and not just for well formed formulas.

As a consequence, we can define "lambda abstraction" as a PVS function (called "lambada" because "lambda" is a reserved keywords in PVS) with type:

by the equation: The price we had to pay in exchange was the proof of: where "l" is our lifting function. Recall two simple lemmas: Back to First order logic or Contents or top.

Quantifiers

Universal and existential quantifiers are defined as functions. We have two versions: We named the quantifiers "foreach" and "thereis" because "forall" and "exists" are reserved PVS keywords, not functions that can be overloaded. Here are the definitions, in the binary case (the interested reader may look at "fol" library "quantifiers" theory for the unary case, which is defined by lifting): The binary and unary quantifiers are related by a commuting diagram: Substitution of a term for a variable in a quantified assertion is provided by the lemmas: These lemmas rely on a semantic definition of independance w.r.t. some variable: Back to First order logic or Contents or top.

Well formed formulas of first order logic

So far, we have studied and represented first order logic by expliciting semantic constructors of terms or assertions. Term constructors are obtained by lifting Dom operators, similarly for assertion constructors. Quantifiers have been defined and may also be considered as assertion constructors. We have not mentionned first order logic syntax, whereas classical text books on first order logic start with the syntax of "well formed formulas".

Well formed formulas are characterized as an inductive subset of the set of assertions. Technically, we first define "well formed terms" inductively under the name of "wterm?" (PVS allows such inductive definitions of sets); we then inductively define a notion of "well formed formula" which is relative to a set of terms: "twff?".

The set "wff?" of well formed formulas is then defined by:

All these definitions are available in "fol" library "fol" theory.

Interestingly enough, our notion of "well formed formula" is independant of any basis of function and predicate symbols, in contrast with classical frameworks.

It turns out that a definition of well formed formulas is actually not used by our theory of imperative program verification. But the only examples we are able to write down fit in this context.

Back to First order logic or Contents or top.

Finite height logic and first order logic

As we saw, formal substitution in a quantified assertion is related to a notion of independance w.r.t. some variable.

A related notion (which relies upon our assumption that variables are numbered) is term or assertion height. Intuitively, the height of an expression e is the highest rank of a variable V such that e depends upon V. Some expressions do not have a finite height, because they depend on variables of arbitrarily high rank. An example of such an expression, consider the assertion

where the domain Dom is nat and "v(i)" denotes the ith variable.

We define a relational notion of height (still denoting "v" the one-to-one mapping between "nat" and "variable":

An expression which has a height (according to "height?") is said to have finite height.

A (logical) language is defined as a pair of a set of terms and a set of assertions. We thus have two languages:

which is the language of well formed terms and formulas, and which is the language of finite height terms and assertions.

We have shown some properties of these languages:

The reader can check "fol" library "language", "fol", "fhl" and "fol_fhl_subset" theories for the formalization and proofs of these results.

Back to First order logic or Contents or top.

Program verification

As we already explained, a program is a total function from env to env. Our PVS version of L2 language consists un four program constructors: set, if_then_else, while, @@.

Each constructor is defined as a PVS function. For each constructor, we have proved the corresponding Hoare rule. The notion of program correctness is defined in "imperative" library "program_correctness" theory:

Remember that the "IMPLIES" used here is not PVS native "IMPLIES: [bool,bool -> bool]"; it is a lifted version with implicit universal quantification over environments: its type is "[assertion, assertion -> bool]".

The consequence Hoare rule is established in the same theory.

The "if_then_else" and "@@" constructors are relatively barren. The other constructors require more attention:

The set assignment constructor

The "set: [variable, term -> program]" constructor is defined as follows: We have proved the corresponding Hoare rule: In fact, we have also proved that there is no other way to define "set" so that the assignment Hoare rule holds. In other words, the assignment Hoare rule is a characterization of assignment semantics. Some authors use Hoare rules (or the like) to define the semantics of a programming language: this is the case of Abrial ("the B book"). We have shown that this is justified in this particular case (see "imperative" library "assignment_statement" theory for details).

Back to Program verification or Contents or top.

The while loop constructor

Recall that H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß define "while" inductively in their report entitled "Mechanized Semantics of Imperative Programming Constructs", in a context where programs are defined as relations among environments (not functions). Note that they did not use PVS inductive definition facility, which was not available at the time, but had to build a fixpoint theory to define "while" as a least fixpoint.

In contrast with them, we define "while" as a total PVS recursive function: this may look like a paradox, since it is well known by programmers that while loops do not always terminate!

The definition of "while" as previously introduced is achieved incrementally, in four steps.

The first step defines "while: [term, program -> program]". The trick is to restrict "while(test, loop)" to "loop" programs that decrease the environment according to some well founded relation "R" whenever the "loop" is executed, that is, for environments satisfying "test". Here is the recursive definition available in "imperative" library "while_statement" theory:

Note the use of a dependant type: the type of "loop" depends on "test"; it also depends on "R" which is a parameter of "while_statement" theory, assumed of type "(well_founded?[env])". This same "R" is used in the "BY" clause of the recursive definition. PVS ability to turn predicates into subtypes seems crucial here, to make such a definition possible. The while Hoare rule is proved in this same "while_statement" theory.

The "decreases?" predicate is defined in "program_termination" theory by:

The second step achieved by "rwhile_statement" theory eliminates the "R" theory parameter by making it an explicit parameter of the "while" function (which was not possible from the outset): The third step achieved by "riwhile_statement" theory introduces an invariant "i" as an explicit parameter of the "while" function, and combines "correct?" and "decreases?" predicates into a single predicate named "corrdecr?" and used to restrict the type of "loop" so as to enforce termination: The fourth and last step achieved by "rivwhile_statement" theory introduces a variant as an explicit parameter of the "while" function, and defines a notion of termination entirely in terms of correctness, which is proved to be equivalent to the previous ones: The idea behind the above new definition of "corrdecr?" is to replace termination with the correctness goal: Here is the final version of the "while" Hoare rule, as it is used in "standard_verification" theory: Back to Program verification or Contents or top.

Library dumps

There are two libraries which should be installed as subdirectories "fol" and "imperative" of a common directory, which we chose to name "pvs", but this name is unimportant. For each library, there are two versions: please select the appropriate one according to the version of PVS you are using.
 
for PVS 2.2 (patch level , 1.29)
for PVS 2.3
"fol" library dump
fol.dump.june_14_1999
fol.dump.28_november_1999
"imperative" library dump
imperative.dump.june_14_1999
imperative.dump.28_november_1999

All dumps are available from directory "pvs/dumps" or "pvs/2.2/dumps" for the older version. Note that all proofs were performed on a Thinkpad 380ED machine, with 64 mégabytes of main storage, and 100 mégabytes of swap space, under Redhat Linux.

To install and test these libraries on your site, use the following steps:

  1. Create directories "fol" and "imperative" at the same level;
  2. Place a copy of "fol.dump.<date>" dump in your "fol" directory, and a copy of "imperative.dump.<date>" in your "imperative" directory, where <date> stands for "june_14_1999" or "28_november_1999";
  3. Start PVS from the "fol" directory, and accept creation of a new context ;
  4. Undump file "fol.dump.<date>" using the "Meta-x undump-pvs-files" PVS command;
  5. Load "dump" theory which is the root of everything in an Emacs buffer using the "Ctrl-c Ctrl-f" PVS command;
  6. Prove everything using the "Meta-x prove-importchain" PVS command: this will take several minutes, and display a PVS Status buffer with a total of 196 succeeded proofs out of 196 attempted (see PVS Status buffer for older version);
  7. Exit PVS and restart it from the "imperative" directory, accepting creation of a new context (alternatively, use the "Meta-x change-context" PVS command to switch to "../imperative" context);
  8. Undump file "imperative.dump.<date>" using the "Meta-x undump-pvs-files" PVS command;
  9. Load "dump" theory which is the root of everything in an Emacs buffer using the "Ctrl-c Ctrl-f" PVS command;
  10. Prove everything using the "Meta-x prove-importchain" PVS command: this will take several minutes, and display a PVS Status buffer with a total of 179 succeeded proofs out of 179 attempted (178 proofs for older version: see PVS Status buffer).
You are ready to check the six examples, or write your own. To refer to this work, please use url. Thank you for your comments.

Back to Contents or top.

Acknowledgement

I thank Julien Nguyen for a first contribution to this work (DEA project, spring 1996) as an E.N.S.E.R.B. student, and Rodolphe Pueyo, for subsequent contribution (DEA project, spring 1997) as a Bordeaux I University student. I thank my colleague François Pellegrini for making Redhat Linux 5.0 work on my Thinkpad, on top of which I was able to install PVS 2.2. Then my colleagues François Pellegrini and David Sherman worked hard to install Redhat 6.0, so that PVS 2.3 could run. Proofs run so fast on this machine that it is a real pleasure to use PVS.

Back to Contents or top.


© Copyright 1999 Paul Y Gloess