SPARK programming language

SPARK is a programming language, a formally defined annotated sub-set of Ada based on Ada83 and Ada95. It 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

 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 (http://www.sparkada.com/)
Praxis High Integrity Systems (http://www.praxis-his.com/)
UK's Safety-Critical Systems Club (http://www.safety-club.org.uk/)

es:SPARK

This article is a stub. You can help Wikipedia by expanding it (http://www.mywiseowl.com/index.php?title=SPARK_programming_language&action=edit).

Retrieved from "http://www.mywiseowl.com/articles/SPARK_programming_language"

This page has been accessed 76 times. This page was last modified 21:39, 24 Nov 2004. All text is available under the terms of the GNU Free Documentation License (see Copyrights for details).