> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK
我刚拿到了Crazyfliequadrotor(图1)从Bitcraze．这架飞机是一个开源项目，包括开源硬件。它被设计成一个开发平台，不像大多数其他四旋翼往往是封闭的系统。该软件可以下载，控制应用程序可以在PC上运行。它支持索尼双震控制器。
我查看了crazyfly的清单，并从PS3上拿出了我的索尼控制器。这个系统运行得很好，但我真正得到crazyfly的原因是为了检查Anthony Gracio的SPARK项目(见“如何使用SPARK防止无人机坠毁”）．安东尼是一个实习生AdaCore他用Ada的一个子集SPARK重写了控制软件。
控制软件和库是用c++编写的。这并不奇怪，因为C和c++往往是用于像这样最深入嵌入的项目的语言。它们也是从芯片供应商那里获得的典型工具集的一部分圣微电子用于crazyfly的Cortex-M3芯片。
Anthony使用了Adacore的标准工具链，该工具链可以作为开源项目使用。SPARK是为高完整性软件设计的，它提供了一个比大多数采用静态和动态验证的平台要好得多的平台。Adacore还有一个SPARK Pro版本。
Ada和SPARK的一个新特性是契约的概念(参见“Ada 2012:契约的喜悦”-电子设计)．它是Ada 2012的一部分，并使用预处理器将最初由SPARK开始的实现形式化。它允许“基于合同的编程”。这是使用指定输入和输出的契约对过程或方法进行注释的地方。这是在Ada固有的范围检查之外的。
将c++代码替换为SPARK代码是一个相对简单的练习。从本质上讲，这与添加c++代码的新版本是一样的。区别在于质量。Anthony发现并纠正了一些由于使用SPARK而导致的错误。SPARK代码在功能上与bug修复是相同的。
我真的很希望看到crazyfly项目切换到SPARK，但我怀疑c++爱好者没有领会这个暗示。在此期间，我希望有机会做一些SPARK编码。
> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK
