CARE stands for Computer Assisted Refinement Engineering.
CARE provides a framework within which specification, programming and verification knowledge can be recorded and reused with minimal need for re-proof. The CARE system includes a library of design templates for which most of the difficult parts of modelling and proof have been done once, off-line, by suitably skilled experts.
CARE tools then help the user build applications by selecting and instantiating pre-proven refinements to fit the problem at hand, and generating and discharging correctness-of-fit proof obligations. Other CARE tools synthesize compilable source code programs which can be integrated with other system components and tested using common integration testing techniques.
The CARE method is generic and can be tailored for use with different specification languages, programming languages and theorem provers. In particular, it can be used to construct verified software for programming languages which themselves do not have a full formal semantics, by restricting use of target-language code to formally specified library routines which have been verified off-line using techniques appropriate to the target language.
The prototype toolset has been populated with a large number of design templates and primitive components for numbers, sets, lists, arrays and records. We have used the CARE method on a number of medium-sized applications including verification of the design of an event logger such as might be used in an embedded device. Work is proceeding on populating the tools with further general purpose design templates and primitive components, developing larger case studies, and improving the functionality of the library browsing tool. The tools themselves have been formally specified.