3

学習目的でグラフフレームワークを作成しています。私はTDDアプローチを使用しているので、多くの単体テストを作成しています。しかし、私はまだユニットテストの正しさを証明する方法を考えています

たとえば、私はこのクラスを持っています（実装は含まれていません、そして私はそれを単純化しました）

public class SimpleGraph(){
 //Returns true on success
 public boolean addEdge(Vertex v1, Vertex v2) { ... }

 //Returns true on sucess
 public boolean addVertex(Vertex v1) { ... }
}

私もこの単体テストを作成しました

@Test
public void SimpleGraph_addVertex_noSelfLoopsAllowed(){
 SimpleGraph g = new SimpleGraph();
 Vertex v1 = new Vertex('Vertex 1');
 actual = g.addVertex(v1);
 boolean expected = false;
 boolean actual = g.addEdge(v1,v1);
 Assert.assertEquals(expected,actual);
}

さて、それは素晴らしいです。ここで重要なのは1つだけです。この場合にのみ、関数が機能することを証明しました。しかし、私のグラフ理論のコースでは、定理を数学的に証明するだけです（誘導、矛盾など）。

だから私は自分のユニットテストが正しいかどうか数学的に証明できる方法があるのだろうかと思っていました。それで、これには良い習慣があります。そのため、特定の結果についてユニットをテストするのではなく、ユニットの正確性をテストしています。

4

6 に答える 6

5

いいえ。ユニットテストは、一般的なケースで正しいことを証明しようとはしません。特定の例をテストする必要があります。アイデアは、エラーが発生した場合に1つ以上のテストで見つかる可能性が高い代表的な例を十分に選択することですが、この方法ですべてのエラーを確実にキャッチすることはできません。たとえば、add関数を単体テストしている場合、正の数、負の数、大きい数、小さい数をテストできますが、このアプローチだけを使用すると、この実装が機能しない場合を見つけることができます。

int add(int a, int b) {
    if (a == 1234567 && b == 2461357) { return 42; }
    return a + b;
}

ただし、単体テストとコードカバレッジを組み合わせることで、このエラーを見つけることができます。ただし、コードカバレッジが100％であっても、どのテストでも検出されなかった論理エラーが発生する可能性があります。

コードが正しいことを証明することは可能です。これはフォーマル検証と呼ばれますが、単体テストの目的ではありません。また、最も単純なソフトウェア以外のすべてのソフトウェアを実行するのは費用がかかるため、実際に実行されることはめったにありません。

于 2011-03-04T07:17:07.357 に答える
2

おそらく そうではありません。単体テストは、徹底的なテストによって問題にアプローチします。

  • 動作を実装する前にテストを作成して、テストが機能することを確認します。
  • 次に、テストが失敗したことがわかります。
  • 次に、そのテストに合格するための動作を実装し、そのテストのみを実装します。テストの実装に必要のないコードは絶対に記述しないでください。
于 2011-03-04T07:17:11.147 に答える
1

実際、あなたが証明しているのは、アルゴリズムの1つのケースが機能していることです。たとえば、実行パスのサブセットが有効であることを証明しています。テストは、厳密な数学的意味での正当性を証明するのに役立つことはありません（非常に単純な場合を除く）。一般的な場合、これは不可能です。テストは、この問題に対する実用的なアプローチであり、代表的なケース（境界値、中間の値など）が正しいことを示し、それが機能することを期待します。

それでも、findbugsなどのいくつかのツールは、コードのいくつかのプロパティの保守的な証拠を提供することができます。

自分のものの正式な証明が必要な場合は、常にCoq、Agda、および同様の言語がありますが、単体テストを作成するのは大変です:)

テストと証明の優れた簡単な紹介の1つは、一言で言えばPatrickCousotの抽象解釈です。

于 2011-03-04T07:22:31.590 に答える
0

コードがどのように動作するかを正式に指定するためのツールや、それらがそのように機能することを証明するためのツールもありますが、それらは単体テスト領域から遠く離れています。

Javaの世界からの2つの例は、JMLとESC/Java2です。

NASAには、形式手法を専門とする部門全体があります。

于 2011-03-04T07:23:32.053 に答える
0

私の2セント。このように見てください。あなたは何かをする関数を書いたと思いますが、実際にしたことは、何かをすると思う関数を書くことでした。コードが何をするかを数学的に証明することができない場合は、関数を仮説として扱うこともできます。それが常に正しいかどうかはわかりませんが、少なくともそれは偽りです。

そして、それが私たちがユニットテストを書く理由です（注：バグが発生しやすい他の関数、ため息）、それが成り立たない反例を見つける仮説を偽造しようとします。

于 2012-06-22T17:27:44.700 に答える
0

コードの正しさのプロパティを確認したい場合は、以前の投稿ですでに述べたように、いくつかのフォーマル検証ツールを適用できます。これは簡単なことではありませんが、それでも実行できる可能性があります。Javaコードの1次プロパティを証明できるKeYシステムのようなツールがあります。KeYには、ジェネリックス、フロート、並列処理などの問題がいくつかありますが、Java言語のほとんどの概念で非常にうまく機能します。さらに、プルーフツリーに基づいてKeYを使用してテストケースを自動的に作成できます。

JML（これは習得するのは難しくありませんが、基本的には少しロジックのあるJava）に精通している場合は、このアプローチを試すことができます。システムの非常に重要な部分の場合、検証は本当に考慮すべきことかもしれません。コードの他の部分については、たとえば回帰の問題を回避するために、単体テストで可能なトレースの一部をテストするだけで十分な場合があります。

于 2014-01-30T08:36:23.987 に答える