Правила, порядок и обещания: как считается решение

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

Минимальный пример

модуль «Продажи»

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

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

Объект описывает форму входа. Функция называет вход (принимает), тип результата (возвращает) и тело — последним, одной формой. Слово тотальная — обещание, что функция завершается на любом входе; компилятор его доказывает. Нуля «по умолчанию» здесь нет: иначе 0 написан автором правила.

Что делает компилятор

1. Разбирает файл и сверяет типы: поля в теле и в примерах существуют, не меньше сравнивает числа, ветви если дают один тип.
2. Доказывает тотальная. Здесь рекурсии нет, и отчёт так и пишет: «доказано композицией: рекурсии нет».
3. Вычисляет каждый пример и сравнивает результат с ожидается. Несовпадение — ошибка проверки, код 1.
4. С ключом --proof — судит каждое обещание обеспечивает: доказано для всех входов, проверено только на примерах или не доказано никак.

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

Правила — это функции, а не цепочка if/else

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

модуль «Продажи»

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

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

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

тотальная функция «Промокод на крупный заказ»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«промокод» равен "ЛЕТО2026" и притом покупка.«сумма» не меньше 15000 и притом покупка.«сумма» не больше 100000
    то (покупка.«сумма» умножить на 7) делить на 100
    иначе 0

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

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка ограничена» результат не больше 22000
  пример «обычная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 5000 и «постоянный клиент» равным нет и «промокод» равным "НЕТ"
    ожидается 0
  пример «крупная покупка без промокода»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным нет и «промокод» равным "ЗИМА"
    ожидается 2000
  пример «крупная покупка постоянного клиента с промокодом»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным да и «промокод» равным "ЛЕТО2026"
    ожидается 4400
  пример «покупка ровно на потолок скидки»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да и «промокод» равным "ЛЕТО2026"
    ожидается 22000
  («Большая покупка» от покупка) плюс («Постоянный клиент» от покупка) плюс («Промокод на крупный заказ» от покупка) плюс («Очень крупная покупка» от покупка)

Для примера с двадцатью тысячами срабатывают три правила из четырёх: 10 % + 5 % + 7 % от 20 000 дают 4 400. Ни одно правило не отменяет другое — их результаты складываются.

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

Если правила должны исключать друг друга — «первое подходящее» — это уже не сумма, а одна функция с если … иначе если:

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

тотальная функция «Ставка доставки»
  принимает вес: неотрицательное
  возвращает число
  обеспечивает «ставка не больше тысячи» результат не больше 1000
  пример «тяжёлое отправление»
    дано вес равно 25
    ожидается 1000
  пример «среднее отправление»
    дано вес равно 12
    ожидается 600
  если вес больше 20
    то 1000
    иначе если вес больше 10
      то 600
      иначе 300

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

Сравнения и проценты

Сравнений шесть: равен, не равен, больше, меньше, не больше, не меньше. равен и не равен работают для числа, строки и признака. Остальные четыре — только для чисел, и это проверяется до запуска:

FLANG_TYPE … левый операнд сравнения «lt» имеет тип строка: сравнения порядка допустимы только для чисел

Условия соединяются словами и притом. Строки сравнивают через равен, даты — только после того, как приложение превратило их в числа (календарного типа нет, см. главу о типах).

Процент записывается двумя способами: 10 процентов от сумма или (сумма умножить на 10) делить на 100. Модели курса пишут второй — так видна каждая операция. Числа — IEEE 754, поэтому для денег без ошибок округления есть тип сотых: целое число копеек.

Обещание — постусловие, а не автокоррекция

обеспечивает — утверждение о результате на любом входе. Если пример его нарушает, компилятор не подрезает скидку до предела. Он останавливает проверку. Затяните потолок в модели выше до 3000:

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

flang check выходит кодом 1. Напечатанная функция ведёт себя так же: вызов с суммой 20 000 бросает ошибку с кодом FLANG_PROPERTY. Она не возвращает 4400 и не обрезает скидку до 3000.

Это граница, а не недоработка. Тихая коррекция спрятала бы ошибку в правиле или во входе. Ошибка наружу заставляет её увидеть и исправить в самом правиле.

Если потолок действительно часть правила — «скидка не больше 22 000, даже если надбавки насчитали больше», — его пишут в теле, а не в обещании. Тогда читатель видит, что обрезка — решение бизнеса, а обещание о потолке доказывается:

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

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

Условие стоит так, чтобы совпасть с обещанием: в ветви то известно, что итог не больше 22 000. Перевёрнутая запись если итог больше 22000 то 22000 иначе итог не доказывается. Итог имеет тип число, а среди чисел IEEE 754 есть NaN. Для него оба сравнения ложны: ветвь иначе вернула бы NaN, а NaN не меньше и не больше потолка.

Что ядро доказывает, а что нет

flang check --proof судит каждое обещание отдельно. Для модели выше:

  постусловие «за очень крупную покупку ровно потолок» функции «Очень крупная покупка» — доказано сведением цели с телом функции: правило «ограниченность точным потолком по построению», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 4 значения (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

Первое обещание доказано для всех входов: в каждой ветви тела стоит число не больше 22 000. Второе — «сетка 4 значения»: оно проверено только на четырёх примерах функции, и это не доказательство. Итоговая строка отчёта:

discount-promo.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 2: доказано 1, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

Код 3 — не ошибка программы. Он значит «не всё доказано». Что доказывается само:

• ветви если, где в каждой стоит число в пределе (потолок, порог);
• импликации над признаками: «если не оплачен, то результат — нет»;
• длина результата отобразить и отфильтровать;
• границы, которые следуют из типов аргументов (неотрицательное).

Что не доказывается: арифметика процентов под потолком. Что 22 % от суммы не больше 22 000, когда сумма не больше 100 000, ядро не выводит — такое обещание остаётся проверенным на примерах, а в напечатанном коде — проверкой при каждом вызове. Связать обещания двух функций через сложение теоремой тоже нельзя: ядро отвечает FLANG_PROOF_STEP.

Детерминированность и границы правила

Одни и те же входные данные всегда дают один и тот же результат: функция не читает часы, не ходит наружу и не хранит состояние между вызовами. Поэтому её проверяют без моков, а песочница, flang run и напечатанный код обязаны совпасть.

Хорошие кандидаты в правило: скидка, тариф, комиссия, классификатор, лимит, решение «разрешить / отклонить» по понятным порогам. Плохие: «отправить письмо», «получить курс валют из сети», «записать заказ в транзакции». Для работы с миром во flang есть план: функция возвращает описание действия, а выполняет его тот, кто запустил программу. Само правило остаётся чистым.

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

1. Посчитайте в уме скидку для 12 000 без статуса постоянного клиента, затем допишите пример с этим входом и проверьте. Добавьте статус — результат вырастет ровно на 5 % от той же суммы.
2. Поменяйте потолок 22000 в обещании «скидка ограничена» на 3000 и прочитайте ответ: нарушенное обещание называют два примера.
3. Найдите в отчёте о доказательствах, какое из двух обещаний доказано, а какое проверено только на примерах.

Найдите обещание «базовый тариф не ниже трёхсот» и объясните, почему оно доказано, а «тариф не опускается ниже базового» — нет.

Типичные ошибки

• FLANG_PARSE … у 'если' нет ветки 'то' — условия соединены словом и вместо и притом, и разбор принял остаток строки за что-то другое.
• FLANG_TYPE … объявлена как неотрицательное, а тело даёт число — деление и умножение дают число. Объявите результат число или перестройте выражение.
• FLANG_EXAMPLE … FLANG_PROPERTY: нарушено свойство — пример ломает обещание. Это не синтаксис, а сигнал: правило или вход выводят результат за объявленную границу. Исправьте правило или осознанно поменяйте предел.
• Код 3 принят за успех. flang check --proof с кодом 3 значит, что часть обещаний только проверена на примерах. В сборке его нужно различать с кодом 0.

Чек-лист

• У функции есть принимает, возвращает и тело; тотальная доказана.
• Независимые надбавки — отдельные функции, которые складываются.
• «Первое подходящее» — одна функция с если … иначе если или разбор.
• Сравнения порядка — только для чисел; строки — через равен.
• Обещание — проверка результата, а не обрезка. Обрезка, если она нужна, — ветвь тела.
• Я знаю, какие обещания модели доказаны, а какие держатся только на примерах, — по отчёту flang check --proof.

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

Дальше: примеры как тесты