Докажите правильность юнит-теста

Question

Я создаю графическую среду для целей обучения.Я использую подход 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);
}

Ладно, круто, это работает.Здесь есть только одна суть, я доказал, что функции работают только для этого случая.Тем не менее, на курсах по теории графов все, что я делаю, - это математическое доказательство теорем (индукция, противоречие и т. Д.)?Так есть ли хорошая практика для этого.Таким образом, мы проверяем устройство на правильность, а не проверяем его на один определенный результат.

Answer 1

Нет.Модульные тесты не пытаются доказать правильность в общем случае.Они должны проверить конкретные примеры .Идея состоит в том, чтобы выбрать достаточно репрезентативных примеров, чтобы в случае возникновения ошибки она, вероятно, была обнаружена одним или несколькими тестами, но вы не можете быть уверены, что поймаете все ошибки таким образом.Например, если вы тестируете модульную функцию добавления, вы можете протестировать некоторые положительные числа, некоторые отрицательные, некоторые большие и некоторые маленькие, но, используя только этот подход, вам посчастливится найти случай, когда эта реализация не работает:

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

Однако вы сможете обнаружить эту ошибку, комбинируя модульное тестирование и покрытие кода .Однако даже при 100% покрытии кода могут быть логические ошибки, которые не были обнаружены никакими тестами.

Это возможно доказать код на корректность.Это называется формальная проверка , но это не то, для чего предназначены юнит-тесты.Это также дорого для всех, кроме самого простого программного обеспечения, поэтому на практике это делается редко.

Answer 2

Возможно не .Модульные тесты решают проблему путем исчерпывающего тестирования:

• Вы проверяете, что ваш тест работает, написав тест, прежде чем реализовывать поведение.
• Тогда вы видите, что тест не пройден.
• Затем вы реализуете поведение для прохождения этого теста, и только этого теста .Никогда не пишите код, который не нужен для реализации теста.

Answer 3

Действительно, вы доказываете, что один случай вашего алгоритма работает, например, вы доказываете, что подмножество ваших путей выполнения являются действительными. Тестирование никогда не поможет вам доказать правильность в строгом математическом смысле (за исключением очень простых случаев). В общем случае это невозможно . Тестирование - это прагматический подход к этой проблеме, когда мы пытаемся показать правильность репрезентативных случаев (граничные значения, значения где-то посередине и т. Д.) И надеемся, что это сработает.

Тем не менее, некоторые инструменты, такие как findbugs и т. Д., Могут дать вам консервативное доказательство некоторых свойств вашего кода.

Если вы хотите получить формальное доказательство своих вещей, всегда есть Coq , Agda и подобные языки, но это чертовски сложно от написания модульного теста:)

Одно замечательное и простое введение в тестирование на доказательствах - это Абстрактная интерпретация в двух словах Патрик Кузо.

Answer 4

Если вы хотите проверить правильность свойств вашего кода, вы можете, как уже упоминалось в предыдущих статьях, применить некоторые формальные средства проверки .Это не легко сделать, но все же возможно.Существуют такие инструменты, как система KeY , способная доказать свойства первого порядка для кода Java.У KeY есть некоторые проблемы с такими вещами, как дженерики, числа с плавающей точкой и параллелизм, но он работает довольно хорошо для большинства концепций языка Java.Более того, вы можете автоматически создавать контрольные примеры с помощью KeY на основе дерева проверок.

Если вы знакомы с JML (это не сложно освоить, в основном Java с небольшим количеством логики)Вы можете попробовать этот подход.Для действительно важных частей ваших систем , проверка действительно может быть чем-то, о чем стоит подумать;для других частей кода тестирование некоторых из возможных трассировок с помощью модульного тестирования уже может быть достаточным, например, чтобы избежать проблем регрессии.

Answer 5

Мои 2 цента. Посмотрите на это так: вы думаете, что написали функцию, которая делает что-то , но на самом деле вы написали функцию, которая , вы думаете, она что-то делает . Если вы не можете написать математически доказательство того, что делает код, вы также можете рассматривать эту функцию как гипотеза ; Вы не можете быть уверены, что это будет всегда правильно, но по крайней мере это фальсифицируется .

И именно поэтому мы пишем модульное тестирование (примечание: только другие функции, склонные к ошибкам, sigh ), чтобы попытаться сфальсифицировать гипотезу, находящую контрпримеры, с которыми она не справляется.

Answer 6

Существуют инструменты для формального определения того, как работает ваш код, и даже инструменты для доказательства их работы таким образом, но они находятся далеко от области модульного тестирования.

Два примера из мира Java: JML и ESC / Java2

НАСА имеет целый отдел , посвященный формальным методам .