О тестах, доказывающих отсутствие ошибок
«Тест может показать наличие ошибок, но ни один тест не может доказать их отсутствия»
На первый взгляд утверждение Дейкстры неопровержимо. Действительно, поди-ка докажи, что в программе X, написанной на языке Y, нет ошибок. Компания, разрабатывающая PVS-Studio, инструмент для обнаружения ошибок в исходных текстах на Си, C++, C# и Java, регулярно знакомит нас с коллекциями ошибок в известном ПО. Они придумывают всё новые и новые методы обнаружения. Но ошибки не собираются сдаваться. Производителям PVS-Studio можно задать вопрос: а готовы ли они дать юридически обязывающие гарантии отсутствия ошибок в ПО, чтобы ПО можно было застраховать, а в случае обнаружения ошибок подать суд? Ответ всем очевиден. Казалось бы, тут безнадёга и полная обречённость. Ошибки неистребимы. Однако всё-таки попробуем опровергнуть Дейкстру. Или показать очевидность того, что в ряде случаев это возможно. Как доказать отсутствие ошибок в чистых функцияхС чистыми функциями всё просто: они детерминированы, не производят побочных эффектов, а любому набору входных параметров всегда соответствует один и тот же результат. Возьмём такой пример:
// Функция, которая принимает восьмибитный символ,
// а возвращает «истину» или «ложь»
bool is_digit (unsigned char c) {
return '0' <= c && c <= '9';
}
Поскольку восьмибитный параметр имеет всего 256 вариаций своего значения, то проверить и получить доказательство отсутствия ошибок можно, сделав 256 проверок. Для этого надо просто перебрать все возможные значения:
c = 0; if (is_digit (c) != false) { printf("Error, c=%d", c); exit; }
. . .
c = 47; if (is_digit (c) != false) { printf("Error, c=%d", c); exit; }
c = 48; if (is_digit (c) != true) { printf("Error, c=%d", c); exit; }
. . .
c = 57; if (is_digit (c) != true) { printf("Error, c=%d", c); exit; }
c = 58; if (is_digit (c) != false) { printf("Error, c=%d", c); exit; }
. . .
c = 255; if (is_digit (c) != false) { printf("Error, c=%d", c); exit; }
Здесь и далее приведено решение «в лоб», которое хорошо иллюстрирует, но на практике не оптимально.
Чтобы считать доказанным отсутствие ошибок в функции
Рассмотренная выше функция Мы немножко поколебали пьедестал, на котором стоит Дейкстра. Но мы помним, что существует доказательство о ненужности программ, состоящих только из чистых функций. А как обстоят дела с нечистыми? Как доказать отсутствие ошибок в недетерминированных функцияхНедетерминированные функции в общем случае выдают разные результаты для одних и тех же входных параметров. Как доказать тестами отсутствие ошибок? Рассмотрим такой пример. Нам надо написать недетерминированную функцию, которая читает системную дату и выдаёт порядковый номер дня недели:
unsigned int get_day_of_week () {
unsigned int day = get_system_date ();
return day % 7; // будем считать, что эпоха началась с понедельника
}
Рассмотрим недетерминированную функцию
static unsigned int value = 0;
unsigned int simulator () {
unsigned int ret = value;
++ value;
return ret;
}
typedef unsigned int (*fn_ptr) ();
// новая версия get_day_of_week
unsigned int get_day_of_week (fn_ptr fun) {
unsigned int day = fun ();
return day % 7;
}
А теперь тесты:
value = 0; if ( get_day_of_week (simulator) != 0) {
printf("Error, value=%d", value); exit; }
value = 1; if ( get_day_of_week (simulator) != 1) {
printf("Error, value=%d", value); exit; }
. . .
value = MAX_INT; if ( get_day_of_week (simulator) != <нечто>) {
printf("Error, value=%d", value); exit; }
В данном случае мы занимаем такую позицию: «Я не знаю, правильно ли работает чужая недетерминированная функция. Не я её написал. Но я знаю, что моя функция работает правильно и я это доказал. Я за неё ручаюсь». Это ещё один камешек в огород Дейкстры. Недетерминированными могут быть не только функции, но и какие-то внешние по отношению к нашей функции переменные. Например, какая-то внешняя переменная непредсказуемо изменяет своё значение, это изменение может делаться операционной системой или параллельным потоком. В этом случае для нашей функции меняется немного. Просто ей передаётся параметром не адрес недетерминированной функции, а адрес недетерминированной переменной. А раз так, то для проведения тестов можно передать функции адрес переменной-симулятора. Как доказать отсутствие ошибок в функциях с побочными эффектамиНапишем функцию, которая производит побочный эффект, которая получает как параметр дату и записывает порядковый номер дня недели.
void set_day_of_week (unsigned int in) {
unsigned int day = in % 7;
put (day); // вывод информации, put производит побочный эффект
}
По аналогии с предыдущим примером функцию, производящую побочный эффект, выносим за пределы нашей функции, пишем функцию-симулятор и в тестах нашей функции передаём адрес симулятора.
static unsigned int value;
void simulator (unsigned int arg) {
value = arg;
}
typedef void (*fn_ptr) (unsigned int);
unsigned int set_day_of_week (fn_ptr fun) {
unsigned int day = in % 7;
fun (day);
}
Тесты:
set_day_of_week (simulator(0)); if ( value != 0) {
printf("Error, input=0, output=%d", value); exit; }
set_day_of_week (simulator(1)); if ( value != 1) {
printf("Error, input=1, output=%d", value); exit; }
. . .
set_day_of_week (simulator(MAX_INT)); if ( value != <нечто>) {
printf("Error, input=MAX_UINT, output=%d", value); exit; }
И здесь мы формулируем свою позицию: «Не буду доказывать безошибочность чужой функции с побочным эффектом. Но безошибочность моей функции я доказал». Побочный эффект может наступать не только при вызове соответствующих функций, но и при записи в некоторые внешние по отношению к нашей функции переменные. Например, запись в глобальную переменную влияет на операционную систему или параллельный поток. В этом случае нашей функции передаётся параметром не адрес функции с побочным эффектом, а адрес такой переменной. А для проведения тестов функции передаётся адрес переменной-симулятора. Как доказать отсутствие ошибок в недетерминированных функциях с побочными эффектамиА теперь рассмотрим самый сложный случай, который сочетает в себе как недетерминированность, так и произведение побочного эффекта. Напишем функцию, которая читает системную дату (в этом проявляется недетерминированность), вычисляет порядковый номер дня недели и производит побочный эффект, записывая этот номер во внешнюю среду.
void get_and_set_day_of_week () {
unsigned int day = get_system_date ();
day %= 7;
put (day); // вывод информации, put производит побочный эффект
}
По аналогии с предыдущими примерами нечистые функции выносим за пределы, пишем симулирующие функции, а в тестах наша функция получит адреса симуляторов.
static unsigned int in_value = 0;
static unsigned int out_value;
unsigned int in_simulator () {
unsigned int ret = in_value;
++ in_value;
return ret;
}
void out_simulator (unsigned int arg) {
out_value = arg;
}
typedef unsigned int (*in_fn_ptr) ();
typedef void (*out_fn_ptr) (unsigned int);
unsigned int get_and_set_day_of_week (in_fn_ptr in_fun, out_fn_ptr out_fun) {
unsigned int day = in_fun () % 7;
out_fun (day);
}
Тесты:
in_value = 0;
get_and_set_day_of_week (in_simulator, out_simulator);
if ( out_value != 0) {
printf("Error, input=%d, output=%d", in_value, out_value); exit; }
in_value = 1;
get_and_set_day_of_week (in_simulator, out_simulator);
if ( out_value != 1) {
printf("Error, input=%d, output=%d", in_value, out_value); exit; }
. . .
in_value = MAX_UINT;
get_and_set_day_of_week (in_simulator, out_simulator);
if ( out_value != <нечто>) {
printf("Error, input=%d, output=%d", in_value, out_value); exit; }
Здесь опять наша позиция такова: «Не буду доказывать безошибочность чужих нечистых функций, но моя функция ошибок не содержит. Я это доказал». ПослесловиеКонечно, в жизни всё сложнее, чем в простеньких примерах. Но идея и способы её достижения, думаю, ясны. Освобождаясь от нечистых функций, вынеся их за пределы и передав как параметр, мы создаём условия для тестирования, доказывающего отсутствие ошибок. Да, в голову могут прийти каверзные вопросы. Например такие:
Но всё это решаемо, теоретических препятствий нет. Но есть ещё один момент, который находится на периферии внимания функционального программирования. Есть такой исчерпаемый ресурс, как память. Когда он заканчивается, то программы перестают работать. В том числе написанные на функциональных языках. Вот такой непредвиденный побочный эффект, который для функционального программирования и вовсе таким не является. Веру в слова Дейкстры, надеюсь, хоть немного пошатнули. Но есть ещё слова Страуструпа: Ограничение возможностей языка с целью предотвращения программистских ошибок в лучшем случае опасно. А мы на примерах выше добились успехов, как раз внося ограничения. И кто тут прав? Post scriptumПосле предварительного обсуждения сделал вывод, что нужно чётче расставить акценты. Существует целое направление в программировании как науке — доказательство корректности программ. Доказательство достигается через верификацию, анализ исходных текстов. К примеру, PVS-Studio так и работает: анализирует, находит ошибки. Но вот доказать безошибочность не может. Выше предложен иной способ. Он предполагает модификацию функций, которая превращает их в чистые, а убираемые нечистые передаются чистым, как параметр. Это позволяет относиться к функциям, как к «черным ящикам». Становится неважным, что там находится внутри. Важно то, что «чёрный ящик» выдаёт правильный результат в ответ на принятые параметры. Для тестирования передаваемые в параметрах адреса нечистых функций заменяются на адреса их симуляторов, а далее делаются вызовы с полным перебором входных параметров. Получение неправильных результатов означает, что в «чёрном ящике» есть ошибка, её надо исправить. И так до тех пор, пока не исчезнут. Из-за того, что «чёрный ящик» является чистой функцией, он не может выдать разные результаты для одинаковых входных параметров. Это гарантирует, что этот ящик (если его не трогали) не может сломаться в дальнейшем. Опубликовано: 2023.01.21, последняя правка: 2023.09.30 20:45
Отзывы
Да, надо обдумать. Gudleifr Я вам не скажу за
Думаю, Вы имели в виду отладку, когда бы запускалось приложение целиком в реальном окружении Нет, я имел в виду проблему остановки. Из неразрешимости которой следует невозможность полного тестирования.
Сама тестируемая функция зациклиться может. Тогда долгое отсутствие результата — это признак наличия ошибки. Это повод к тому, чтобы вернуться к работе над ошибками. Такая же реакция, как и в случае явного указания на ошибку.
На вход тестируемой функции подаются перебираемые параметры, на выходе проверяются результаты Ок. Подаю на вход описание Машины Тьюринга. Жду...
bool is_digit (unsigned char c) {Видите, на вход функции подаётся unsigned char c. Если подать на вход объект «Машина Тьюринга», то он будет отвергнут компилятором по формальным (не говоря уже о других) основаниям: он не имеет тип unsigned char. Поэтому проблема остановки того, чего не будет в программе, просто не возникнет.Жду — Рабинович, как ваше здоровье?— Не дождетесь!
Если подать на вход объект «Машина Тьюринга», то он будет отвергнут компилятором по формальным (не говоря уже о других) основаниям: он не имеет тип unsigned char Не надо играть в обозначения. Вы согласны, что одна Машина Тьюринга не может заранеее судить о поведении другой Машины Тьюринга? Если не согласны, идите спорьте с Тьюрингом. Если согласны, признайте, что полное тестирование невозможно.
_0 _1 _2 _3 _4 _5 _6 _7 _8 _9 _A _B _C _D _E _FПравильность доказана? Доказана. Упорствующие могут ссылаться на недоказанность правильности работы компилятора, операционной системы и процессора, на машину Тьюринга, на тезис Чёрча («правильность или неправильность формальной арифметики недоказуемы средствами самой формальной арифметики»), на законы Паркинсона и британских учёных. Однако это не отменит того факта, что правильность is_digit доказана. И было бы неплохо иметь хорошие средства тестирования, которые могли предъявлять такие подобные доказательства. Доказательства не для научных журналов. А для себя или для заказчика.
Правильность доказана? Разумеется, нет. В зависимости от контекста, цифрами могут считаться и буквы A-Z...Вот, например, аналогичная таблица из одной моей программы: @1251@ DW 0FF00h, 0FF01h, 0FF02h, 0FF03h, 0FF04h, 0FF05h, ... 0FF0FhКоторая из двух правильнее?
В зависимости от контекста, цифрами могут считаться и буквы A-Z. Не знаком с таким контекстом. А классики пишут так:Isdigit(c) — это функция в языке Си, которая может использоваться для проверки того, является ли переданный символ цифрой или нет. Он возвращает ненулевое значение, если это цифра, иначе он возвращает 0. Например, он возвращает ненулевое значение для '0' — '9' и ноль для других. В определении функции is_digit написано, что она имеет входной тип unsigned char, т. е. размер аргумента 1 байт. А вы поднимаете вопрос о двухбайтовом аргументе. Для этого случая нужна другая функция. А is_digit, которая для однобайтового unsigned char, свою задачу решает безупречно, о чём свидетельствует табличка.
А классики пишут так... Или так: цифрой является все от нуля до текущего значения BASE, читая 0-9, A-Z...Isdigit(c) — это функция в языке Си Опять ошибка. Не в Си, а в POSIX.А вы поднимаете вопрос о двухбайтовом аргументе Да, мне так удобнее. И моя таблица также решает задачу безупречно.Вы просто запутались. Методы программирования масштабированием и структурный — это два разных метода. В первом применяется тестирование и нет доказательств правильности. Во втором — наоборот, но в нем надо доказывать все с самого начала, явно описывая контексты.
bool is_digit (unsigned char c) {Без ненужного раздувания он должен был выглядеть так:bool is_digit (unsigned char c) {
Вы правы, мой код содержит ошибку. Исправил. тема — это наброс Тема — не наброс, а стремление увеличить надёжность программ (что вытекает из «философии»), а для этого все средства хороши. От того, что опровергается какой-то постулат на каком-то подмножестве случаев, Дейкстра не будет втоптан в грязь, а я не вознесусь вместо него ввысь.Есть такая техника тестирования — фаззинг, когда программы проверяются как можно большим числом вариантов параметров. Да, серьёзно помогает в поиске ошибок. Но не гарантирует отсутствие ошибок. Хотя бы из-за наличия побочных эффектов. Моё предложение — обеспечить чистоту функции и после этого можно доказывать её безошибочность. А корректность вынесенных наружу нечистых функций (а это — ввод/вывод, который зависит от ОС) — это уже не моя забота.
#include <библиотека ввода/вывода>подставить #include "библиотека с симулякрами"где функции с такими же именами и сигнатурой, как и у функций ввода/вывода, обеспечивают перебор параметров и фиксируют результаты.
Есть другой вариант. Можно дублировать функции, для этого как раз пригодится вынесение нечистоты за пределы функций (Это ответ на предложение о подмене библиотечных функций их симуляторами). Дублирующие функции может написать кто-то другой, чтобы соблюсти чистоту эксперимента. Тогда можно делать перебор всех вариантов и выявлять несовпадения, которые говорят об ошибочности либо основной, либо дублирующей функции. И добиваться полного совпадения результатов. Правда, надо ещё проверять, не совпадает ли код основной и дублирующих функций, поскольку сравнивать результаты одинаковых функций бессмысленно.
Написать автору можно на электронную почту |
2023/01/24 22:49, Неслучайный читатель