On Typechecking B

Abstract. The typechecking system of the formal method B is discussed. An inconsistency in the public definition of the B method, attributable to a flaw in the typechecking system, is uncovered: the typechecking method expects the types of variables to be given in one membership predicate, such as a, b, c ∈ A × B × C, instead of with several membership predicates joined by conjunction, like a ∈ A∧b ∈ B ∧c ∈ C, even though such constructions are liberally used in the literature. A set of modifications to the typechecking system fixing this flaw is presented and analyzed.

• Type: Conference
• Year: 2003
• Where: SPLST
• Authors: Antti-Juhani Kaijanaho
• Keywords: Formal Method, Programming Languages, SPLST 2003, Typechecking Method, Typechecking System