Верификация частными случаями

Буду говорить в контексте программирования, но соображения можно распространить шире.

Когда мы описываем алгоритм: программу, доказательство теоремы или решение математической задачи — мы строим его описание в рамках некоторой формальной модели. В рамках соглашений и ограничений, которые мы явно или неявно принимаем.

Описать алгоритм вне формальной модели невозможно. Хотя бы потому, что любой язык — уже формализация.

Отсюда вытекает интересная проблема.

Проблема

Модель — это урезанное описание реальности, которое упрощает анализ одной части мира, за счёт игнорирования другой. Поэтому каждая модель имеет ограничения применимости. Если забыть о них, то в лучшем случае все действия в с моделью окажутся бессмысленными; в худшем — что-нибудь сломается, взорвётся, убьётся, etc.

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

Для примера. Описывая алгоритм, мы должны учитывать особенности следующих моделей, список не полный:

• Языка, на котором поставлена задача.
• Математики, в рамках которой строится алгоритм.
• Языка программирования, его синтаксиса, семантики, прагматики.
• Компилятора / интерпретатора / транслятора, которые обрабатывают исходный код.
• Библиотек, которые использует алгоритм.
• Железа, на котором будет запускаться программа.
• Программного окружения, в котором будет работать программа.
• Социального окружения: людей, компаний, общества —  которые будут пользоваться программой.

Если мы нарушим соглашения одной из моделей, то во время эксплуатации программы может случиться неприятность. Например, уборщица на АЭС взорвёт реактор, пытаясь отчитаться о помытом поле.

Необходимо учитывать особенности всех моделей и сочетания этих особенностей. Но:

1. Все ошибаются.
2. Невозможно проверить работу программы во всех возможных условиях со всеми  возможными входными данными.

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

С этим приходится как-то жить.

Контроль через частные случаи

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

Если подходить к вопросу более формально, то под условием мы будем понимать входной параметр чистой функции.

Мы можем сформировать такой набор частных случаев, проверив на котором программу можно будет утверждать о её надёжности с достаточным для нас уровнем уверенности. Критерий довольно субъективный, но лучше пока не придумали.

Проверять можно по-разному. В контексте программирования, в первую очередь, это автоматизированное тестирование.

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

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

Поэтому, при попытке полного анализа ситуаций, случается комбинаторный взрыв, который замедляет анализ или делает его невозможным.

Формирование полного и небольшого набора проверок — сложная задача.

Лучше всего подходы к её решению должны быть проработаны у QA, но я довольно редко наблюдал признаки системности в их работе. Может быть у них есть внутренняя кухня, которая не выходит за границы отделов, во всех компаниях :-)

Интересные подходы точно есть у классической науки, которая во многом и стоит на поиске несоответствия теорий частным случаям. Для чего разработаны специальные процедуры проведения экспериментов. До знакомства с которыми я никак не могу добраться.

В любом случае, чтобы сформировать набор частных случаев, необходимо знать особенности моделей, для которых они формируются.

Частные случаи при проверке алгоритмов

Для большего погружения советую почитать мои посты:

• Тесты, которые тестируют тесты
• Дублирование логики — единственный способ верификации ПО

И статью википедии про морфологический анализ.

При планировании верификации программы важно помнить две вещи:

1. Совсем без тестов нельзя тяжело;
2. Проверить все частные случаи не получится.

Формируя набор случаев для проверки необходимо искать компромисс между полнотой (итоговой надёжностью) и объёмом работы.

Почтовый сервер требует одного уровня надёжности, текстовый редактор — другого, хобби-проект — третьего.

Поэтому при формировании набора тестов возникает два вопроса:

1. Как ограничить набор случаев?
2. Какие случаи включать в набор?

Ограничение набора частных случаев

Количество частных случаев уменьшится, если сократить количество моделей, которые мы считаем существенными.

Сделать это можно двумя способами.

Можно выкинуть модель из рассмотрения, так как последствия нарушения её соглашений для нас несущественны. Например, не для каждого софта существенно нарушение соглашений работы процессора — упадёт так упадёт — не страшно. Равно как и не всегда существенно нарушение соглашений программного и социального окружения.

Можно объединить несколько моделей в метамодель, сформировав её ограничения на базе ограничений дочерних моделей. Например, программная библиотека может скрывать особенности работы железа и программного окружения, предлагая меньший набор ограничений.

Формирование набора случаев

Когда мы определили набор проверяемых моделей, можно формировать перечень частных случаев.

Для каждого параметра алгоритма мы можем определить, какие особенности каких моделей он затрагивает.

В рамках конкретной модели разные значения параметров могут приводить к разным правилам работы с ними.

В простейшем случае, параметры могут быть валидными — при которых модель функционирует нормально и невалидными — при которых поведение модели не определено. Например, если мы определяем функцию сложения чисел, то её поведение может быть не определено для строк.

В более сложных случаях поведение может варьироваться сильнее. Например, в математике:

• 0 является валидным числом, но результат деления на него определён не всегда, а при сложении он имеет особое свойство x+0=x.
• 1 имеет особое свойство при умножении: x*1=x.

Оба случая — пример нейтрального элемента.

Для определения частных случаев мы разбиваем множество возможных значений параметра на подмножества значений с одинаковыми свойствами (в рамках моделей). Тогда нам надо проверить поведение алгоритма:

• на типичном значении параметра из каждого подмножества;
• на значениях параметра у границ подмножеств.

Граничные значения мы проверяем так как распространены ошибки определения границ множеств параметров.

Например, если наш алгоритм принимает параметром целое число, мы, опираясь на математику и знания о реализации железа, можем выделить следующие группы значений:

• +бесконечность
• -бесконечность
• 0
• ±1
• ±2
• очень большое положительное число
• очень маленькое отрицательное число
• просто положительное число
• просто отрицательное число
• не целое число: дробное, строка

Если алгоритм может принимать и целое и дробное число, то все эти варианты рассматриваются для каждого типа. Плюс для дробных рассматриваем числа из интервалов между этими группами и числа на границах множеств целых чисел, например 1 ± delta.

Как только мы берём в расчёт модель железа, у нас появляются дополнительные группы значений, например:

• ±0
• NaN

Если у алгоритма два и более входных параметров, то уже необходимо проверять все сочетания возможных значений. Комбинаторный взрыв всё ещё есть.

Можно меньше

Для уменьшения количества проверок есть несколько эвристик.

Упрощать логику. Часто можно выделить чёткое множество допустимых значений (например: целые числа от 50 до 100) и проверять только два случая:

1. одинаковая корректная работа на множестве допустимых значений;
2. одинаковая ошибка для всех остальных значениях.

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

Группировать проверки. Если мы хотим проверить алгоритм с двумя числовыми аргументами на работу с нулём и очень большими числами, то вместо четырёх проверок для аргументов (0, 0), (0, max), (max, 0), (max, max) — можно сделать две: (0, 0), (max, max) — скорее всего они закроют собой большинство случаев.

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

Всё ещё творческая задача

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

Во многом, качество софта зависит от разработчика:

• Широты его кругозора — сколько моделей и их особенностей он знает;
• Умения найти компромисс — как он умеет сократить количество проверяемых случаев, без ущерба для гарантий качества.

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