A formal language CCSL is introduced for describing specifications of classes in object-oriented languaes. We show how class specifications in CCSL cna be translated into higher order logic. This allows us to reason about these specifications. In particular, it allows us (1) to describe implementations of a particular class specification, (2) to develop the logical theroy of a specific class specification, and (3) to establish refinements between two class specifications. We use the higher order logic of the proof-assistant PVS, so that we have extensive tool support for reasoning about class specifications. Morover, we describe our own front-end tool to PVS, which generates fro mCCSl class specifications appropriate PVS theories and proofs of some elementary results.
展开▼
