Ada是一种“安全关键”的编程语言吗？

Question

Ada是一种“安全关键”的编程语言吗？

ada

29

我尝试在谷歌上搜索并阅读了一些片段。为什么Ada是一种“安全关键”语言？我注意到的一些事情包括：

没有指针
指定范围（此类型是整数，但只能为1-12）
明确声明函数参数是否为out或in/out
基于范围的循环（避免边界错误或边界检查）

我对其余的语法要么不理解，要么不知道它如何帮助它成为“安全关键”的语言。这些都是一些点，但我没有看到大局。它是否具有我没有看到的设计契约？它是否有使代码更难编译的规则（如果有，是什么规则）？为什么它是一种“安全关键”的语言？

- user34537

1

我认为必须进行比较才能回答这个问题。例如，将其与 C（更少限制）进行比较，然后再与 Haskell（在某些情况下更加限制，但在其他情况下不会变得复杂；-）进行比较。 - user166390

8

Ada 确实有指针；它称之为“访问类型”。 - Keith Thompson

7

为了更加安全可靠的系统，可以使用SPARK。它是Ada语言的一个子集，并带有附加检查的注释：http://en.wikipedia.org/wiki/SPARK - Rommudoh

1

请参阅类型安全性：http://en.wikipedia.org/wiki/Type_safety - NWS

3

在Ada中，访问类型是真正的指针，而不是C语言中的地址/整数混合体。 - WGroleau

5个回答

14

所有这些都适用于安全关键应用程序；但是还要考虑能够指定布局（直到位）以及[可选地]指定此类记录仅可以在特定位置（对于诸如视频内存映射之类的事物非常有用）的能力。

请考虑，许多安全关键应用程序也没有标准界面（在“广泛”和前向兼容性的意义上均如此）；例如：核反应堆、火箭发动机（工程本身从一代到下一代的差异不同*）、飞机模型。

即将推出的Ada 2012标准确实具有实际的合同，形式为前置条件和后置条件；示例（摘自http://www2.adacore.com/wp-content/uploads/2006/03/Ada2012_Rational_Introducion.pdf）：

generic
   type Item is private;
package Stacks is

type Stack is private;

function Is_Empty(S: Stack) return Boolean;
function Is_Full(S: Stack) return Boolean;

procedure Push(S: in out Stack; X: in Item)
with
    Pre => not Is_Full(S),
    Post => not Is_Empty(S);

procedure Pop(S: in out Stack; X: out Item)
with
    Pre => not Is_Empty(S),
    Post => not Is_Full(S);

Stack_Error: exception;

private
 -- Private portion.
end Stacks;

另外，被忽略的一件事情是能够从您的访问/指针类型中排除Null的能力; 这很有用，因为您可以a）在子程序参数中指定该排除条件，b）简化算法[因为您不必在每个使用实例中检查null]，并且c）让异常处理程序处理（我假设是）异常情况下的Null。

* Arianne 5事故之所以发生，正是因为管理层忽视了这一事实，并要求程序员使用错误的规范：Arianne 4的规范。

- Shark8

2

关于Arianne 5 - 该程序在Arianne 4上正常工作，当轨迹超出Arianne 4的限制时，它正确地触发了自毁程序。 - NWS

1

没错，如果 Arinne 5 和 4 在工程上是兼容的，就不会有问题了，就像如果你把 747 上的所有客舱部分拆除来用作家具货机一样，航空器上的软件也不会有任何问题。 - Shark8

1

“_它正确地触发了自毁程序_” 实际上是气动力破坏了发射器。 - curiousguy

4

同时考虑到，Ada使得许多人错误地声称“真正的程序员”太聪明而不会犯的许多错误几乎变得不可能。 - WGroleau

10

AdaCore在这里对Ada 2005的各种安全功能进行了精彩的介绍:

http://www.adacore.com/knowledge/technical-papers/safe-secure/

美国政府和行业也曾经进行过有关程序可靠性的研究，比较了各种编程语言。由于这些网站都很老，我没能快速找到其中一篇，但下面是DDCI网站上的引用:“在八十年代进行的研究中，Ada始终优于像Pascal、Fortran和C等已有的编程语言。在九十年代，Ada在衡量能力、效率、维护、风险和生命周期成本等方面仍然胜过C++。”

在以下链接中列出了Commanche项目选择Ada的原因。我想补充的是，平台实现已经存在很长时间并保持稳定。正如文章中的一位消息来源所说，维护是成本的主要来源。我们已经看到现代竞争者.NET和Java不断变化。 Ada的长期稳定性对于常常需要投入使用几十年的安全关键应用程序来说更为重要。

http://www.ddci.com/displayNews.php?fn=programs_rah66.php

另一个好处是Ada被设计用于跨语言开发。我不断看到新闻中的人们谈论.NET和JVM如何创新，因为它们让您将“正确的工具用于正确的工作”混合到一个系统中。 Ada已经有这种能力很长一段时间了。应用程序常常是Ada、C、C++、汇编等的混合体（例如MULTOS CA）。而且它们仍然运行良好。

Ada也没有停滞不前。他们不断更新语言，最近在2012年进行了更新。它的可移植性使其能够运行在JVM和.NET上，以便那些想要库或者已经有大量现有代码的人使用。还有来自IBM、Aonix、AdaCore和Green Hills的Ada开发工具和强大的运行时环境，适用于许多操作系统和实时操作系统。

最后一个好处：如果它能编译通过，那么它将能够正常运行。通常来说。

- Nick P

1

我曾经为你寻找那个参考资料，但是却发现了这个宝藏：NASA关于安全关键软件开发的指南。第207页着重介绍如何选择适合工作的编程语言。它列出了需要注意的事项，评估了主要的编程语言，并选出了最佳选择。（由于政府停摆导致真实链接无法使用，所以使用了archive.org） - Nick P

http://web.archive.org/web/20130510145632/http://www.hq.nasa.gov/office/codeq/doctree/871913.pdf - Nick P

6

那篇文章中提到的一个点表述得过于简略：错误的早期检测。即使错误一直持续到运行时，你仍然有机会得到一个异常，并且异常消息将指向非常接近错误的位置，而不是静默地改变数据，导致在故障之后很久才出现其他表现... 在我看来，这一点单独来说就是一个巨大的优势。 - user1818839

4

我知道这有点晚了，但这是我最近遇到的一个例子。我写了下面这个 C++ 函数，在 -O0 下工作得很好：

size_t get_index(const Monomial & t, const Monomial & u) {
    get_index(t, u.log()); // forgot to type "return" first...
}

这段代码虽然能编译通过，如果你的编译器比较好，可能会发出警告，但是当它和其他程序一起被编译时，你很可能看不到这个警告。当我使用-O0编译它时，它居然奇迹般地运行良好。但是当我使用-O3编译它时，它每次都崩溃了，而我却找不出原因，因为我没有看到警告（如果有的话）。试想当你认为在那里应该有一个return语句时，你还需要进行调试。

同样的，在我学习C语言的时候，我经常犯这个错误：

int a;
scanf("%d", a); /* left out & before the a */

在C语言中，使用int作为指针或反之的做法被认为是常规编程实践，以至于25年前的编译器甚至不会发出警告。这是C语言的一个特性，而不是缺陷。(例如，参见Brian Kernaghan的"Why Pascal is not my favorite Language")。当然，在那个时候，家用计算机操作系统没有内存保护；如果你很幸运，当计算机重启时，它没有写入硬盘。

这些错误在Ada中甚至无法编译。函数必须返回值，而你不能意外地使用Integer代替access Integer(即指向整数的指针)。

这只是个开始！

- John Perry

在Ada中，未初始化的变量不会被初始化为零。 - Molly Stewart-Gallus

2

我遇到了一个程序，在离线测试版本（Windows）中运行良好，但在真实版本（PowerPC上的VxWorks）中失败，原因是Windows编译器将未初始化的数据清零，而PPC则没有。 - Simon Wright

2

Ada对实时性的支持非常优秀。这使得程序员能够实现更高程度的确定性，而不必担心编程语言本身的技术细节。虽然C语言也可以通过深入理解来实现Ada支持的许多运行时特性，但由于Ada是标准化的，因此它实现了大多数实时特性。Ada甚至有一个Ravenscar配置文件，以及SPARK语言，其中基于Ada 83和95的子集，"高度可靠的操作是必要的" http://en.wikipedia.org/wiki/Ravenscar_profile http://en.wikipedia.org/wiki/SPARK_%28programming_language%29。我猜测，SPARK没有针对更新的Ada版本推出版本，是因为目前还无法确定新版本的安全性。在后一篇文章中还提到，Ada可以进行优化，达到与C语言相媲美的速度，这对于依赖于快速变化事件期间精确控制的实时应用程序非常重要。Ada内置了许多标准功能，用于实时控制，这显然对于“安全关键”语言非常重要。

- user922475

4

实际上，Spark-2014 基于 Ada-2012 的契约机制，使得编写可被形式化证明的代码更加容易。http://www.spark-2014.org/ - user1818839

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- T.E.D. · Accepted Answer

这很简单。Ada语法中有很多似乎与使语言“安全关键”（无论对于一种语言来说这意味着什么）没有什么关系的原因是，这不是Ada的设计目标。它被设计为一种通用的编译系统编程语言，足够强大，以至于美国国防部可以摆脱所有需要支持各地小型一次性语言的问题。

最终结果是一个相当适用于安全关键应用程序的语言，这只是因为 该语言设计得非常出色，考虑到军事应用程序（在这里软件可靠性通常涉及到生命危险）。

惊人的是，很少有其他现代语言将建立可靠的软件作为设计目标。 大多数语言似乎是由一个孤独的“天才”黑客创造的，其主要目标是能够快速产生大量的代码，也许是以某种黑客喜欢的新方式。