The CARE language

A CARE program consists of types, fragments and theorems. CARE types correspond to data structures; fragments correspond roughly to functions and procedures in a procedural programming language; and theorems correspond to definitions, lemmas and CARE proof obligations.

Each CARE program component has its own formal specification, which may include constraints on how the component can be used. Program components are classified as primitive or higher-level. In essence, primitive components are those whose proof of correctness is outside the scope of CARE, while higher-level components have associated proof obligations. More specifically:

• Primitive components are supplied as part of the CARE library, and are not written by the ordinary user. Primitive types and fragments are implemented directly in the target programming language and provide access to target language data structures and basic functionality. The specification of such a component describes the component in terms of a mathematical model of the semantics of the target language and its compiler: a primitive type's specification describes the set of mathematical values corresponding to the associated data structure; a primitive fragment's specification describes the associated target code's functionality. Primitive theorems are axioms; their statement is their `specification'.
• Higher-level components are constructed from other components. Higher-level types and fragments express data refinements and algorithm designs respectively, and are implemented in a special-purpose language with a formally-defined mathematical semantics; using this semantics, CARE tools generate proof obligations which show that the component's implementation is correct with respect to its specification. Higher-level theorems (lemmas) are `implemented' by proofs.

CARE programs are developed incrementally: top-down, bottom-up or in a mixture of styles. During development a CARE program may contain components which have specifications but which do not yet have implementations. A complete program is one in which all components are implemented.

For full details.

Other CARE papers

Return to CARE home page