Sciweavers

SPLST
2003

On Typechecking B

14 years 14 days ago
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.
Antti-Juhani Kaijanaho
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 2003
Where SPLST
Authors Antti-Juhani Kaijanaho
Comments (0)