> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK
编写安全、可靠和安全的软件需要奉献精神、经验和好的工具。使用像C和c++这样的编程语言来开发这些类型的应用程序，以便开发人员可以改进他们的代码质量，通常意味着依赖于额外的软件，如静态分析工具。
Ada和它的子集SPARK合并了静态分析工具处理的大部分特性。然而，这些编程语言做得更好，因为它们允许程序员在他们的代码中更具体。因此，编译器可以根据这些明确的规范进行更多的检查。Ada 2012的合同支持更进一步，仍然允许程序员为函数和子例程提供前置和后置条件，以及指定类型不变量的能力。
这种极端的方法利用了SPARK的正式可验证的证明。通过使用契约定义，SPARK可以证明应用程序符合规范。在大多数情况下，契约中指定的检查将从生成的代码中删除，因为所有的检查都已由编译器完成。
那么我们该如何评价艾达和SPARK呢?
1.AdaCore的learn.adacore.com提供交互式的Ada和SPARK培训材料。
如果你喜欢一些繁重的阅读，那就退房吧约翰Barne的Ada 2012的编程．这本相当厚重的书很有深度，是一个有用的参考，但对Ada程序员新手来说不是一个好主意。相反,我建议AdaCore的新learn.adacore.com网站(图1)．课程包括两门课程:Ada导论和SPARK导论。还有一本在线电子书叫Ada用于c++或Java开发人员．电子书可以下载为PDF文件。
另外两门课程目前还不能以PDF文件的形式提供，因为它们附带了交互式代码块(图2)可以编译和运行。它们使用的是运行在AdaCore web服务器上的实际Ada和SPARK工具。大多数代码块的运行目的是显示编译器将报告的错误或运行代码将产生的结果。
可以编辑代码并重新运行/检查它，而不必安装开发环境。这项工作并不困难，但是在加载和编辑代码的同时必须返回到描述，这就更加繁琐了。另一方面，基于web的方法用代码本身来点缀关于代码的文章。
2.Ada和SPARK课程。
Ada和SPARK课程内容广泛，但并不详尽。同样，它们解决了基本的问题，比如包;子包和嵌套包留给以后的课程使用。Ada课程确实涵盖了一些重要的主题，如面向对象编程、多任务处理和泛型。SPARK课程涉及流程分析、程序完整性证明和功能正确性证明。
有很多神话对艾达和火花。希望通过了解Ada和SPARK可以帮助消除其中一些问题，并最终突出Ada和SPARK的优势。这些课程不会让你成为Ada或SPARK专家，但它们应该会让你更适应这些语言和它们能够完成的事情。
AdaCore也有很多免费的PDF电子书，包括最新的，AdaCore网络安全技术罗德里克·查普曼和亚尼克·莫伊著。其中大约一半介绍了AdaCore的产品，包括Ada和SPARK编译器，以及这些产品如何帮助解决网络安全问题。
对嵌入式开发人员有用的是“安全漏洞及其缓解”部分。本文提出了缓解的建议共同弱点枚举(CWE)由斜方维护。
CWE处理几乎任何应用程序中都可能出现的通用问题。这一节开头的两个文件处理数据验证问题。CWE 20处理不正确的输入验证，而CWE 1019处理如何验证输入错误。当然，缓解方法是在Ada和SPARK的背景下介绍的。有些，如Weak或No Crypto，无论使用何种编程语言，其缓解措施都是一样的。
> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK
