Compositional Structuring in the B-Method: A Logical Viewpoint of the Static Context

The B-Method provides a collection of structuring mechanisms which support information hiding, modularisation and compositionality of module operations, although, in order to achieve compositionality and independent (parallel) refinement, sharing is restricted in B. In this paper we elaborate some non-interference and compositionality assumptions that underlie structuring mechanisms such as uses, sees and imports and show how they may be …