Category:SPARK: Difference between revisions

From Rosetta Code
Content added Content deleted
m (Made Ada references into links)
(add changed syntax coming with SPARK 2014)
 
(11 intermediate revisions by 6 users not shown)
Line 1: Line 1:
{{language|SPARK
{{language|SPARK
|site=http://www.altran-praxis.com/spark.aspx
|tags=spark
|exec=machine
|exec=machine
|gc=allowed
|gc=allowed
Line 9: Line 11:
|safety=safe
|safety=safe
|LCT=yes}}
|LCT=yes}}
{{language programming paradigm|concurrent}}
⚫
[http://en.wikipedia.org/wiki/SPARK_programming_language '''SPARK'''] or '''SPARK Ada''' is a sub-language of [[Ada]], supplemented with annotations (formal comments). Its primary purpose is for high-integrity applications, where static analysis of the source is used to determine properties of the program.
{{language programming paradigm|imperative}}
{{language programming paradigm|object-oriented}}
⚫
[[wp:SPARK_programming_language|'''SPARK''']] or '''SPARK Ada''' is a sub-language of [[Ada]], supplemented with annotations (formal comments). Its primary purpose is for high-integrity applications, where static analysis of the source is used to determine properties of the program.


The properties that SPARK code can be analysed for are:
The properties that SPARK code can be analysed for are:
Line 19: Line 24:
*Absence of dead paths.
*Absence of dead paths.


The annotations always begin, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the [[Ada]] standard.
In older versions, the annotations always began, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the [[Ada]] standard. Newer versions, starting with SPARK 2014, use the aspect syntax known from Ada 2012.


A SPARK program can be compiled by any [[Ada]] compiler or processed by any other [[Ada]] tool.
A SPARK program can be compiled by any [[Ada]] compiler or processed by any other [[Ada]] tool.
Line 27: Line 32:
A description of the SPARK Proof process is [[SPARK_Proof_Process|here]].
A description of the SPARK Proof process is [[SPARK_Proof_Process|here]].


The SPARK tools are freely available under the GNU GPL. The SPARK language definition is proprietary - the main copyright is held by [http://www.sparkada.com/ Altran-Praxis].
The SPARK tools are freely available under the GNU GPL. The SPARK language definition is available from AdaCore at [http://docs.adacore.com/spark2014-docs/html/lrm/ SPARK 2014 Reference Manual].

The [news:comp.lang.ada comp.lang.ada] [[newsgroup]] ([http://groups.google.com/group/comp.lang.ada/topics access via Google Groups])is the main forum for discussing or asking questions about SPARK.

Latest revision as of 12:22, 22 November 2016

Language
SPARK
This programming language may be used to instruct a computer to perform a task.
Official website
Execution method: Compiled (machine code)
Garbage collected: Allowed
Parameter passing methods: By reference, By value
Type safety: Safe
Type strength: Strong
Type compatibility: Nominative
Type expression: Explicit
Type checking: Static
Lang tag(s): spark
See Also:
Listed below are all of the tasks on Rosetta Code which have been solved using SPARK.

SPARK or SPARK Ada is a sub-language of Ada, supplemented with annotations (formal comments). Its primary purpose is for high-integrity applications, where static analysis of the source is used to determine properties of the program.

The properties that SPARK code can be analysed for are:

  • Freedom from data-flow errors.
  • Freedom from information flow errors.
  • Freedom from information flows that violate safety or security.
  • Type safety (freedom from run-time errors).
  • Functional correctness.
  • Absence of dead paths.

In older versions, the annotations always began, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the Ada standard. Newer versions, starting with SPARK 2014, use the aspect syntax known from Ada 2012.

A SPARK program can be compiled by any Ada compiler or processed by any other Ada tool.

The annotations state the required properties of a program. Different properties may require different types of annotation.

A description of the SPARK Proof process is here.

The SPARK tools are freely available under the GNU GPL. The SPARK language definition is available from AdaCore at SPARK 2014 Reference Manual.

The comp.lang.ada newsgroup (access via Google Groups)is the main forum for discussing or asking questions about SPARK.

Subcategories

This category has the following 3 subcategories, out of 3 total.

@

Pages in category "SPARK"

The following 8 pages are in this category, out of 8 total.

A

B

D

F

L

S

Retrieved from "https://rosettacode.org/wiki/Category:SPARK?oldid=154884"