FOUNDATIONS OF THE B METHOD

 Dominique Cansell, Dominique Méry


2003 

 

Computing and Informatics, Vol. 22, 2003, 1–31 

 Abstract.
B is a method for specifying, designing and coding software systems. It is
based on Zermelo-Fraenkel set theory with the axiom of choice, the concept of
generalized substitution and on structuring mechanisms (machine,refinement,
implementation). The concept of refinement is the key notion for developing B
models of (software) systems in an incremental way. B models are accompanied
by mathematical proofs that justify them. Proofs of B models convince the
user (designer or specifier) that the (software) system is effectively correct. We
provide a survey of the underlying logic of the B method and the semantic
concepts related to the B method; we detail the B development process partially
supported by the mechanical engine of the prover.
Keywords: Events, Actions, Systems, Refinement, Proof, Validation, Formal
Method.

https://www.imm.dtu.dk/~dibj/cai/cai-b.pdf 

Comments

Popular posts from this blog

Ce que je dois à Jean-Raymond Abrial

Jean-Raymond Abrial (1938, 2025)

On B, Jean-Raymond Abrial