Антипаттерны: что не стоит выражать спецификацией

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

Как читать этот каталог

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

Все ответы получены двоичным flang 0.7.29. Программы с пометкой «ошибка» нарочно не проходят проверку; остальные проходят flang check --proof и flang test — их можно скопировать в песочницу как есть.

Эффекты в спецификации

1. Действие внутри функции

Задача. При крупной покупке отправить клиенту письмо с промокодом.

модуль «Письма»

объект «Покупка»
  «сумма»: неотрицательное
  «почта»: строка

тотальная функция «Большая покупка»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 10000
    то отправить письмо на покупка.«почта»
    иначе 0

Что произойдёт. Проверка падает:

FLANG_UNKNOWN_NAME в файле a1.flang, строка 11, столбец 8: имя «отправить» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»

Глагола «отправить» в языке нет, и выдумать его нельзя: функция flang вычисляет значение и больше ничего не делает. Сеть, файлы и процессы ей недоступны.

Как правильно. Решение и действие разделяются. Функция отвечает на вопрос «положено ли письмо», а отправку описывает план: функция возвращает команду («Запросить» — HTTP-запрос к службе рассылки), выполняет её хозяин (flang io), а ответ приходит обратно в ту же функцию. Логика остаётся чистой и проверяется примерами без сети:

модуль «Письмо о промокоде»

объект «Покупка»
  «сумма»: неотрицательное
  «почта»: строка

тотальная функция «Нужно письмо с промокодом»
  принимает покупка: «Покупка»
  возвращает признак
  обеспечивает «мелкой покупке письма нет» если покупка.«сумма» меньше 10000 то результат равен нет иначе да
  пример «на десять тысяч письмо положено»
    дано покупка равно запись «Покупка» с «сумма» равным 10000 и «почта» равным "a@example.org"
    ожидается да
  если покупка.«сумма» меньше 10000
    то нет
    иначе да

тип «Ход»
  вариант «Отправляем»
  вариант «Ждём ответа»

план «Отправить письмо»
  состояние «Ход»
  начинает с «Начало»
  обрабатывает «Дальше»

тотальная функция «Начало»
  возвращает «Ход»
  вариант «Отправляем»

тотальная функция «Дальше»
  принимает ход: «Ход», отклик: «Отклик»
  возвращает «Продолжение»
  пример «первым делом уходит запрос к службе рассылки»
    дано ход равно вариант «Отправляем»
    дано отклик равно вариант «Пока ничего»
    ожидается вариант «Сделать» с поручение равным (вариант «Запросить» с способ равным "POST" и адрес равным "http://127.0.0.1:8025/send" и тело равным "промокод") и потом равным (вариант «Ждём ответа»)
  пример «служба ответила — план закончен»
    дано ход равно вариант «Ждём ответа»
    дано отклик равно вариант «Ответ сети» с код равным 202 и тело равным "принято"
    ожидается вариант «Конец работы» с значение равным "принято"
  разбор ход
    случай вариант «Отправляем»
      то вариант «Сделать» с поручение равным (вариант «Запросить» с способ равным "POST" и адрес равным "http://127.0.0.1:8025/send" и тело равным "промокод") и потом равным (вариант «Ждём ответа»)
    случай вариант «Ждём ответа»
      то разбор отклик
        случай вариант «Ответ сети» с код как код и тело как тело
          то вариант «Конец работы» с значение равным тело
        случай вариант «Сбой» с код как код и сообщение как сообщение
          то вариант «Провал» с код равным код и сообщение равным сообщение
        случай любое
          то вариант «Провал» с код равным "FLANG_IO_ORDER" и сообщение равным "ждали ответ сети"

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

2. Действие, спрятанное в имя

Опаснее вариант, где эффекта в коде нет, а есть только в имени.

модуль «Уведомления»

объект «Заказ»
  «номер»: строка
  «оплачен»: признак

тотальная функция «Письмо клиенту отправлено»
  принимает заказ: «Заказ»
  возвращает признак
  пример «оплаченный заказ»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да
    ожидается да
  заказ.«оплачен»

Что произойдёт. Ничего: модель проходит проверку, диагностик нет. Ловушка в имени — оно названо свершившимся фактом, и через месяц кто-нибудь прочитает да как подтверждение, что письмо ушло. Функция говорит другое: заказ оплачен. Отправку никто не проверял.

Как правильно. Имя функции называет разрешение или обязанность: «Нужно уведомить клиента». Факт отправки возвращается из системы рассылки в данные и становится полем объекта — тогда о нём можно что-то утверждать.

3. Повторы, таймауты, очереди

Задача. После сбоя платежа повторить через пять секунд, потом через тридцать, дальше — не повторять.

Ожидания, расписания и очереди в языке нет: ждать 5 секунд даст тот же FLANG_UNKNOWN_NAME, что и в пункте 1.

Как правильно. Разделите «сколько ждать» и «кто ждёт». Политика повторов — чистая таблица, её стоит зафиксировать; исполнение задержки, идемпотентный ключ и дедупликация остаются в приложении.

модуль «Повторы платежа»

объект «Неудачная попытка»
  «номер попытки»: неотрицательное
  «ошибка окончательная»: признак

тип «Повтор»
  вариант «Повторить через» содержит секунд: неотрицательное
  вариант «Не повторять»

тотальная функция «Следующий повтор»
  принимает попытка: «Неудачная попытка»
  возвращает «Повтор»
  пример «после первой попытки ждём пять секунд»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 1 и «ошибка окончательная» равным нет
    ожидается вариант «Повторить через» с секунд равным 5
  пример «окончательная ошибка не повторяется»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 1 и «ошибка окончательная» равным да
    ожидается вариант «Не повторять»
  пример «третья попытка не назначается»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 3 и «ошибка окончательная» равным нет
    ожидается вариант «Не повторять»
  если попытка.«ошибка окончательная»
    то вариант «Не повторять»
    иначе если попытка.«номер попытки» равен 1
      то вариант «Повторить через» с секунд равным 5
      иначе если попытка.«номер попытки» равен 2
        то вариант «Повторить через» с секунд равным 30
        иначе вариант «Не повторять»

«Не повторять» здесь — отдельный вариант ответа, а не ноль секунд. Приложение обязано разобрать оба случая и не может принять отказ за «повторить сразу».

Внешний мир: время, случайность, сеть

4. Внешний источник как поле

Задача. Пересчитать тариф по текущему курсу валюты из внешнего API.

модуль «Тарифы»

объект «Отправление»
  «вес»: неотрицательное
  «курс валюты» является запросом

Что произойдёт.

FLANG_UNKNOWN_NAME в файле a4.flang, строка 3, столбец 1: неизвестный тип «запросом»

У поля бывает только объявленный тип: встроенный (число, строка, признак, неотрицательное) или свой, заведённый словом тип или объект. Незнакомое слово после является — ошибка, а не новый тип. Прежняя поверхность FTS такое слово молча принимала; flang отказывает сразу.

Как правильно. Курс получает приложение — с таймаутом, кэшем и запасным значением. В модель он приходит обычным полем «курс валюты»: число.

5. «Сегодня» внутри правила

Задача. Начислить пени, если счёт просрочен относительно сегодняшнего дня.

модуль «Пени»

объект «Счёт»
  «срок оплаты»: неотрицательное

тотальная функция «Просрочен»
  принимает счёт: «Счёт»
  возвращает признак
  счёт.«срок оплаты» меньше сегодня

Что произойдёт.

FLANG_UNKNOWN_NAME в файле a5.flang, строка 9, столбец 29: имя «сегодня» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»

Часов в языке нет, и это не недоработка: функция, которая сегодня отвечает одно, а завтра другое, не может нести примеры. Типа даты в flang 0.7.29 тоже нет.

Как правильно. Время вычисляет приложение и передаёт как данные — здесь номером дня (число дней от 1 января 1970 года), чтобы сравнение было обычным сравнением чисел:

модуль «Пени»

объект «Счёт»
  «сумма»: неотрицательное
  «день срока оплаты»: неотрицательное

тотальная функция «Дней просрочки»
  принимает счёт: «Счёт», сегодня: неотрицательное
  возвращает число
  обеспечивает «до срока просрочки нет» если сегодня не больше счёт.«день срока оплаты» то результат равен 0 иначе да
  пример «в день срока просрочки ещё нет»
    дано счёт равно запись «Счёт» с «сумма» равным 10000 и «день срока оплаты» равным 20650
    дано сегодня равно 20650
    ожидается 0
  пример «три дня после срока»
    дано счёт равно запись «Счёт» с «сумма» равным 10000 и «день срока оплаты» равным 20650
    дано сегодня равно 20653
    ожидается 3
  если сегодня не больше счёт.«день срока оплаты»
    то 0
    иначе сегодня минус счёт.«день срока оплаты»

Обещание «до срока просрочки нет» доказано для всех входов. Пример с конкретным днём воспроизводится через год так же, как сегодня, и разбор спорного начисления задним числом возможен.

6. Случайность: A/B, выборка, случайная скидка

Задача. Половине покупателей выдать скидку и сравнить конверсию.

модуль «Эксперимент»

тотальная функция «Скидка по жребию»
  принимает сумма: неотрицательное
  возвращает число
  если случайное число меньше 0.5
    то (сумма умножить на 5) делить на 100
    иначе 0

Что произойдёт. FLANG_UNKNOWN_NAME в файле a6.flang, строка 6, столбец 8: имя «случайное» не связано. Случайных чисел в языке нет.

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

модуль «Эксперимент»

тип «Группа»
  вариант «Контроль»
  вариант «Скидка пять процентов»

тотальная функция «Скидка эксперимента»
  принимает сумма: неотрицательное, группа: «Группа»
  возвращает число
  пример «контрольная группа без скидки»
    дано сумма равно 2000
    дано группа равно вариант «Контроль»
    ожидается 0
  пример «опытная группа получает пять процентов»
    дано сумма равно 2000
    дано группа равно вариант «Скидка пять процентов»
    ожидается 100
  разбор группа
    случай «Контроль»
      то 0
    случай «Скидка пять процентов»
      то (сумма умножить на 5) делить на 100

Группа становится частью входа: пример на каждую ветку эксперимента пишется так же, как на любую другую.

Логика правил

7. Перекрывающиеся правила складываются

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

модуль «Скидка по ступеням»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «От тысячи»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 1000
    то (покупка.«сумма» умножить на 5) делить на 100
    иначе 0

тотальная функция «От десяти тысяч»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 10000
    то (покупка.«сумма» умножить на 10) делить на 100
    иначе 0

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  («От тысячи» от покупка) плюс («От десяти тысяч» от покупка)

Что произойдёт.

FLANG_EXAMPLE: пример «крупная покупка» функции «Скидка»: значение не совпало с ожидаемым: ожидалось 2000, получено 3000

При сумме 20000 истинны оба условия, и вклады сложились: 1000 плюс 2000. Сложение функций — это сложение, а не выбор. Здесь ошибку поймал пример; без него модель была бы зелёной.

Как правильно. Взаимное исключение выражается одной цепочкой если … иначе если: ветки проверяются по порядку, и выполняется ровно одна.

модуль «Скидка по ступеням»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  пример «средняя покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 5000
    ожидается 250
  пример «ровно тысяча»
    дано покупка равно запись «Покупка» с «сумма» равным 1000
    ожидается 50
  если покупка.«сумма» не меньше 10000
    то (покупка.«сумма» умножить на 10) делить на 100
    иначе если покупка.«сумма» не меньше 1000
      то (покупка.«сумма» умножить на 5) делить на 100
      иначе 0

Складывать вклады правил законно тогда, когда это и есть бизнес-правило: «пять процентов постоянному клиенту сверх скидки за объём». Тогда так и называйте функции и закрывайте сложение примером на пересечении.

8. Цепочка если по виду значения вместо разбор

Задача. Разрешить отгрузку заказа по его статусу.

модуль «Статусы»

тип «Статус»
  вариант «Создан»
  вариант «Оплачен»
  вариант «Готов к отгрузке»
  вариант «Отменён»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  пример «отменённый не отгружается»
    дано статус равно вариант «Отменён»
    ожидается нет
  если статус равен вариант «Создан»
    то нет
    иначе если статус равен вариант «Оплачен»
      то нет
      иначе да

Что произойдёт.

FLANG_EXAMPLE: пример «отменённый не отгружается» функции «Можно отгрузить»: значение не совпало с ожидаемым: ожидалось false, получено true

Отменённый заказ молча ушёл в последний иначе и получил разрешение. Пример это поймал; новый вариант статуса, добавленный через полгода, поймать будет нечем.

Как правильно. Выбор по виду значения пишется через разбор: компилятор требует назвать все варианты. Тот же код с забытым вариантом:

модуль «Статусы»

тип «Статус»
  вариант «Создан»
  вариант «Оплачен»
  вариант «Готов к отгрузке»
  вариант «Отменён»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  разбор статус
    случай «Создан»
      то нет
    случай «Оплачен»
      то нет
    случай «Готов к отгрузке»
      то да

FLANG_MATCH_NOT_EXHAUSTIVE в файле a8b.flang, строка 12, столбец 3: разбор «Статус» не покрывает «Отменён»

Пропущенный случай виден при проверке, а не у человека на складе.

9. Обещание, которое выполняется обрезкой

Задача. Ограничить скидку пятнадцатью тысячами.

модуль «Потолок скидки»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка не больше пятнадцати тысяч» результат не больше 15000
  пример «покупка на сто тысяч постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 20000
  если покупка.«постоянный клиент»
    то (покупка.«сумма» умножить на 20) делить на 100
    иначе (покупка.«сумма» умножить на 15) делить на 100

Что произойдёт. Обещание обеспечивает не правит результат, а проверяет его. Пример на ста тысячах честно ломается:

FLANG_EXAMPLE: пример «покупка на сто тысяч постоянного клиента» функции «Скидка»: FLANG_PROPERTY: нарушено свойство «скидка не больше пятнадцати тысяч» функции «Скидка»

Так и должно быть: правила насчитали 20 000, бизнес обещал не больше 15 000 — это находка. Соблазнительный ход — добавить обрезку в тело:

модуль «Потолок скидки»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка по правилам»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«постоянный клиент»
    то (покупка.«сумма» умножить на 20) делить на 100
    иначе (покупка.«сумма» умножить на 15) делить на 100

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка не больше пятнадцати тысяч» результат не больше 15000
  пример «покупка на сто тысяч постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 15000
  если («Скидка по правилам» от покупка) не больше 15000
    то «Скидка по правилам» от покупка
    иначе 15000

Теперь ответ безупречен:

постусловие «скидка не больше пятнадцати тысяч» функции «Скидка» — доказано сведением цели с телом функции: правило «разбор цели по условию», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно

Доказано — и ничего не значит. Обещание стало повторением тела: правила по-прежнему насчитывают 20 % там, где бизнес ждёт не больше 15 000, а обрезка это прячет. Ошибка правил переехала из отчёта в молчание.

Как правильно. Потолок закладывается в сами правила (отдельной веткой «очень крупная покупка», как в order-discount.flang), а обещание остаётся проверкой: если правила его нарушают, должен узнать владелец правила, а не если … то 15000. То же касается тавтологий вроде результат равен (0 минус х) при теле 0 минус х: такое обещание принимается даром и не проверяет ничего.

Примеры и доказательства

10. Модель без примеров

модуль «Без примеров»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше десятой части» результат не больше (сумма делить на 10)
  если сумма не меньше 10000
    то (сумма умножить на 10) делить на 100
    иначе 0

Что произойдёт. Голая проверка зелёная:

a10.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Отчёт о доказательствах говорит правду:

постусловие «скидка не больше десятой части» функции «Скидка» — объявлено, не доказано: ни теоремы, ни примеров. Его считает рантайм после каждого возврата — на тех входах, которые придут

и flang check --proof выходит кодом 3. Обещание без примера проверяется только при работе — на тех входах, что придут от пользователей. Спецификацией текст становится тогда, когда в нём появляются числа, о которых договорился бизнес: минимум по примеру на ветку и по примеру на границу.

11. Пример, подогнанный под реализацию

Самый тихий способ обесценить конструкцию. Вернитесь к пункту 7: пример честно ждёт 2000, функция даёт 3000, проверка красная.

Дальше развилка. Правильный ход — чинить правила: расхождение и есть находка. Соблазнительный — исправить ожидается 3000: CI зелёный, коммит маленький. После этого пример перестаёт быть требованием и становится слепком поведения. Модель считает не то, что обещано клиенту, но теперь об этом не узнает никто.

Правило код-ревью: изменение строки ожидается в одном коммите с изменением правил считается изменением договорённости с бизнесом и требует ссылки на источник — тикет, приказ, тариф. Без ссылки — возврат.

12. Код 0 или ответ на фактах, выданные за доказательство

Задача. Показать аудиту, что модель скидки держит потолок, а заказ ЗК-7781 можно отгружать.

Что происходит. В CI стоит flang check, он зелёный — и это читают как «доказано». На модели курса order-discount.flang:

static/spec/models/order-discount.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Без ключа --proof о доказательствах не сказано ни слова. С ключом:

постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 5 значений (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет
static/spec/models/order-discount.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 4: доказано 1, условно 0, сетка 3, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

«Сетка 5 значений» — потолок проверен на пяти примерах, как пятью юнит-тестами. Для всех входов он не доказан.

Вторая подмена — ответ flang facts на данных одного заказа. Утверждение «заказ с этим номером отгружается» на order-shipment.facts.json выполнено: "holds": true, "status": "verified". Это факт об одном заказе в одном снимке данных, а не правило. Правило — обещания функции «Можно отгрузить» («неоплаченный заказ не отгружается»), и о них отчёт говорит «доказано» — для всех заказов.

Как правильно. В CI — flang check --proof, и код 3 не считается зелёным. Аудиту идёт строка отчёта о доказательствах по каждому обещанию, а не цвет сборки. Ответ на фактах — это журнал конкретного решения, его хранят рядом с решением. И помните, что flang run недоказанную программу без ключа --trust не считает вовсе.

13. разбор по да и нет вместо если

Привычка из пункта 8 — «всё через разбор» — заходит слишком далеко, когда разбирают результат сравнения.

модуль «Порог»

тотальная функция «Не ниже порога»
  принимает число: неотрицательное, порог: неотрицательное
  возвращает число
  обеспечивает «не ниже порога» результат не меньше порог
  пример «выше порога»
    дано число равно 7
    дано порог равно 5
    ожидается 7
  пример «ниже порога»
    дано число равно 3
    дано порог равно 5
    ожидается 5
  разбор (число не меньше порог)
    случай да
      то число
    случай нет
      то порог

Что произойдёт. Код работает, примеры сходятся, но обещание «не ниже порога» остаётся сетка 2 значения, а flang check --proof — кодом 3. Ядро доказательств сводит цель по условию если; разбор признака по случаям да и нет это правило ломает.

Как правильно. Сравнение чисел и строк — через если. Тот же код с если число не меньше порог то число иначе порог:

модуль «Порог»

тотальная функция «Не ниже порога»
  принимает число: неотрицательное, порог: неотрицательное
  возвращает число
  обеспечивает «не ниже порога» результат не меньше порог
  пример «выше порога»
    дано число равно 7
    дано порог равно 5
    ожидается 7
  пример «ниже порога»
    дано число равно 3
    дано порог равно 5
    ожидается 5
  если число не меньше порог
    то число
    иначе порог

a13bn.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1, условно 0, сетка 0, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 0

разбор оставьте для вопроса «какого вида значение» и «пуст ли список».

14. «Очевидное» обещание на типе число

Задача. Модуль числа неотрицателен — что тут проверять.

модуль «Модуль числа»

тотальная функция «Модуль»
  принимает х: число
  возвращает число
  обеспечивает «модуль неотрицателен» результат не меньше 0
  пример «минус три»
    дано х равно -3
    ожидается 3
  если х не меньше 0
    то х
    иначе 0 минус х

тотальная функция «Модуль не числа»
  возвращает число
  пример «ноль на ноль»
    ожидается 0
  «Модуль» от (0 делить на 0)

Что произойдёт.

FLANG_EXAMPLE: пример «ноль на ноль» функции «Модуль не числа»: FLANG_PROPERTY: нарушено свойство «модуль неотрицателен» функции «Модуль»

Числа flang — машинные числа с плавающей точкой (IEEE-754). 0 делить на 0 проходит проверку типов и даёт «не число»; любое сравнение с ним ложно, и «модуль не меньше нуля» перестаёт быть правдой. По той же причине тот же если из пункта 13 с типом число вместо неотрицательное не доказывается: ядро помнит о «не числе». Ещё одна ловушка того же рода — минус ноль: −0 и 0 различаются при сравнении на равенство.

Как правильно. Объявляйте неотрицательное там, где значение неотрицательно: это даёт ядру границы, и половина обещаний доказывается сама. Деньги считайте целыми копейками (тип сотых), а деление делайте там, где делитель заведомо не ноль.

Границы модели

15. Гигантский модуль

Задача. «Опишем компанию одной моделью, чтобы всё было в одном месте».

Первое, обо что споткнётся такая модель, — омонимы. Заказ в продажах и заказ в логистике различны, и одноимённое объявление отклоняется:

модуль «Компания»

объект «Заказ»
  «номер»: строка
  «сумма»: неотрицательное

объект «Заказ»
  «номер»: строка
  «вес»: неотрицательное

FLANG_TYPE в файле g1.flang, строка 7, столбец 1: тип «Заказ» объявлен дважды

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

модуль «Компания»

объект «Заказ»
  «номер»: строка
  «сумма»: неотрицательное
  «вес отправления»: неотрицательное
  «регион доставки»: строка
  «кредитный рейтинг»: неотрицательное
  «канал продаж»: строка

тотальная функция «Скидка»
  принимает заказ: «Заказ»
  возвращает число
  пример «большая покупка»
    дано заказ равно запись «Заказ» с «сумма» равным 20000
    ожидается 2000
  если заказ.«сумма» не меньше 10000
    то (заказ.«сумма» умножить на 10) делить на 100
    иначе 0

FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «номер» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «вес отправления» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «регион доставки» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «кредитный рейтинг» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «канал продаж» записи «Заказ»

Это не придирка, а измеритель связности: цена примера растёт вместе с размером объекта, и объект-свалка делает примеры непереносимыми задолго до того, как станет неудобно читать модель.

Как правильно. Модуль — это ограниченный контекст: один язык, один владелец, одна причина для изменения. Функция принимает только то, что участвует в её решении, а пересечения оформляются отдельными объектами с собственными именами.

16. Строковые статусы вместо типа с вариантами

Задача. «У заказа есть статус, сравним его со строкой — зачем варианты».

модуль «Статус строкой»

объект «Заказ»
  «номер»: строка
  «статус»: строка

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  заказ.«статус» равен "готов к отрузке"

Что произойдёт. Проверка зелёная, и даже --proof отвечает кодом 0 — утверждать в модели нечего. Опечатка в "готов к отрузке" — обычный строковый литерал, сравнивать компилятору не с чем. Функция никогда не отвечает да; при живом примере это видно, без примера — никак.

Как правильно. Всё, к чему привязаны переходы и разрешения, объявляется типом с вариантами. Та же опечатка в варианте:

модуль «Статус вариантом»

тип «Статус»
  вариант «Создан»
  вариант «Готов к отгрузке»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  разбор статус
    случай «Создан»
      то нет
    случай «Готов к отрузке»
      то да

FLANG_UNKNOWN_NAME: неизвестный вариант «Готов к отрузке»
FLANG_MATCH_NOT_EXHAUSTIVE в файле s2.flang, строка 10, столбец 3: разбор «Статус» не покрывает «Готов к отгрузке»

Опечатку ловит компилятор, а не оператор склада. Строка остаётся строкой там, где она действительно данные: номер, регион, адрес.

Практика в песочнице

Добавьте функцию «Средний чек»: если сумма не меньше 1000, то 7 процентов от суммы, — и прибавьте её к итогу в «Рассчитать скидку». Проверьте. Покраснеют шесть примеров: «обычная покупка» получит 350 вместо 0, а две крупные покупки дадут FLANG_PROPERTY: нарушено свойство «скидка ограничена» — пункты 7 и 9 этого каталога в одном действии.

Добавьте в объект поле «курс валюты» является запросом и найдите в ответе FLANG_UNKNOWN_NAME. Затем объявите его как «курс валюты»: число и убедитесь, что проверка снова проходит.

Сдвиньте порог дальней зоны с 500 на 600 километров, чтобы один пример перестал сходиться. Затем подгоните строку ожидается под новый результат и сформулируйте одним предложением, что модель перестала гарантировать.

Найдите в отчёте два доказанных обещания функции «Можно отгрузить». Замените в её теле иначе нет на иначе да и проверьте снова: оба обещания станут сетка 2 значения, хотя примеры по-прежнему сходятся. Объясните, почему зелёные примеры здесь ничего не гарантируют.

Чек-лист код-ревью модели

1. Нет ли в модели глаголов действия — «отправить», «списать», «повторить»? Действие описывает план, решение — функция.
2. Не названа ли функция свершившимся фактом вместо разрешения или обязанности?
3. Не приходит ли в модель «сегодня», курс или жребий изнутри? Внешнее приходит полем или аргументом.
4. Могут ли две функции-правила дать вклад одновременно? Тогда это сложение, а не выбор, — и на пересечении нужен пример.
5. Нет ли цепочки если … иначе если по виду значения? Нужен разбор.
6. Нет ли разбор по да и нет над сравнением? Нужен если.
7. Закрыта ли каждая граница примером — значение ровно на пороге, а не рядом?
8. Не обрезает ли тело результат под обещание? Доказанное обещание, которое повторяет тело, не проверяет ничего.
9. Есть ли у каждого обещания пример? Без него оно «объявлено, не доказано».
10. Стоит ли в CI flang check --proof, и не считается ли код 3 зелёным?
11. Не менялась ли строка ожидается вместе с правилами без ссылки на решение бизнеса?
12. Где тип число можно заменить на неотрицательное или сотых?
13. Все ли поля объекта нужны функции? Лишние оплачиваются в каждом примере.
14. Нет ли в модуле объектов из чужого контекста — по имени, по владельцу, по причине изменения?
15. Статусы — тип с вариантами, а не строки?

Кейсы каталога по этой теме