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:
-
L1, the language of "flowcharts", featuring "if then else" , parallel assignment
"x1, ..., xn := t1, ..., tn" and "goto";
-
L2, the "while statement" language, featuring sequential composition ";",
"if then else", single assignment "x := t" and "while".
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:
-
env: TYPE = [nat -> Dom];
-
term: TYPE = [env -> Dom];
-
assertion: TYPE = [env -> bool];
-
program: TYPE = [env -> env].
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:
X: variable ("variable" is a subtype of "term" as explained below);
t, v: term;
e, i, comment: assertion;
r: [Dom, Dom -> Bool] (more precisely: r:(wellfounded?[Dom]));
S, S1, S2: program.
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:
variable: TYPE = {v: term | (EXISTS (i: nat): v = (LAMBDA (sigma: env):
sigma(i)))} .
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:
set(Y1, X) @@
set(Y2, 1) @@
while(lti, 201+21*Y2-2Y1,
Y1<=111 AND Y2>=1 AND ((Y1>=101 AND equals(Y2,1)
IMPLIES equals(Y1,101)))
(Y1<=100 OR (Y1>100 AND diff(Y2,1))
,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)
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:
correct?(X<=100, f91, Z=91) .
We have actually proved this formula (named "f91_correct: LEMMA" in our
"f91_example" theory). The PVS
proof script
("" (EXPAND "f91") (HFA))
only takes two commands:
-
(EXPAND "f91") replaces "f91" with its actual definition, as given above;
-
(HFA) invokes our HFA most powerful strategy, which combines three steps:
-
(HOARE) applies Hoare rules until nomore rule is applicable, and turns
termination goals arising from application of the "while" Hoare rule into
"correct?" goals, to which it recursively applies the HOARE strategy. HOARE
thus acts as a verification condition generator: it automatically yields
goals of the form
where "a" is an assertion. The universal quantifier is actually implicit,
so that the assertions thus generated are readable, and exactly correspond
to assertions one would generate by hand;
-
(FOL) skolemizes the implicit "s" variable, and goes down from the abstract
level of assertions to the concrete level of closed formulas which no longer
contain any abstract term or assertion constructor: typically, these are
boolean formulas on concrete atoms written using function or predicate
symbols of the basis B, and constants of the form X(s), where X is a variable
occurring in the original program or in its specification. Constants of
type Dom, of the form "d", "d!1", ..., may also arise, due to termination
goals;
-
(ARITHMETICS) combines PVS arithmetics and boolean decision procedures
with additional rules of arithmetics, among whichs some rules about exponentiation
("**").
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*)
|
->
|
two_power_example
|
Back to Contents or top.
Factorial example
Here is the "factorial" program as defined in PVS:
= while(lti, N,
equals(R*fac(N),R0*fac(N0)))
It computes R0*N0! into R, where R0 and N0 are the initial values of R
and N, according to the specification:
factorial_correct: LEMMA
correct?(equals(N,N0) AND equals(R,R0), factorial, equals(R, R0*fac(N0)))
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:
fac: [term -> term] = l(fac) .
The proof of "factorial_correct" lemma requires three steps:
-
(EXPAND "factorial") replaces "factorial" with its definition in the "correct?"
goal;
-
(AUTO-REWRITE "fac") is a hint to the prover that "fac" should be expanded
sometime in the course of the proof, using its recursive definition;
-
(HFA) invokes our most powerful program verification strategy,
which combines Hoare rules, first order logic and arithmetics with PVS
decision procedures to prove "correct?" goals.
The reader of the factorial_example
PVS theory will notice the
factorial_termination: SUBLEMMA
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:
lti(i, j: int): bool = (i>=0 AND i<j)
.
Precisely, expanding the "terminates?" predicate yields two subgoals:(using
L2 rather than PVS syntax for easier reading):
-
[R*fac(N)=R0*fac(N0) ^ N>0] R := R*N;
N := N-1 [R*fac(N)=R0*fac(N0)],
-
[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:
-
The exact same formula is raised by PVS as a TCC upon type-checking the
"factorial" program, because of the type of the "while" loop as defined
in "rivwhile_statement"
theory: we prefer to make this TCC explicit, since it is often the heart
of the correctness proof;
-
This same formula is raised a second time by PVS as a TCC, in the course
of the proof of the "factorial_correct" lemma, upon applying a "while"
Hoare rule. For more complex programs, see "gcd"
or "2**a" for example, we prefer not to
repeat the termination proof and use the termination lemma in the correctness
proof.
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:
f91_correct: LEMMA correct?(X<=100, f91, equals(Z, 91))
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:
-
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,
+, -, *, ...);
-
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;
-
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:
(FORALL (x1: t1, ..., xk:tk): h1 ^ ... ^ hk => lhs = rhs)
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:
-
[p] s [q], where s is a single statement: in this case, we provide a combination
of the Hoare rule relevant of the kind of statement s, and the consequence
Hoare rule, so that a subgoal of the form "p => wlp(s,q)" arises among
others;
-
[p] S; s [q], where s is the last statement of the program "S; s": in this
case we provide a combination of the Hoare rule relevant of the kind of
statement s, and the sequential composition Hoare rule, so that a goal
of the form [p]S[wlp(s,q)] arises among others.
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:
alt(x,t)(l(f)(e1, ..., ek)) = l(f)(alt(x,t)(e1), ..., alt(x,t)(ek))
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:
alt(x,t)(x) = t ,
x/=y IMPLIES alt(x,t)(y) = y .
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)) .
|
|
|
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:
|
|
(FA)
|
Equivalent to
(then (FOL) (ARITHMETICS)) .
|
|
(GROUND*)
|
Repeatedly applies PVS linear arithmetics and boolean decision procedures.
Equivalent to
|
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:
[A>0 AND B>0 AND gcd?(A, B, D)] gcd [equals(A, D)]
The "gcd?" used here is the abstraction "l(gcd?)" of the concrete "gcd?"
defined in PVS by:
gcd?(a, b, d: int): bool = cd?(a,b,d) AND (FORALL (dd: int): cd?(a,
b, dd) IMPLIES dd <= d)
with
cd?(a, b, d: int): bool = divides?(d, a) AND divides?(d, b)
divides?(d, n: int): bool = (EXISTS (q: int): n = d*q)
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:
A 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
foreach: [variable, assertion -> assertion]
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
alt: [variable, term -> [expr -> expr]]
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:
-
environment modifiability: for each "sigma: env", "X: variable",
"d: Dom", there exists "sigma': env" such that "V(sigma')=V(sigma)" for
all "V: variable" with "V/=X", and "X(sigma')=d";
-
environment determinism: for each "sigma1, sigma2: env", we have
"sigma1=sigma2" provided that "V(sigma1)=V(sigma2)" for all "V: variable".
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
alt: [variable, Dom -> [env -> env]]
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:
alt: [variable, term -> [expr -> expr]] .
Our definition of substitution is:
e[X/t](sigma) = e(sigma[X/t(sigma)])
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:
lambada: [variable, expr -> [term -> expr]]
by the equation:
lambada(X,e)(t) = e[X/t] .
The price we had to pay in exchange was the proof of:
(l(f)(e1, ..., ek))[X/t] = l(f)(e1[X/t], ..., ek[X/t])
where "l" is our lifting function. Recall two simple lemmas:
X[X/t] = X ,
X/=Y => Y[X/t] = Y .
Back to First order logic or Contents
or top.
Quantifiers
Universal and existential quantifiers are defined as functions. We have
two versions:
-
unary quantifiers, which apply to lambda-abstractions,
have the type:
[[variable, assertion -> [term -> assertion]]
->
assertion] ;
-
binary quantifiers, traditionnally apply to a variable and assertion, and
have the type:
[variable, assertion -> assertion] .
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):
foreach(X: variable, a: assertion): assertion
= (LAMBDA (sigma: env):
(FORALL (d: Dom): a(alt(x, d)(sigma))))
;
thereis(X: variable, a: assertion): assertion
= (LAMBDA (sigma: env):
(EXISTS (d: Dom): a(alt(x, d)(sigma))))
.
The binary and unary
quantifiers are related by a commuting diagram:
binary_unary_foreach: LEMMA
foreach = foreach
o lambada ;
binary_unary_thereis: LEMMA
thereis = thereis
o lambada .
Substitution of a term for a variable in a quantified assertion is provided
by the lemmas:
foreach_alt: LEMMA
(FORALL (X, Y: variable, a: assertion, t: term):
IMPLIES alt(Y,t)(foreach(X,a)) = foreach(X,alt(Y,t)(a))) ;
thereis_alt: LEMMA
(FORALL (X, Y: variable, a: assertion, t: term):
IMPLIES alt(Y,t)(thereis(X,a)) = thereis(X,alt(Y,t)(a))) .
These lemmas rely on a semantic definition of independance w.r.t. some
variable:
indep?(X: variable)(e: expr): bool
= (FORALL (d: Dom, sigma: env):
e(alt(X,d)(sigma)) = e(sigma)) .
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:
wff?: [assertion -> bool] = twff?(wterm?) .
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
(LAMBDA (sigma: env): (FORALL (i: nat): v(i)(sigma) = 0)): 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":
height?(e: expr)(h: nat): bool
= (FORALL (n: nat): n>h IMPLIES indep?(v(n))(e)) .
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:
fol: language
= (# terms := wterm?, assertions := wff? #) ,
which is the language of well formed terms and formulas, and
fhl: language
= (# terms := fh_term?, assertions := fh_assertion?
#) ,
which is the language of finite height terms and assertions.
We have shown some properties of these languages:
-
fol is the smallest language containing variables, stable by all abstract
constructors (including quantifiers);
-
fol is stable by substitution;
-
fhl is stable by substitution and all abstract constructors;
-
fol is a subset of fhl.
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:
correct?(input_assertion: assertion, S: program, output_assertion:
assertion)
: bool
= input_assertion IMPLIES (output_assertion o S) .
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:
set(X: variable, t: term)(sigma: env): env
= alt(X, t(sigma))(sigma) .
We have proved the corresponding Hoare rule:
assignment_hoare_rule: LEMMA
(FORALL (a: assertion, X: variable, t: term):
correct?(alt(X,t)(a), set(X,t), a)) .
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:
decreases?(R: [env,env -> bool])(p: assertion)(S: program): bool
= (FORALL (sigma: (p)): R(S(sigma),sigma)) .
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):
IMPORTING while_statement
while(R: (well_founded?[env]))
: [test: assertion, (decreases?(R)(test)) ->
program]
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:
IMPORTING rwhile_statement[environment]
corrdecr?(R: [env, env -> bool]) (p, q: assertion) (S: program)
: bool = (correct?(p, S, q) AND decreases?(R)(p)(S)) ;
while(R: (well_founded?[env]), i: assertion)
(test: assertion, loop: (corrdecr?(R)(i AND test, i)))
: program = while(R)(i AND test, loop) .
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:
IMPORTING riwhile_statement[environment]
corrdecr?(R: [Dom, Dom -> bool], variant: term)
(a, b: assertion)
(S: program)
: bool
= correct?(a, S, b) AND
(FORALL (d: domain):
correct?(a AND equals(variant, l(d)),
S,
l(R)(variant, l(d)))) ;
terminates?(R: (well_founded?[Dom]),
variant: term, invariant: assertion)
(test: assertion)
(S: program)
: bool
= corrdecr?(R, variant)(invariant AND test, invariant)(S) ;
trel(R: [Dom, Dom-> bool])(t: term)(sigma1, sigma2: env): bool
= R(t(sigma1), t(sigma2)) ;
while(<: (well_founded?[Dom]),
variant: term,
invariant: assertion)
(test: assertion,
loop: (terminates?(<, variant, invariant)(test)))
: program
= while(trel(<)(variant), invariant) (test, loop) .
The idea behind the above new definition of "corrdecr?" is to replace termination
with the correctness goal:
[invariant & test & variant = d] loop [invariant & variant
< d] .
Here is the final version of the "while" Hoare rule, as it is used in "standard_verification"
theory:
(FORALL (<: (well_founded?[Dom]), i, e: assertion,
v: term,
S: (terminates?(<, v, i)(e))):
correct?(i, while(<, v, i)(e, S), i AND NOT e)) .
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.
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:
-
Create directories "fol" and "imperative" at the same level;
-
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";
-
Start PVS from the "fol" directory, and accept creation of a new context
;
-
Undump file "fol.dump.<date>" using the "Meta-x undump-pvs-files" PVS
command;
-
Load "dump" theory which is the root of everything in an Emacs buffer using
the "Ctrl-c Ctrl-f" PVS command;
-
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);
-
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);
-
Undump file "imperative.dump.<date>" using the "Meta-x undump-pvs-files"
PVS command;
-
Load "dump" theory which is the root of everything in an Emacs buffer using
the "Ctrl-c Ctrl-f" PVS command;
-
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
http://dept-info.labri.u-bordeaux.fr/~gloess/imperative
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