Title :
Penelope: an Ada software assurance editor
Author :
Marceau, Carla ; Harper, C. Douglas
Author_Institution :
Odyssey Res. Associates Inc., Ithaca, NY, USA
Abstract :
The development of a prototype verification editor named Penelope, which allows users to develop specifications, Ada programs, and proofs of verification conditions, is presented. Penelope differs from previous verification systems in that it is interactive, allowing the user to develop specification, program, and proof concurrently. Verification conditions can be inspected and used to guide program development and the correction of errors. The user proves verification conditions within Penelope, appealing to previously formulated axioms and lemmas
Keywords :
Ada; text editing; Ada software assurance editor; Penelope; error correction; interactive; program development; proofs; prototype verification editor; verification conditions; verification systems; Computer bugs; Constraint theory; Contracts; Costs; Error correction; Programming profession; Quality assurance; Safety; Software prototyping; System testing;
Conference_Titel :
Computer Assurance, 1989. COMPASS '89, 'Systems Integrity, Software Safety and Process Security', Proceedings of the Fourth Annual Conference on
Conference_Location :
Gaithersburg, MD
DOI :
10.1109/CMPASS.1989.76050
