Models of software systems are built in Z and VDM using partial functions between sets and certain operations on these partial functions : extension (⊔), restriction (◁), removal (⋪) and override (†). Can these operations be given a categorial semantics? Doing so will show the ‘nature’ of the operations. The operation of override is found to depend on the ‘shape’ on X , the poset PX . The operations are developed in an elementary topos ɛ. This is achieved by constructing each operation in the topos Set , of sets and total functions, and then using these constructions as the definition of the operations in an elementary topos. Each of the operations is thus given a categorical semantics. As an example the operation of override is considered in the topos Set ↓, of total functions and commuting diagrams. Can models of software systems be built in topoi other than Set ?
Content
Author and article information
Contributors
Arthur Hughes
Conference
Publication date:
July
1998
Publication date
(Print):
July
1998
Pages: 1-16
Affiliations
[0001]University of Dublin,
Trinity College, Dublin, Ireland