DocumentCode
277812
Title
Program development with SPARK
Author
Carré, Bernard
Author_Institution
Program Validation Ltd., Southampton, UK
fYear
1991
fDate
33246
Firstpage
42461
Lastpage
42464
Abstract
SPARK is an annotated subset of Ada for high-integrity programming. This subset, in conjunction with its system of annotations (formal comments), is designed to eliminate language ambiguities and insecurities, and to allow rigorous static code analysis and formal verification of programs. The development, flow analysis and correctness proof of SPARK programs is supported by a software tool, the SPARK Examiner. The paper outlines the essential features of SPARK and explains how the Examiner is used in program development
Keywords
Ada; program verification; software reliability; software tools; Ada; SPARK; SPARK Examiner; correctness proof; flow analysis; formal verification; high-integrity programming; insecurities; language ambiguities; program development; software tool; static code analysis;
fLanguage
English
Publisher
iet
Conference_Titel
High Integrity Ada, IEE Colloquium on
Conference_Location
London
Type
conf
Filename
180767
Link To Document