Deriving Proof Rules Form Continuations Semantics

Philippe Audebaud (1) , Elena Zucca (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

We claim that the continuation style semantics of a programming language can provide a starting point for constructing a proof system for that language. The basic idea is to see weakest precondition as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples {p}C{r}) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations.

Nous montrons comment la sémantique par continuations peut servir de point de départ pour construire un système de preuves pour ce langage. L'idée clé est de voir la plus faible précondition comme une sémantique par continuations particulière, puis d'interpréter les assertions à la Hoare ({p}C{r}) comme des inégalités portant sur les continuations. Cette approche permet également d'établir une correspondance entre étiquettes dans un programme et annotations.

Mots clés: Hoare Semantics

Mots clés: Continuations; Exceptions; Labels; Semantique a la Hoare

Domaines: Informatique [cs]

Philippe Audebaud, Elena Zucca. Deriving Proof Rules Form Continuations Semantics. [Research Report] LIP RR-1997-19, Laboratoire de l'informatique du parallélisme. 1997, 2+19p. ⟨hal-02101852⟩