SPARK是一种安全的、经正式定义的编程语言。它被设计用来支持一些安全或商业集成为关键因素的应用软件的设计。SPARK有基于Ada 83和Ada 95的版本。最新版本RavenSPARK包含了Ravenscar Tasking Profile来支持高度集成应用中的同步。SPARK的正式和明确的定义使得多种静态分析技术在SPARK源代码的应用中成为可能。
外部链接
- SPARK官方主页（页面存档备份，存于互联网档案馆）
- Praxis高度集成系统（页面存档备份，存于互联网档案馆）
- Correctness by Construction: A Manifesto for High-Integrity Software
- 英国安全系统俱乐部主页（页面存档备份，存于互联网档案馆）
- SPARK 95 - The SPADE Ada 95 Kernel（包含RavenSPARK）
