A Hidden Agenda: an algebraic combination of the object and logic paradigms

Grant Malcolm

(Oxford University)

This talk describes a programme of research directed to unifying the functional, logic, and object paradigms in an algebraic setting. Our chief resource in this endeavour is "hidden algebra", a framework that allows the specification of abstract machines with hidden local state.

The initial goal of our research was both straightforward and ambitious: to give a semantics for software engineering, and in particular for the object paradigm, supporting correctness proofs that are as simple and mechanical as possible. This emphasises proofs rather than models, and thus suggests an equational approach, because equational logic is fully expressive, yet simple and has a great deal of mechanical support.

Hidden algebra takes as basic the notion of behavioural abstraction, or more precisely, behavioural satisfaction: our specifications characterise how objects (and systems) behave, not how they are implemented; they provide a notion of behavioural type, which we prefer to call a hidden theory.

Building on the algebraic specification tradition, hidden algebra uses some sorts for data values (of attributes) as in the algebraic approach to data types, and some for states, as in the algebraic approach to abstract machines; the latter give us objects and classes. These two uses of sort are dual: induction establishes properties of data types, while coinduction establishes properties of objects. Similarly, initiality is important for data types, whereas finality is important for objects. Our correctness proofs show that one such theory behaviourally satisfies another.

An important contribution of this programme of research is the development of powerful hidden coinduction techniques for proving behavioural correctness of object systems.
Tuesday 11th February 1997, 14:30
Seminar Room 322
Department of Computer Science