flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Снятая правка обязана красить тест — иначе она ничего не держит

Дисциплина, применяемая к каждой работе. Порядок:

  1. снять правку;
  2. назвать покрасневший тест поимённо;
  3. вернуть правку;
  4. убедиться, что снова зелено.

Что это ловит. Правку, которая ничего не держит: либо тест не тот, либо правка не нужна. Если снятие ничего не меняет — работа не сделана, как бы хорошо она ни выглядела.

Сильная форма — назвать вклад числом. Пример из работы над фактами о встроенных формах:

оба правила            43 функции корпуса
без правила формы      30
без правила свёртки    27
без обоих              17

Сумма нарочно не сходится (17+13+10=40): трём функциям нужны оба правила сразу. Такое разложение говорит больше, чем итоговое число.

Третья форма — снятие, которое НЕ покраснело, тоже результат, и его надо записать, а не замять. Из журнала упреждающей записи (work/zhurnal-wal) по очереди вынимали четыре решения, корпус из 61 входа краснел так:

снят канон номера (приняты ведущие нули)        1 вход
снята метка конца записи в разборе              3 входа
снята поглощаемость сбоя после мусора           3 входа
снята метка конца из ПЕЧАТИ записи             14 примеров
снят потолок накопления цифр                    0 входов

Последняя строка — не дыра в корпусе. Она означает, что потолок не держит ответа: за ответ отвечают проверка канона и точная сетка double, а потолок стережёт память (без него строка цифр растёт вместе с мусором на входе). Записано это отдельной проверкой в наборе, которая покраснеет, если положение дел изменится, — то есть измеренный ноль поставлен под наблюдение, а не забыт (a-measured-zero-is-valuable).

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

Связано: byte-for-byte-comparison, checks-that-stopped-comparing, zero-axioms, a-measured-zero-is-valuable