SPARK - 維基百科，自由的百科全書

SPARK是一種安全的、經正式定義的編程語言。它被設計用來支持一些安全或商業集成為關鍵因素的應用軟件的設計。SPARK有基於Ada 83和Ada 95的版本。最新版本RavenSPARK包含了Ravenscar Tasking Profile來支持高度集成應用中的同步。

zh.wikipedia.org