Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Towards an Override in Topoi

    2nd Irish Workshop on Formal Methods

    Cork, Ireland. 2nd - 3rd July 1998


    A. Hughes


    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?


    PDF filePDF Version of this Paper (240kb)