Ada 为何是“安全关键”？语言？

Question

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

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

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

Answer 1

嗯，这很简单。之所以有很多 Ada 语法似乎与使语言变得“安全关键”（无论这对语言意味着什么）没有太多关系，是因为这不是 Ada 的设计目标。它被设计为一种通用编译系统的编程语言，足以让美国国防部摆脱它必须支持的所有小型一次性语言。

事实上，最终结果是一种对安全关键型应用程序相当有用的语言，这只是一个令人高兴的副作用，因为该语言针对军事应用程序设计得非常好（其中 >生命通常取决于软件的可靠性）。

令人惊讶的是，很少有其他现代语言支持构建可靠软件作为设计目标。大多数语言似乎都是由一个孤独的“天才”黑客炮制出来的，其主要目标是能够以黑客喜欢的某种新方式快速编写大量代码。

Answer 2

所有这些都适合安全关键型应用；但还要考虑分配布局（精确到位）的能力以及[可选]指定此类记录只能位于某个位置的能力（对于视频内存映射等有用）。

考虑到许多安全关键型应用程序也没有标准（在“广泛传播”和前向可比性的意义上）接口；例如：核反应堆、火箭发动机（工程本身每一代都不同*）、飞机模型。

即将推出的 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;

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

* Arianne 5 灾难的发生正是因为管理层忽视了这一事实，让程序员使用了错误的规格：Arianne 4 的规格。

Answer 3

AdaCore 在这里很好地介绍了 Ada 2005 的各种安全功能：

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

美国政府和业界很久以前也对程序可靠性进行了比较语言的研究。我无法很快找到一个，因为这些网站都很旧（！），但这里引用了 DDCI 网站上的一段话：“在 80 年代进行的研究中，Ada 的性能始终优于 Pascal、Fortran 和 C 等成熟的编程语言。在 90 年代，Ada 在衡量能力、效率、维护、风险和生命周期成本的性能评估方面继续超越 C++。”

在下面的链接中列出了他们在 Commanche 项目中使用它的原因。我要补充一点的是，该平台的实现已经存在很长时间并且保持稳定。正如文章中的一位消息人士所说，维护是大部分成本的来源。我们已经看到现代竞争者 .NET 和 Java 发生了疯狂的变化。 Ada 的长期稳定性对于通常长期（有时数十年）部署的安全关键型应用程序来说更好。

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

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

它也不是静态的。他们不断更新该语言，最近一次是在 2012 年。它的可移植性使其能够在 JVM 和 .NET 上运行，对于需要这些库或拥有大量现有代码的人来说。还有适用于 IBM、Aonix、AdaCore 和 Green Hills 的许多操作系统和 RTOS 的 Ada 开发工具和强大的运行时。

最后一个好处：如果它能编译，它就能工作。通常。

Answer 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 中编译它时，它每次都会崩溃，我一生都无法弄清楚为什么，因为我没有看到警告（如果它出现的话）。想象一下调试，当您认为您只是因为知道自己的意图而返回时。

同样，当我学习 CI 时，经常犯这样的错误：

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

使用 int 来表示指针，反之亦然，这被认为是 C 语言中的正常编程实践，以至于 25 年前的编译器甚至都懒得理会。发出警告。哎呀，这是 C 的功能，而不是错误。 （例如，参见 Brian Kernaghan 的“为什么 Pascal 不是我最喜欢的语言。”）当然，当时的家庭计算机操作系统没有内存保护；如果幸运的话，计算机重置时不会写入硬盘。

这些类型的错误甚至无法在 Ada 中编译。函数必须返回一个值，并且您不能意外地使用Integer代替访问Integer（即，指向整数的指针）。

这只是开始！

Answer 5

Ada 对实时 http 具有出色的支持://www.adaic.org/resources/add_content/standards/05rat/html/Rat-1-3-4.html。这使得程序员能够实现更大程度的确定性，而不必担心编程语言本身的技术细节。虽然 Ada 支持的许多运行时功能可以通过对事物的深入理解用 C 实现，但由于 Ada 是标准化的，所以它可以很好地实现大多数实时功能。 Ada 甚至还有 Ravenscar 个人资料 http://en.wikipedia.org/wiki/Ravenscar_profile 和 SPARK一种“高度可靠的操作至关重要”的计算机语言，基于 Ada 83 和 95 的子集 http://en.wikipedia.org/wiki/SPARK_%28programming_language%29。我的猜测是 SPARK 没有适用于更高版本 Ada 的版本 b/c 现在判断新版本的安全性还为时过早。后一篇文章中还提到，Ada 可以针对与 C 相媲美的速度进行优化，这对于在快速变化的事件期间依赖于精确控制的实时应用程序非常重要。有许多用于实时控制的内置标准功能，这对于“安全关键”语言显然很重要。