Skip to Main content Skip to Navigation
New interface
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073912
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:03:24 PM
Last modification on : Friday, February 4, 2022 - 3:18:52 AM
Long-term archiving on: : Thursday, March 24, 2011 - 1:20:48 PM

Identifiers

  • HAL Id : inria-00073912, version 1

Collections

Citation

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

Share

Metrics

Record views

47

Files downloads

145