Loading...
Please wait, while we are loading the content...
The Care Toolset for Developing Veriied Programs from Formal Speciications the Care Toolset for Developing Veriied Programs from Formal Speciications
| Content Provider | Semantic Scholar |
|---|---|
| Author | Hemer, David |
| Copyright Year | 1995 |
| Abstract | This paper describes the Care toolset for interactive development of veriied programs from formal speciications. The software engineer begins by giving a characterization of the application domain in the form of a mathematical theory. Care tools are then used to progressively design a program by sketching out the program structure and gradually lling in the details. At any stage the correctness of the partial design can be checked by using one of the Care tools to generate proof obligations. Another tool gives access to pre-proven parameterised design templates which encapsulate useful programming knowledge. When the design is complete, a third Care tool is used to automatically synthesize a source code program which { if all the proof obligations can be discharged { is guaranteed to meet its formal speciication. The knowledge base of Care can be extended by users in a soundness-preserving manner to include reusable domain theories, library routines, design templates and proof tactics. The Care toolset includes a fully automatic resolution-based theorem prover which will discharge many of the simpler proof obligations, and a general-purpose interactive theorem prover for the rest. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
