Specification and verification of spatial data types with B-Toolkit

Spatial data types provide a fundamental abstraction for modelling the geometric structures of objects in space, their relationships, properties and operations. In this work, we present a formal specification and verification of spatial data types with the B-Toolkit. We give a formal specification of a realm and operations by using abstract machine notations of B. We then refine and implement a realm update operator in B, and verify formally an implementation of a realm update operator with B-Toolkit.