Towards an institution for Object-Z specifications

摘要

Despite its three decades of existence, institution theory continues still to inspire new trends and approaches in the field of formal specification and programming. One such an approach is the so-called 'Grothendieck institution' approach to multi-logic heterogeneous specification paradigm, emphasising the idea that for some kinds of applications it is more suitable to use a 'composite institution' (capable to capture multiple views) rather than a single one. In this work, we define an institution for a 'subset' of Object-Z notation and prove that it has amalgamation. This property is useful for the behaviour of Object-Z specifications in-the-large and for their integration in the framework of a heterogeneous institution supporting a multi-modelling language based on UML and Object-Z.