>>网站资源
.. >>图书馆：Techxchange
.. .. >> Techxchange：嵌入式软件
. . . . . .>>主题:Ada和SPARK
|
|
下载本文以.pdf格式 此文件类型在适用时包括高分辨率图形和原理图。 |
ADA是一种通用语言，如C ++或Java，支持现代编程语言的常用功能，例如数据封装，对象方向，模板（称为“泛型”），例外和任务。最初在1983年定义，它已经经历了几个修订，最新的2012年。除了其他通用语言之外的ADA是什么，它是从开始以可靠性，安全和安全的开始设计的。毫不奇怪，ADA用于软件正确性至关重要的域名：太空，航空电子，空中交通管制，铁路和军队。
Spark是ADA的专业子集，旨在促进使用正式方法，因此可以通过基于数学的保证保证软件或其他程序性质的正确性。因此，Spark在与ADA相同的域名中，由那些重视正式方法提供的强担保的人。
因为正式的方法可以比测试在对软件正确性的高度置信度的测试中更具成本效益，所以软件的新域名也是关键的，例如汽车和无人机软件，越来越多地吸引了像火花一样的解决方案。特别是，正式的方法提供比防御软件漏洞的安全攻击的测试更好的解决方案。
ada.
ADA最突出的特点之一是一种强大而强大的系统。ADA支持广泛的用户定义类型。它包括符号（具有溢出语义）和模块化整数类型（带包装语义）的各种尺寸。这两种类型都允许限制有效整数的范围。ADA还支持由任何整数或枚举类型索引的枚举类型和数组类型：
类型my_index为1 .. 100;- 仅包含1到100类型My_Color的Integers的符号整数类型为（红色，蓝色，黄色）;- 一个枚举类型，它与ADA类型my_array中的整数相同，是my_color的数组（my_index范围<>）;- my_array对象由my_index（即，1到100之间的整数）索引索引 - 并包含类型my_color 类型的元素Ada提供了一个增强可靠性的重要特性:它自动插入针对大量常见错误的运行时检查。具体来说，它动态地检查数组边界以外的访问(通常称为“缓冲区溢出”错误)和类型范围之外的整数值。如果发生冲突，则在运行时引发异常。如果需要(例如，在验证提供了错误不会发生的信心之后)，出于效率原因，可以禁用这些检查:
i：my_index：= <=“”a =“”复杂=“”computation =“”>;- 如果我的价值不在1到100°之间，将提出异常：my_array（1 .2）：=（红色，蓝色）;- a是索引范围为1到2的数组，其中a（1）=红色和a（2）=蓝色c：颜色：= a（i）;- C是A的I-TH元素。如果我大于2. ，将提出异常。Ada的当前（2012）版本通过对基于合同的编程的支持来进一步推广可靠性。最常见的合同形式是子程序前提和后期性。这些是布尔表达式，它可以分别作为呼叫者和分支机构之间的合同，在每个呼叫子程序之前和之后必须真实。合同有助于若干原因开发安全和安全软件。首先，通过为子程序的假设和保证提供源代码文档来提高程序的可读性和可维护性。其次，它们增强了测试，因为它们可以在运行时检查。
过程增加（x：out整数），pre => x <= max， - 每个调用者都有责任来检查其参数是否低于最大值。post => x>xâ€旧;- 增加的责任，以确保 - 返回的X的值严格大于其初始值。火花
Spark，基于ADA，也旨在考虑安全，安全性和可靠性，但它的不同之处在于支持正式验证。Spark已经与ADA一起发展，Spark 83基于ADA 83（其中包括增强ADA子集的验证相关注释的程式化的注释语法），到当前版本，Spark 2014。
这个最新版本是Ada 2012的一个子集(使用Ada内置的契约机制)，并允许多种形式的静态验证。特别是，软件开发人员可以指定信息应该如何通过程序中的变量流动，并定义有关程序行为的函数属性。所有这些契约，以及运行时没有错误和异常，都可以进行静态验证。
为实现这一目标，已从Spark中排除了不易验证的ADA的一些特征。最值得注意的是，禁止的功能包括指针（但允许地址）。这种限制是由使用指针的可验证程序所需的重型语法以及自动验证此类程序的困难。
SPARK不仅是Ada的子集，而且还包含了专门支持正式分析的特性。其中包括增强用户注释能力的新型契约，从而可以正式验证属性。例如，SPARK定义了描述子程序使用哪些变量的契约，以及变量和子程序之间的信息如何流动:
步骤swap_x_and_y与globals =>（in_out =>（x，y））， - swap_xand_y修改全局变量x和y。依赖于=>（x => y，y =>X）;- x的最终值仅取决于y的初始值 - 并且y的最终值仅取决于x的初始值。Spark还允许程序员将子程序的合同定义为一组不同的情况，子程序的分组值应该具有相同的行为，以类似于传统测试用例：
函数绝对值(X:整数)回归自然与Pre = > X / = Integera首先,——不应该呼吁Absolute_Value整数的最小值,这将导致一个溢出Contract_Cases = > (X < 0 = > Absolute_Valuea结果= - X, X = 0 = > Absolute_Valuea结果= 0,X > 0 = > Absolute_Valuea结果= X);——Absolute_Value在x的三个域上的行为不同——对于负值，它返回相反的值，对于0，它返回0——对于正值，它返回与输入相同的值。用火花用ADA
虽然技术上ADA和Spark是不同的语言，但它们在一起工作。在Spark使用标准ADA语法（Pragmas，Apposss和Attributes）中引入的新功能的其他功能。ada.and SPARK can be mixed at a fine-grained level—the programmer can combine Ada and SPARK code in different packages or subprograms, or inside a single package or subprogram (for example, between a subprogram’s specification and its body, or between a package declaration’s visible and private parts). This mixing helps alleviate the SPARK language restrictions. For instance, the programmer can use full Ada in places where the flexibility of pointers is more important than the ability to formally verify behavior:
包Abstract_Pointer with SPARK_Mode是——这里我们是在SPARK类型My_Pointer是私有的;——这个包的用户不能看到My_Pointer是什么。——他们必须使用子程序来访问其内容。My_Pointer (P: My_Pointer)的返回值函数Create_Pointer (V: Value)返回My_Pointer;SPARK_Mode (Off);——我们现在在Ada类型My_Pointer是访问所有值;——My_Pointer实际上是一个指针!Abstract_Pointer结束;Ada和Spark制作一个有效的双语团队，用于写作安全，安全和可靠的软件。Spark为ADA执行的动态验证添加了静态正式验证。应用程序的最关键部分可以用火花写入，允许用户从形式验证技术中受益，而可以保留适用于需要更直接实现的那些部件的完全表现力。
总之，ADA与Spark不是竞争，而是一种有效和合作关系：一种语言（ADA）通过传统的验证方法（测试和审查）提供了对可靠性，安全性和安全性的强烈功能，并提供了令人信心兼容语言（Spark）提供强大功能，以保证具有正式方法的可靠性，安全性和安全性。
>>网站资源
.. >>图书馆：Techxchange
.. .. >> Techxchange：嵌入式软件
. . . . . .>>主题:Ada和SPARK
