SPARK programming language
|
|
SPARK is a formally defined annotated sub-set of the Ada programming language, based on Ada 83 and Ada 95, which includes compile-time design-by-contract proving. 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 (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/)