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.
Mots-clés : adder incremental development refinement b method multiplier méthode b multiplieur additionneur raffinement développement incrémental
Type de document :
Communication dans un congrès
Eugenio Villar. 5th Forum on Specification and Design Language - Workshop SFP in FDL'02, 2002, Marseille, France, 12 p, 2002
Liste complète des métadonnées
https://hal.inria.fr/inria-00100945
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:53:04
Dernière modification le : jeudi 11 janvier 2018 - 06:21:04

Identifiants

  • HAL Id : inria-00100945, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

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

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

91

Contact


archive-ouverte@inria.fr