Tag: refinement

Jean-Raymond Abrial’s B method and later Event-B made refinement, proof obligations and set-theoretic modeling central to a disciplined path from abstract system models toward increasingly concrete designs.

Z made abstract state, invariants and operations into a mathematical specification language, while Abrial's later B work pushed formal methods toward refinement and verified construction.