Technical Overview
SPARK aims to exploit the strengths of Ada while trying to eliminate all its potential ambiguities and insecurities. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada compiler. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking) and partly by introducing annotations or "formal comments" which encode the application designer's intentions and requirements for certain components of a program.
The combination of these approaches is meant to allow SPARK to meet its design objectives, which are:
- logical soundness
- rigorous formal definition
- simple semantics
- security
- expressive power
- verifiability
- bounded resource (space and time) requirements.
- minimal runtime system requirements
SPARK being an 'annotated subset' of Ada, programs written in SPARK can be compiled by any Ada compiler ('subset' of Ada implies that not all Ada features may be used).
'Annotated' means that certain annotations in form of Ada comments (i.e., ignored by the Ada compiler) are evaluated by an additional tool called the 'Examiner' which is meant to ensure strict enforcement of the requirements expressed via the aforementioned annotations to analyze the corresponding SPARK/Ada program for its correctness before passing it to an Ada compiler to compile the source code.
Read more about this topic: SPARK (programming Language)
Famous quotes containing the word technical:
“A technical objection is the first refuge of a scoundrel.”
—Heywood Broun (1888–1939)