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.
https://hal.inria.fr/inria-00100945
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:53:04 PM Last modification on : Friday, September 4, 2020 - 11:20:23 AM
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⟩