Skip to Main content Skip to Navigation
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 metadatas

https://hal.inria.fr/inria-00073912
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:03:24 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 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

131

Files downloads

199