7

哪些编程语言是高完整性系统的不错选择？

一个错误选择的例子是 Java，因为有大量的代码是程序员无法访问的。我正在寻找强类型、块结构语言的示例，其中程序员负责 100% 的代码，并且尽可能少地受到 JVM 之类的干扰。

编译器显然是个问题。语言必须有一个完整而明确的定义。

编辑：高完整性系统是安全关键系统等、安全系统等的总称。

编辑编辑：我想要不受平台影响的语言示例，无论编译器如何并且完全定义，它们都会产生相同的结果。

4

7 回答 7

4

您正在寻找多高的诚信度？

  • 俄勒冈州波特兰市的Galois在用Haskell编写的高完整性系统上建立了非常成功的业务。我相信他们强调数据的完整性和安全性。用如此复杂的语言、非常复杂的运行时系统来做这种工作有点令人惊讶，但是 Haskell 的类型系统提供了非常强大的保证，并且语言语义提供了比大多数语言强得多的推理原理。此外，您倾向于为每个应用程序编写更少的代码，因此很容易显示正确。

  • 如果您需要更强大的保证，SPARK Ada（或者现在只是 SPARK）是一种相对简单的传统命令式语言，具有完整的形式语义和用于完整形式验证的工具。与使用 Haskell 相比，您可以获得更强大的保证，但在资本和劳动力方面的价格要高得多。

于 2010-05-03T13:28:15.340 回答
4

我认为 ADA 通常用于此目的。

于 2010-05-03T12:01:13.333 回答
4

Ada 的 SPARK 子集将是一个很好的起点。SPARK 继承了 Ada 的所有优秀特性（强类型、易读等），并具有没有未定义特性的额外好处，这意味着所有 SPARK 程序都将执行完全相同的操作，无论使用哪种 Ada 编译器编译它。

SPARK 可以在没有运行时的情况下使用。对于 Ada 语言也是如此（参见 pragma No_Runtime）。

当然，使用诸如 SPARK 之类的语言，您是在用灵活性换取安全性（或安全性）。

于 2010-05-03T12:09:57.263 回答
3

您可能想从Eiffel的角度来思考，在这种情况下，对前置条件和后置条件的更强执行使高完整性系统更容易。

于 2010-05-03T12:10:16.293 回答
1

这在术语上是矛盾的。强类型、块结构的语言几乎总是由编译器编译，产生程序员不负责的机器代码。如果你想对代码100%负责，你需要使用汇编语言。

于 2010-05-03T12:01:45.080 回答
1

我不完全理解它是什么“高完整性系统”。假设您的意思是“一个为 bug 留下更少空间的系统”，我建议您看一下ML，它是 OOP 的衍生产品O'CaML。ML 旨在最大限度地减少类型错误。ML 中没有转换错误或空指针 - 您根本无法对其进行编码。它还缺乏动态功能——这使得它不那么酷但更安全。

话虽如此，ML 远非黑客的乐趣。这是一种有些繁琐的语言。但是，如果您希望多工作一个小时而少获得一个例外，那么这是一个相关的选择。

于 2010-05-03T12:10:46.793 回答
-2

你可能会寻找你想要的东西，但你不会得到它。

您的要求彼此不兼容。他们基本上完全排除了任何类型的图书馆。你可以说你可以使用 C / C++ - 但没有任何包含文件和标准库（程序员显然不会对此负责）。

这让你几乎处于旱地——这个要求是不切实际的。即使有一个庞大的团队，也不想对大多数库进行重新编程。

如果您有适当的编程方法，Java 实际上非常好 - 并且足够有趣，您的要求（高完整性系统）更多是编程方法的问题（单元测试，大量内部测试，多个实例并行比较结果 - 比如航天飞机控制计算机-以防万一发生故障）而不是语言决定的。

于 2010-05-03T12:01:52.427 回答