17. Glossary

The SPARK Reference Manual uses a number of technical terms to describe its features and rules. Some of these terms are well known others are less well known or have been defined within this document. In the glossary given here the less well known terms and those defined by SPARK are listed with a brief explanation to their meaning.

  • Data-flow analysis is the process of collecting information about the way the variables are used and defined in the program. In particular, in SPARK it is used to detect the use of uninitialized variables and state abstractions.

  • Executable semantics is the definition of what it means for a construct to be executed at run-time. In SPARK, most contracts have executable semantics, which means in particular that they can halt execution by raising an exception if some error condition occurs.

  • Flow analysis is a term used to cover both data-flow and information-flow analysis.

  • Formal Verification, in the context of hardware and software systems, is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. In SPARK this entails proving the implementation of a subprogram against its specification given its precondition using an automatic theorem prover (which may be part of the SPARK toolset). The specification may be given by a postcondition or assertions or may be implicit from the definition of the program when proving absence of run-time exceptions (robustness property).

  • Information-flow analysis in an information theoretical context is the transfer of information from a variable x to a variable y in a given process, that is y depends on x. Not all flows may be desirable. For example, perhaps the behavior of one part of a system is intended to be completely independent of the state of another part so that information flow from the latter part to the former would indicate a design error. Or a system shouldn’t leak any secret information to public observers. In SPARK information-flow analysis is used to detect useless statements and check that the implementation of a subprogram satisfies its Global aspect and Depends aspect (if they are present). It may also be used for security analysis in SPARK.