P. Cousot & R. Cousot, Reasoning about program invariance proof methods

Patrick Cousot and Radhia Cousot
Reasoning about program invariance proof methods
Research Report CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980, 22p.

Abstract:
      We present a mathematical model based on dynamic discrete transition systems for constructing, explaining, verifying, comparing, optimizing and transforming program proof methods. We are particularly interested in invariance properties of parallel programs such as partial correctness, absence of global deadlock or non-termination which consist in characterizing a super-set of the possible descendents of the valid initial states.
      We first characterize invariance properties using fixpoints and next derive the fundamental sound and complete invariance proof method. Proving the invariance of an assertion Ψ consists in showing that some global invariant I stronger that Ψ is true for the valid entry states and remains true after any transition. Known invariance proof methods (Floyd, Hoare, Naur,... for sequential deterministric programs; Clarke, Clint,... for coroutines; Howard,... for monitors; Ashcroft, Ahscroft & Manna, Hoare, Keller, Lamport, Mazurkiewicz, Newton, Owicki & Gries,... for parallel programs with shared variables; Apt, Francez & De Roever, Cousot & Cousot, Levine, ... for communicating sequential processes à la Hoare;...) all reduce to the fundamental invariance proof method and differ only because they use different decompositions of the global invariant into local assertions attached to program control points.
      We formalize this notion of decomposition by means of Galois connections, the mathematical properties of which are reminded. We next show that a given decomposition of the global invariant into local assertions associated with program control points can lead to a complete lattice of distinct verification conditions. In order to illustrate this point, we propose several variants of the Lamport-Owicki proof rules. All these variants are sound and complete although some of them require stronger invariants than others. Invariance proof methods which have been designed for very different languages can nevertheless be compared by showing that they rely on similar decompositions of the global invariant. It is also remarked that some decompositions lead to sound but intrinsically incomplete proof methods when the correspondance between the global invariant and its decomposition is not one-to-one for all programs.
      We next introduce the notion of reduction/extension of a dynamic discrete transition system in order to formalize the transformation of a program by introduction of auxiliary variables so that the assertions interleaved in the program text need not explicitly mention program control points.
      We finally compare our approach with other formalisms for reasoning about program proof methods in particular program logics.

Résumé:
      Nous présentons un modèle mathématique basé sur les systèmes dynamiques à transitions discrètes permettant de construire, expliquer, vérifier, comparer, optimiser et transformer les méthodes de preuve de propriétés des programmes. Nous nous intéressons particulièrement aux propriétés d'invariance des programmes parallèles comme la correction partielle, l'absence d'interblocage global ou la non-terminaison, qui consistent à caractériser un sur-ensemble des descendants possibles des états d'entrée.
      Après avoir caractérisé les propriétés d'invariance par point-fixe, nous montrons que la méthode fondamentale de preuve d'invariance d'une assertion Ψ consiste à découvrir une assertion plus forte I qui est vraie pour les états initiaux et reste vraie après une transition quelconque. Les méthodes connues de preuve d'invariance (Floyd, Hoare, Naur,... pour les programme séquentiels déterministes; Clarke, Clint,... pour les coroutines; Howard,... pour les moniteurs; Ashcroft, Ahscroft & Manna, Hoare, Keller, Lamport, Mazurkiewicz, Newton, Owicki & Gries,... pour les programmes parallèles partageant des variables communes; Apt, Francez & De Roever, Cousot & Cousot, Levine, ... pour les processus communicants à la Hoare;...) se ramènent à la méthode fondamentale et ne diffèrent que par des décompositions différentes de l'invariant global en des assertions locales associées aux différents point de contrôle du programme.
      Après avoir formalisé cette décomposition au moyen de connections de Galois dont nous rappelons les propriétés mathématiques, nous montrons qu'une même décomposition de l'invariant global en des assertions associées aux points de contrôle du programme peut donner lieu à des règles de vérification distinctes formant un treillis complet. Nous illustrons ce résultat en proposant quelques variantes de la méthode de Lamport-Owicki, qui sont toutes correctes et complètes bien que certaines d'entre-elles nécessitent l'emploi d'invariants plus forts que d'autres. Des méthodes de preuves d'invariance ayant été conçues pour des langages très différents peuvent également être comparées en montrant qu'elles sont fondées sur des décompositions similaires de l'invariant global. Nous remarquons également que certaines décompositions conduisent à des méthodes qui sont correctes mais intrinsèquement incomplètes quand la correspondance entre l'invariant global et sa décomposition n'est pas injective pour tous les programmes.
      Nous introduisons ensuite la notion de réduction/extension de systèmes dynamiques à transitions discrètes qui permet de formaliser la transformation d'un programme par introduction de variables auxiliaires afin d'éviter de mentionner explicitement les points de contrôle du programme dans les assertions.
      Finalement, nous comparons notre approche pour raisonner sur les méthodes de rpeuve de programmes avec d'autres formalismes, notamment les logiques de programmes.
.pdf (17.1 Mb, to be read with Acrobat Reader)

Bibliographic reference:

\bibitem{Cousot-CRIN-80-P050-jul-1980}
P.~Cousot and R.~Cousot.
\newblock Reasoning about program invariance proof methods.
\newblock Research report CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), 
Institut National Polytechnique de Lorraine, Nancy, France, July 1980, 22p.

@TECHREPORT{CousotR-CRIN-80-P050-jul-1980,
   author =    {R.~Cousot},
   title =     {Reasoning about program invariance proof methods},
   type =      {{R}es{.} rep{.}},
   number =    {CRIN-80-P050},
   institution =  {Centre de Recherche en Informatique de Nancy (CRIN), 
                   Institut National Polytechnique de Lorraine},
   address =   {Nancy, France},
   pages =     22,
   month =     jul,
   year =      1980,
}

Copyright notice
Last modified: Monday, 12-Dec-2011 20:50:10 CET