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ため、最初のステートメントはコンパイルされません。sqrt3 番目のステートメントはコンパイルされません。これは、*演算子が の出力になる入力のみを受け取るためです[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 に答える