Category: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: |
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.
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 proprietary - the main copyright is held by Altran-Praxis.
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.
- Execution method/Compiled/Machine code
- Garbage collection/Allowed
- Parameter passing/By reference
- Parameter passing/By value
- Typing/Safe
- Typing/Strong
- Typing/Compatibility/Nominative
- Typing/Expression/Explicit
- Typing/Checking/Static
- Programming Languages
- Programming paradigm/Concurrent
- Programming paradigm/Imperative
- Programming paradigm/Object-oriented
