SPARK is a formally defined annotated sub-set of the Ada programming language (it is based on Ada 83 and Ada 95). This language is developed by Praxis High Integrity Systems (Praxis HIS), a UK software developer. Praxis HIS claims it was designed for development of software for applications where "correct operation is vital either for reasons of safety or business integrity."

"Hello, World!" in SPARK

The Hello world program in SPARK is:

with Spark_IO;
--# inherit Spark_IO;
--# main_program;

procedure Hello_World
--# global in out Spark_IO.Outputs;
--# derives Spark_IO.Outputs from Spark_IO.Outputs;
is
begin
   Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hello World!", 0);
end Hello_World;

References

• John Barnes: High Integrity Ada: The SPARK Approach, Addison-Wesley, ISBN 0201175177
• John Barnes: High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley, ISBN 0-321-13616-0

External links

• Official SPARK website
• Praxis High Integrity Systems
• UK's Safety-Critical Systems Club