Tool Support
The "Examiner" (part of the "SPARK Toolset") performs two kinds of static analysis. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage can be incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (e.g., use of uninitialised data) on a system-wide basis (including abstract state in package bodies).
The second, optional, analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds the Constraint_Error exception to the list of possible errors eliminated by SPARK. This proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties. It can also be used to show conformance with some suitable specification.
Read more about this topic: SPARK (programming Language)
Famous quotes containing the words tool and/or support:
“The veto is a President’s Constitutional right, given to him by the drafters of the Constitution because they wanted it as a check against irresponsible Congressional action. The veto forces Congress to take another look at legislation that has been passed. I think this is a responsible tool for a president of the United States, and I have sought to use it responsibly.”
—Gerald R. Ford (b. 1913)
“Surely, ‘tis one step towards acting well, to think worthily of our nature; and as in common life, the way to make a man honest, is, to suppose him so ... so here, to set some value upon ourselves, enables us to support the character ... of generosity and virtue.”
—Laurence Sterne (1713–1768)