Integration of the proof process in the system development through refinement steps

Dominique Cansell 1 Dominique Méry 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we present the incremental methodology to develop a multiplier and an adder. We start from an abstraction which gives the result in one shot and we introduce the algorithm using division by 2 and an accumulator to store a temporary result. For the adder we give another refinement to introduce the carry. Next we introduce two codings: an abstract one (sequence of bits) and a concrete one (bounded sequence of bits). We discover an overflow in the last refinement.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00100945
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:53:04 PM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM

Identifiers

  • HAL Id : inria-00100945, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Integration of the proof process in the system development through refinement steps. 5th Forum on Specification and Design Language - Workshop SFP in FDL'02, 2002, Marseille, France, 12 p. ⟨inria-00100945⟩

Share

Metrics

Record views

151