Nous essayons tout d'abord d'exprimer l'essence d'une méthode de preuve à l'aide de principes d'induction. Quand c'est fait, nous en déduisons la correction et la complétude sémantique. Nous cherchons ensuite l'équivalence forte c'est-à-dire qu'une preuve par une méthode peut se réécrire en une preuve par une autre méthode. Nous nous efforçons également de généraliser ces principes d'induction, en particulier au cas de comportement à des ensembles de traces non clos. C'est le cas des hypothèses d'exécution faiblement équitables pour les programmes parallèles que nous prenons en exemple dans ce rapport. Finalement, nous étudions comment adapter une méthode de preuve à un langage particulier en partant d'une sémantique opérationnelle de ce langage et d'un principe d'induction formalisant la méthode de preuve.
We first try to express the essence of a proof method by an induction principle. Once done, we derive the soundness and relative completeness of the proof method. We then look for strong equivalence results in order to show that a proof by one method can be rewritten into a proof by another method. We also try to generalize these induction principles, in particular to the case of non closed sets of traces. This is the case of the weak fairness hypotheses on parallel program execution that we consider as the basic example in this paper. Finally, we study how to adapt a proof method to a particular language starting from an operational semantics of this language and from an induction principle formalizing the proof method.
\bibitem{CousotCousot85-ATP-CNRS-PCS} P{.} Cousot and R{.} Cousot. \newblock Principe des M{\'e}thodes de Preuve de Propri{\'e}t{\'e}s d'Invariance et de Fatalit{\'e} des programmes Parall{\`e}les. \newblock In \emph{Parall{\'e}lisme, communication et synchronisation}, J.-P{.} Verjus et G{.} Roucairol (Eds.), {\'E}ditions du CNRS, Paris, pp{.} 129--149, 1985, ISBN 2-222-03672-0. @inproceedings{CousotCousot85-ATP-CNRS-PCS, author = {Cousot, P{.} and Cousot, R{.}}, title = {Principe des M{\'e}thodes de Preuve de Propri{\'e}t{\'e}s d'Invariance et de Fatalit{\'e} des programmes Parall{\`e}les}, booktitle = {Parall{\'e}lisme, communication et synchronisation}, editor = {J.-P{.} Verjus and G{.} Roucairol }, publisher = {{\'E}ditions du CNRS, Paris}, pages = {129--149}, year = {1985, ISBN 2-222-03672-0}, }
Monday, 04-Jan-2010 12:42:50 CET