1

原谅设计得很糟糕的伪代码，但我希望它能明白这一点：

float sqrt takes float n : [0,inf)
    // fancy algorithm
    return result

void main
    x = sqrt -1             // Compilation error
    y = sqrt float.max      // This works
    z = (y + 1) * (y + 1)   // Compilation error (this would result in overflow)

在编译期间，编译器分析sqrt函数并将其表征为

sqrt : [0,float.max] -> [0, sqrt float.max[

它通过对+, -, *, /操作员做同样的事情来做到这一点。

在main函数中，第一条语句不编译，因为sqrt不接受负输入。第三条语句无法编译，因为*运算符只接受会导致输出的输入[float.min, float.max]。

4

2 回答 2

6

您正在寻找像 COQ、Agda 和 Idris 这样的语言，其中类型系统允许通过值对类型进行参数化。（依赖类型）

这并不像您想象的那么容易，并且通常需要（在调用方）满足条件的完整证明。在您的情况下，您必须证明 sqrt 的论点不能为负。这在以下情况下很简单

sqrt(5)

但在以下情况下并不容易：

sqrt(some_long_computation_on_floats(f))

您需要在这里证明some_long_computation_on_floats只会返回正数。这可能会也可能不会。

于 2013-11-05T08:14:22.290 回答
3

您可能想阅读按合同设计的内容。特别是，有许多语言和语言扩展支持在代码中设置复杂的合约，其中一些可能会在编译时检查。一个简单的例子是JML——事实上，这篇关于 JML 的论文的第一页有以下sqrt契约：

//@ requires x >= 0.0;
//@ ensures JMLDouble.approximatelyEqualTo(x, \result * \result, eps);
public static double sqrt(double x) {
    /*...*/
}

确实有一些工具可以在不运行代码的情况下检查合同违规情况，例如ESC/Java。

现在，契约式设计实际上非常流行，因为静态类型语言中的类型声明实际上是一种契约形式。然而，更复杂的合约远不那么受欢迎，我想说，因为：

  1. 编写复杂的合约会很快变得非常冗长。
  2. 错误可能会蔓延到复杂的合同中，这让您回到第 1 点——谁来检查合同？
  3. 在编译时检查复杂的合约通常是：
    1. 计算成本高
    2. 产生大量误报（或更糟的是，有误报）
  4. 还有其他公认的检查代码的技术，最常见的是使用自动化测试。
于 2013-11-05T07:11:47.547 回答