Introduction to SPARK Reference High integrity Ada John Barnes SPARK Is formally a subset of Ada in that any correct SPARK program is also a correct Ada program But this is misleading because the annotations are really a major language feature SPARK Basic Structure Take Ada Remove features to get a small subset Define a set of annotations Annotations are from Ada s point of view comments lexically they start with But they are syntactic elements of SPARK So SPARK is a separate language What to Leave Out of Ada Things that make certification and formal reasoning e g verification harder Tasks Exceptions Generics Access types Gotos Why no tasks Because tasking programs are inherently more complex than simple sequential programs The state of a tasking program is a much more complex object Task interactions are complex Non determinacy is a concern Why no Exceptions Because exceptions make the control flow of a program much more complex Certifiable programs cannot have unexpected exceptions anyway Exception handlers lead to deactivated code which is problematic for certification Why no Generics Generics are a short hand for repeated instantiations so do not provide any fundamental expressive power But proving properties is more complex because we have to quantify over types If we have to prove separate instantiations we may as well write them Why no Access Types Access types only make sense in connection with dynamic storage allocate But dynamic allocation is a real problem since it is hard to prove that storage is never exhausted Why no Gotos Not really needed in most programming At best only a minor convenience But they complicate formal analysis Because the effect of a sequence of code can no longer be represented as the composition of the effects of its sequential components What Else to Leave Out Ada favors the reader heavily over the writer in its design SPARK carries this principle to further extremes Why because the reader may be a formal tool Furthermore writing code takes a fraction of the time it takes to certify Other Things Left Out Dynamically sized arrays Eases reasoning about range correctness Overloading Implicit operations e g sliding Implicit subtypes X Integer range 1 10 not allowed Must declare separate subtype The Annotation Language All statements start with but they are not comments they are strict elements of the SPARK syntax Global Definitions Declare use of global variables Dependency Relations Specify information flow what outputs depend on what inputs Oher types of annotations Access of Variables in Packages The idea is to restrict visibility Inherit clauses Control visibility of package names Own variable clauses Control access to package variables Initialization Indicate initialization of own variables Purpose of Annotations Make code clearer at spec level Introduce redundancy compiler can check Allow error checks to be made Support verification The SPARK tools SPARK Examiner processes SPARK programs Checks syntactic validity Including checking annotations for consistency and correctness Generates useful warnings Generates auxiliary information helpful in analysis and certification Annotations in Action Procedure Sly V in vector global in out A derives A from A V is begin A 1 V 1 V 1 A 1 V 1 V 1 end Sly A 1 1 0 Sly A error param overlaps global variable An example Exchange Procedure Exchange X Y in out Float global T derives X from Y Y from X is begin T X X Y Y T end This is illegal because it modifies T and the annotations do not make this clear Exchange attempt 2 Procedure Exchange X Y in out Float global T derives X from Y Y from X is T Float begin T X X Y Y X end This generates 4 fatal errors Errors in attempt 2 T X is an ineffective statement Importation of initial value of X ineffective Variable T is not referenced or exported Imported value of X not used in deriving the value of Y Imported value of Y may be used in the derivation of Y Path Functions Compute all possible paths through program and provide explicit information about possible paths List conditions for each path Check consistency of conditions Check Path Consistency if X Y then if X Y then end if end if Path 2 traversal conditions 1 X y 2 X Y Path 2 path eliminated contradictory conditions Verification Conditions procedure Exchange X Y in out Float derives X from Y Y from X post X Y Y X is T Float begin T X X Y Y T end Verification Conditions H1 C1 C2 true y y x x Meaning is H1 C1 and C2 Obvious in this case The Simplifier Attempts to simplify the verification conditions generated by the examiner For example previous set of conditions simplifies to true Another Example Type T is range 128 128 procedure Inc X in out T derives X from X is begin X X 1 end Verification Conditions After simplification we get the conditions H1 H2 C1 x 128 x 128 x 127 This last conclusion cannot be proved An Improved Inc procedure procedure Inc X in out T derives X from X pre X T Last is begin X X 1 end Now proof obligation shifts to call site The Proof Checker The simplifier does a lot but it is after all a simplifier it does not prove complex theorems Proof of complex theorems may be needed The proof checker is in charge of making sure these proofs are correct Is SPARK really usable In real life there are complex external gizmos like external sensors with weird data Devices with inherently nondetermistic behavior Computations that require low level messing around One more feature hide Allows arbitrary use of full Ada or anything else for that matter Hidden from examiner For example we can give a procedure spec with full annotatations And then completely hide the body And use other means to verify the body How is SPARK Used SPARK program is written Examined with examiner Otherwise examined by various techniques and tests Might include formal proof for example at least freedom from exceptions Then result is compiled with Ada compiler The object code is verified