This programming language may be used to instruct a computer to perform a task.
|Execution method:||Compiled (machine code)|
|Parameter passing methods:||By reference, By value|
If you know SPARK, please write code for some of the tasks not implemented in SPARK.
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.
The annotations always begin, on each line, with the Ada comment symbol “--”, so all SPARK programs comply with the Ada standard.
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 proprietary - the main copyright is held by Altran-Praxis.
This category has the following 3 subcategories, out of 3 total.