Как вы докажете, что функция работает?

Question

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

Это все не очень приятно для меня.Когда я начинаю думать о необходимости создавать тесты для удовлетворения охвата веток и путей, а затем тестировать интеграцию, предполагаемые перестановки могут стать немного сводящими с ума.

Итак, мой вопрос, как можно доказать (вВ том же духе доказательства теоремы в математике), что функция работает (и в идеальном мире объединяет эти «доказательства» в доказательство того, что система работает)?

Существует ли определенная область тестирования, котораяохватывает подход, при котором вы пытаетесь доказать, что система работает, доказывая, что все ее функции работают?Кто-нибудь за пределами академии беспокоит такой подход?Существуют ли инструменты и методы, которые могут помочь?

Я понимаю, что мое использование слова «работа» не совсем точно.Я предполагаю, что имею в виду, что функция работает, когда она делает то, что в какой-то спецификации (написанной или подразумеваемой) говорится, что она должна делать, и ничего не делает, кроме этого.

Обратите внимание, я не математик, просто программист.

Answer 1

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

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

Answer 2

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

В TDD вы пытаетесь сформулировать крайние случаи, которые метод должен выполнить, чтобы быть действительным, однако, такой случай можно пропустить. Даже если (нетривиальный) метод выполняет все ваши тесты, может быть комбинация аргументов или последовательность событий, о которых вы даже не думали, что нарушит ваш код. Проще говоря: это жизнь. Возможно, вы можете предсказать все результаты в нетривиальной реализации, но вы можете убедиться, что метод работает для конкретных крайних случаев, за исключением некоторых случаев, которые являются настолько острыми, что вы порежетесь при прикосновении к ним. (Зинг, плохой каламбур).

Answer 3

«Звучит так, будто вы определяете работу как функцию, выполняющую то, что вы хотите, чтобы она делала» Обычно вам также нужно убедиться, что функция не выполняет то, чего вы не хотели, определения близкино не то же самое, например, функция ADD () может вернуть правильный ответ, но также распечатать дополнительный мусор отладки.

Answer 4

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

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

Похоже, что в Википедии есть статья на эту тему: Формальная проверка