| A framework that can be used to specify, derive and verify the semantics of an object-oriented program is presented. The framework, FOOS (Framework for Object-Oriented Semantics) is built upon a Three-domain Architecture: a theory domain, a program domain, and an object domain. Under this architecture, specifications are logic theories, programs are the implementations of these theories, and objects are logic models of these theories. In addition to modeling the relationships among specification, implementation, and run-time behavior of an object-oriented program, means are also provided for reasoning the dynamic features of objects, including object references, reference aliasing, dynamic bindings, etc.; FOOS extends the theories of many-sorted logic and predicate transformation to accommodate the object-oriented paradigm. The result is the TOT (Theory of Object Types). Objects are simply regarded as models of the TOTs in FOOS. Based on the compositional nature of objects, a multi-layered proof obligation into layers of smaller proof tasks. To demonstrate, the framework also includes a miniature object-oriented language TOOL (a Tiny Object-Oriented Language), whose semantics is obtained following the approaches of FOOS. |
