DENOTATIONAL SEMANTICS OF OBJECT SPECIFICATION

From an arbitrary temporal logic institution we show how to set up the corresponding institution of objects. The main properties of the resu lting institution are studied and used in establishing a categorial, d enotational semantics of several basic constructs of object specificat ion, namely aggregation (parallel composition), interconnection, abstr action (interfacing) and monotonic specialization. A duality is establ ished between the category of theories and the category of objects, as a corollary of the Galois correspondence between these concrete categ ories. The special case of linear temporal logic is analysed in detail in order to show that categorial products do reflect interleaving and reducts may lead to internal non-determinism.