On Typechecking B

13 years 5 months ago

Download www.cs.uku.fi

Abstract. The typechecking system of the formal method B is discussed. An inconsistency in the public deﬁnition of the B method, attributable to a ﬂaw 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 modiﬁcations to the typechecking system ﬁxing this ﬂaw is presented and analyzed.

Antti-Juhani Kaijanaho

Real-time Traffic