1

我从来没有真正用契约语言设计过编程，我当然不希望这篇文章成为动态与静态类型系统的战争。

读了一会儿后，我的问题是标题中的问题：类型系统可以“捕获”的所有内容，也可以通过合同进行设计吗？在某些网站上，我读过诸如“合同是类固醇的类型”之类的内容，以及类似的声明。但它真的是一个真正的超集吗？

或者换句话说，带有合约的动态语言是否可以比没有合约的静态类型语言具有相同且更多的验证（再次，在运行时）？

谢谢！

4

2 回答 2

2

不可以。只能动态检查本地属性，而需要某种全局知识的属性则不能。考虑一些属性，例如某些东西是唯一的、没有别名的东西、没有竞争条件或死锁的计算。一个合适的静态类型系统可以验证这些属性，因为它能够在被检查的表达式的上下文中建立某些不变量。

于 2012-06-01T13:58:26.193 回答
1

我不是合同方面的专家，但我认为这基本上是正确的。一般来说，合约允许你编写动态检查来强制执行任意复杂的行为。合约最酷的地方在于，您可以使用它们：

  • 指定类型系统无法捕获的行为。（对于类型系统的通常定义。）
  • 在运行时将它们包含在您的程序中，以获得有关问题的详细报告。
  • 分配、跟踪和传播责任，看看哪里出了问题，哪里出了问题。

是的，合同可以像类型系统一样简单，从某种意义上说，“类型作为集合”的共同观点（这在多态 cse 中并不正确，但在您关心的许多情况下近似于某些行为）可以看作是契约语言的结构约束。但是，合同系统允许您编写更多修饰的行为。虽然您可以编写合约来表达排序函数的输入和排序后的输出之间的关系，但这需要依赖类型如果在类型中正确写下。所以简单的答案是，是的，合约可以用来定义类型系统所能做的一切，甚至更多。（我不完全确定像奇怪的子结构类型系统这样的边缘情况，但我认为这也可以通过污染事物的合同来完成。）

硬币的另一面是类型系统为您提供静态保证，即您的程序在某种程度上是正确的。然而，有了合同，你真的根本不能这么说。（当然，您可以将某些退化的合同案例视为通过使用标准类型系统、模型检查、SMT 求解器等进行了部分验证，并且在这方面确实已经完成了一些工作。）但是，合约真正强大的东西基本上是程序验证很难的想法，让我们抛弃一些静态保证，忍受一些可能的错误，并获得有关问题的更好信息，以便我们可以快速修复它。

顺便说一句，现在有更高级的合约系统，除了简单的结构约束之外，还有更高阶的时间合约（这里）和其他扩展，使使用合约进行编程非常酷。

编辑：我想我也应该更清楚地说明这一点，您的程序肯定有一些本地属性，您无法通过合同在全球范围内跟踪，所以安德烈斯的回应在这方面对我来说似乎更正确，对此感到抱歉！

于 2012-06-01T07:37:25.980 回答