Reasoning with Executable Specifications

Yves Bertot 1 Ranan Fraer
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Starting from the specification of a small imperative programming language, and the description of two program transformations on this language, we formally prove the correctness of these transformations. The formal specifications are given in a single format, and can be compiled into both executable tools and collections of definitions to reason about into a theorem prover. This work is a case study of an environment integrating executable tool generation and formal reasoning on these tools.
Type de document :
Rapport
RR-2780, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073912
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:03:24
Dernière modification le : lundi 3 septembre 2018 - 10:56:02
Document(s) archivé(s) le : jeudi 24 mars 2011 - 13:20:48

Fichiers

Identifiants

  • HAL Id : inria-00073912, version 1

Collections

Citation

Yves Bertot, Ranan Fraer. Reasoning with Executable Specifications. RR-2780, INRIA. 1996. 〈inria-00073912〉

Partager

Métriques

Consultations de la notice

101

Téléchargements de fichiers

113