The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #594

Title:A Calculus of Refinements: Its Class of Models
Authors:Agusti,J; Esteva,F; Garcia,P; Levy,J
Date: 1992
Presented:Submitted to the First National Conference onDeclarative Programming, ProDe'92
Abstract:Data and its classification into types are kept separated and used distinctively in most programming languages. Types are mainly used as a discipline that contributes to program correctness and computation is not done on types. Nevertheless types have also been considered as specifications. The subtyping can be seen as a kind of specification refinement defining a type hierarchy where programs are the leaves on which computation is done. The Calculus of Refinements (COR) presented here takes this idea of types as specifications and subtyping as refinement and pushes it to an extreme. Types and values are no longer distinguished; in COR we consider a unique hierarchy of objects without distinctions between leaves and the rest of nodes. The subtyping relation is the only relation between objects and is called refinement: an object is a refinement of another if the latter is a more specified version of the former. A good way to deal with the hierarchy of objects is to structure it as a complete lattice. And if functions are to be considered as first class citizens in the hierarchy then the lattice must be reflexive: it must have the space of functions (some of them) as a sublattice. So complete reflexive lattices are the intended semantic domains we want to use to model stepwise refinement from specifications (upper objects in the hierarchy) to programs (objects well defined for the actual purposes of the programmer). We have shown how these lattices can be used as a semantic basis for knowledge representation languages..

[Search These Pages] [DAI Home Page] [Comment]