Deriving Proof Rules Form Continuations Semantics - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1997

Deriving Proof Rules Form Continuations Semantics

(1) , (1)
1

Résumé

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.
Fichier principal
Vignette du fichier
RR1997-19.pdf (297.28 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101852 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101852 , version 1

Citer

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⟩
5 Consultations
8 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More