Sémantique
et Preuve de Programmes
lundi 14h-17h salle TD5
created october 25, 2002
last version december 13, 2002
Contents
Mediathèque
Back to Top.
Session 1: Monday October 7, 2002 - Room TD 5
Introduction to the course. Purpose of the course: learn how to formalize
knowledge, in a typed higher order logic such as PVS.
Evaluation will be based upon
-
50%: participation of students in a cooperative project (see syllabus
for details),
-
50%: team mini-project: analysis of a small PVS theory, and a 30 minutes
oral presentation on Friday february 8, 2002.
As an introduction to formal specification and proof methods, we
study the PVS specification and proof of correctness and completeness of
a simple program for computing a solution to "le compte est bon" problem:
~gloess/pvs/2.4/count_ok/2.4.count_ok.12mar2002.dump.dump
This example (to be restored into a ~user/pvs/count_ok/ directory)
also illustrates PVS ground evaluator. This is a classical Scheme or Common
LISP exercise.
One student asked whether it would be possible to prove that the count_ok
function is optimal, meaning that it always yields an optimal solution.
Answer: we would have to specify what "optimal" means. For
example "optimal" could mean "the shortest possible solution" (shortest
length). The count_ok function as it is is probably not optimal.
PVS language
(slides 1--9).
Back to Top.
Session 2: Monday October 14, 2002 - Room TD 5
PVS language
(slides 10--27), up to well founded relations and recursive functions.
Rapid look at the "imperative
program verification library", showing the proof of correctness of
the "sqrt" example. This big library demonstrates the expressive power
of PVS, which allowed us to actually define program correctness, develop
and prove Hoare calculus, and corresponding strategies that provide a semi-automatic
proof method.
Back to Top.
Session 3: Monday October 21, 2002 - Room TD 5
We first take a closer look at the PVS proof of the theorem
There is no bijection from A to [A -> bool] (in classical math,
from A to 2A).
that was done in "Ateliers" class. We compare three proofs, see:
~gloess/pvs/2.4/2.4.sets.21oct2002.bij.dump
We then go back to recursive functions and well founded induction:
-
PVS language
(slides 24--27): recursive functions and well founded relations;
-
PVS inference
(slides 28--29): well founded induction principle.
We then study inductive sets:
We finally take a closer look at imperative
program verification library, with emphasis on specification method:
-
"no syntax" approach to formalization of imperative programs, assertions,
-
variables, terms, programs and assertions are directly semantic objects,
-
assignment Hoare rule, formal substitution defined semantically, subsumes
"substitution theorem",
-
while statement and while Hoare rule: while is defined as a recursive function
(owing to dependant types).
Back to Top.
Session 4: Monday October 28, 2002 - Room TD 5
Répartition de bibliothèques PVS à étudier
par petit groupes (en vue de l'évaluation): aller vers evaluation
pour la liste.
Fixpoint theory and PVS inductive sets.
Back to Top.
Session 5: Monday November 4, 2002 - Room TD 5
We study a PVS formalization
of well founded recursion.
Then last year
Alose project results are presented.
Thus, last year project main result was a fixpoint semantics of Alose
(in the style of Prolog fixpoint semantics): all lemmas and proof obligations
were completely proved.
This year, we'll aim at providing Alose with an operational semantics
(a semantics that can be evaluated using PVS ground evaluator), and proving
the equivalence between this operational semantics and the former fixpoint
semantics.
Some additional work toward this goal was done by Paul Y Gloess,
in april 2002:
Back to Top.
Session 6: Monday November 18, 2002 - Room TD 5
Previous session was dedicated to a presentation of Alose, and its
PVS declarative (fixpoint) semantics (as defined last year), and of the
library of confluent relations (subsequently introduced) that will now
turn out to be useful.
The present goal (this year) - only two sessions are left! -
is twofold:
-
define an operational semantics for Alose, that is, a semantics that can
be checked using PVS ground evaluator (which resembles a LISP evaluator);
-
show the equivalence between
-
Alose declarative semantics,
-
and Alose operational semantics,
using the "unique normal form" theorem which applies to confluent relations.
After doing some general purpose tests with PVS ground evaluator,
we concluded that:
-
sets are not appropriate (even if we restrict ourselves to finite sets)
and should be mapped into lists;
-
we should use a concrete representation of rules and scripts, where sets
are replaced with lists;
-
equivalence between the declarative and operational semantics should take
this mapping into account, and should assume a finite set of finite
rules (infinite objects are not operational).
Results
-
two operational types have been defined:
-
orule corresponding to rule;
-
oscript corresponding to script;
-
operational inference has been implemented in oinference
theory:
-
application of a rule requires two auxillary functions:
-
assoc for getting the birthdate of an event
in a script;
-
a recursive apply function to check each rule
condition against the script, and accumulate a maximum delay;
a potential problem (to be improved later) is that the property "script
defines each event once only" is not maintained, because we used cons
instead of a more sophisticated function to add something to the script;
-
application of a list of rules to a script is straightforward;
-
iterated application of a list of rules to a script uses an operational
fixpoint (omu function in ofixpoint
theory):
-
termination of omu_prec function will have
to be refined, as it will raise unprovable importing TCCs!
-
PVS dumps:
Back to Top.
Session 7: Monday December 2,
2002 - Room TD 5
We first completed and improved PVS operational semantics (oinference
theory) and added some tests for the PVS ground evaluator in the oinference_eval
theory:
-
instead just consing the event (e, n) corresponding to successful application
of a rule to the script s under consideration, we first check that (e,
n) does not already belong to script s; otherwise, if some pair (e, n')
already belongs to s, we replace it with (e, min(n, n'));
-
implementation from Thomas Chatain, see comb
function in oinference theory;
-
with the above improvement, the operational fixpoint omu
used in fc terminates; furthermore, the result
does not seem to depend upon rule ordering;
We then take another look at ofixpoint
operational fixpoint theory:
-
omu or omu_prec
parameters do not restrict the type [T->T] of f function. Hence, there
will be no way to prove omu_prec termination
TCC, since nothing says that f(start) is smaller than start with respect
to R well founded relation (passed as a parameter of ofixpoint
theory);
-
in order to get a provable termination TCC, we restrict the type of f to:
-
f: {f: [T -> T] | (FORALL (start: T): f(start) = start OR R(f(start),
start))} ;
-
hence, either start is a fixpoint of f, or f(start) will get smaller than
start w.r.t. R;
-
this turns out to work better, although the termination TCC is still unprovable!
-
the reason is that since f is the first theory parameter, it cannot depend
on prec parameter; alternatively, we'll need to express some relation between
prec and start parameters; we postpone the problem;
We finally formalize our main goal, which is to prove the correctness
of Alose operational forward checking w.r.t. Alose declarative forward
checking semantics:
-
we define a correspondance alpha (abstraction) from declarative concepts
to operational concepts:
-
the essential idea is to map each list into a (finite) set, using the list2set
converter provided in PVS prelude;
-
alpha(s: oscript): script = list2set(s) % see oscripts
theory;
-
alpha(R: orule): orule % defined in orules
theory;
-
alpha(Rs: list[orule]): [rule -> bool] = list2set(map(alpha, Rs)) % see
orules
theory;
-
the main correctness theorem, see oinference theory, is:
fc_correct: THEOREM
(FORALL (Rs: list[orule]): alpha(fc(Rs)) = fc(alpha(Rs)))
;
Resulting PVS dump:
~gloess/pvs/2.4/alose/2.4.alose.3december2002.dump.dump
Finally, I give a sketch of a manual proof of the above correctness
theorem (sunday afternoon work in Lacanau Ocean):
-
I have come up to the conclusion that the theory of confluent rewriting
systems would not help here, because we would need a unique relation R
for both the declarative semantics and the operational semantics, so that
we can get two normal forms
-
empty script --R*--> s1 (irreducible) through declarative semantics;
-
empty script --R*--> s2 (irreducible) through operational semantics;
and use the "unique normal form" theorem to equate s1 and s2. However,
although we can easily define a relation R suitable for operational inference
(R corresponds to application of a delay rule from the list Rs of rules),
and we have
alpha(s) --R*--> alpha(pi(Rs)(s)),
this relation R does not work for declarative inference. We do not have
alpha(s) --R*--> lub(alpha(Rs))(alpha(s)).
In fact operational inference does not closely match declarative inference:
it is more efficient! In general:
alpha(pi(Rs)(s)) > lub(alpha(Rs))(alpha(s)).
-
Hence the correctness proof will be based on fixpoint theory itself, rather
than on the theory of confluent rewriting systems:
-
Let Fs = {apply(r1), ..., apply(rn)} be the finite set of functions {f1,
..., fn} corresponding to the delay rules {r1, ..., rn};
-
We have three fixpoint semantics:
-
mu(lub(Fs)) where lub(Fs) can be understood as f1 U ... U fn, where (f
U g)(s) is defined as f(s) U g(s): this is the declarative semantics;
-
mu(pi(Fs)) where pi(Fs) denotes the composition product f1 o ... o fn of
the list (: f1, ..., fn :) of functions: this is not strictly speaking
the operational semantics, because we use the theoretical mu instead of
the operational omu, but it is close to;
-
omu(pi(Fs)): the operational semantics;
-
The proof requires two main steps:
-
mu(lub(Fs)) = mu(pi(Fs)):
-
mu_lub_mu_pi manual proof,
using related lemmas:
-
mu is monotonic, see mu_monotonic
manual proof;
-
I < f AND k > 1 => mu(fk)
= mu(f), see mu_power manual proof;
-
mu(I U f) = mu(f), see mu_refl
manual proof;
-
mu(pi(Fs)) = omu(pi(Fs)):
-
this should be easily achieved by showing that R is noetherian, and using
the monotonicity of pi(Fs);
All hand-written proofs.
Back to Top.
Session 8: Evaluation Monday
December 16, 2002 - Room TD 5
Voici une liste de bibliothèques ou théories PVS à
étudier par petits groupes de 3 élèves, ou 6 élèves
(2 groupes de 3), selon l'importance du sujet.
Le travail demandé à chaque élève est de
l'ordre de 3 à 4 heures (hors soutenance orale de 30 minutes par
groupe de 3):
-
analyse d'une partie de la bibliothèque étudiée;
-
approfondissement de certaines preuves essentielles (extraction de l'idée
de la preuve à partir du scénario PVS);
-
synthèse et préparation de l'exposé.
La soutenance a pour but de faire comprendre à l'auditoire médusé
le rôle de la bibliothèque étudiée. On n'attachera
pas trop d'importance à la présentation: elle peut se faire
au tableau et à la craie, sans transparents.
Une liste de sujets d'étude est proposée ci-dessous: il
est demandé à l'ensemble des élèves (et au
représentant en particulier) de me proposer par mail une répartition
nominative, d'ici lundi 21 janvier 2002. Un autre sujet peut être
étudié, avec mon accord.
Back to Top.
© Copyright 2001-3000 Paul
Y Gloess
