Category:SPARK: Difference between revisions
Content added Content deleted
(Amended SPARK language description.) |
m (Corrected link.) |
||
| Line 25: | Line 25: | ||
The annotations state the required properties of a program. Different properties may require different types of annotation. |
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 [[Encyclopedia: |
A description of the SPARK Proof process is [[Encyclopedia: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 proprietary - the main copyright is held by [http://www.sparkada.com/ Altran-Praxis]. |
||