The Proof Technology in Formal Method B
Lei Lu · Modern Electronic Technique · 2005
Developing software using formal method is key to advance software reliability,improve developing efficiency and realize software automation.Formal method B can be used in the whole developing cycle from specifications to implementation by the aid of its tools.This paper presents the processes of hierarchical development and proof of method B,depicts its type checking and proof obligations from the construction of abstract machine to refinement and implementation in detail.Finally,the efficiency of the proof technology in method B is proved via practical applications.