DocumentCode
2748211
Title
Penelope: an Ada software assurance editor
Author
Marceau, Carla ; Harper, C. Douglas
Author_Institution
Odyssey Res. Associates Inc., Ithaca, NY, USA
fYear
1989
fDate
19-23 Jun 1989
Firstpage
119
Lastpage
127
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/CMPASS.1989.76050
Filename
76050
Link To Document