Исполняемые спецификации на flang Ментальная модель: данные, правила, вывод и эффект
English
 0%

Ментальная модель: данные, правила, вывод и эффект

7 мин 1440 слов
#flang#модель#детерминизм#архитектура

Ментальная модель: данные, правила, вывод и эффект

Эта глава задаёт словарь на весь курс: как читать файл на flang, не путая четыре разные вещи, которые в обычном коде свалены в один метод. Если это разделение усвоено, дальнейшие главы — подробности тех же четырёх слоёв.

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

модуль «Исполнение заказа»

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

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

Здесь видны все четыре слоя сразу. объект «Заказ» — данные. Функция «Можно отгрузить» — правило. Строка обеспечивает — обещание, которое компилятор доказывает для всех заказов. А то, что заказ реально уехал со склада, произойдёт снаружи, в коде склада, и только если правило сказало «да».

Четвёртый шаг — вывод на настоящих данных. Факты кладутся в JSON, утверждение пишется словами:

$ flang facts shipment.flang --facts order.json --claims '["«Можно отгрузить» от заказ равно да"]'

Для заказа, который оплачен, но не подтверждён складом, ответ такой (поле steps с шагами вычисления опущено):

{
  "ok": false,
  "results": [
    {
      "claim": "«Можно отгрузить» от заказ равно да",
      "holds": false,
      "why": "«Можно отгрузить» от факта «заказ» = нет, а утверждение требует «равно да». Исходные факты — «заказ»: номер = «ЗК-7781», оплачен = да, склад подтвердил = нет",
      "status": "refuted"
    }
  ]
}

Код возврата — 1: утверждение опровергнуто, и ответ называет факты, на которых это получено.

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

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

flang facts вычисляет утверждения на фактах. Звать он позволяет только функции с доказанным завершением, поэтому ответ приходит всегда: вычисление не может зависнуть.

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

Четыре слоя

Данные. объект описывает форму входа: набор именованных полей с типом. Методов, конструкторов и скрытого состояния нет — это не класс. Когда значение бывает разного рода (заказ «создан», «оплачен», «отгружен»), заводится тип с вариантами, и разбирать его обязательно по всем вариантам.

Правила. Правило — тотальная функция: вход → решение. Она не меняет данные и не знает про время, сеть и базу. Её поведение на конкретных входах записано примерами, а на всех входах — обещаниями обеспечивает.

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

Эффект. Списание денег, запись в базу, команда складу происходят вне модели. Компилятор может ответить «отгрузка разрешена» или посчитать скидку, но сам ничего во внешнем мире не делает.

Граница эффекта проведена намеренно. Функция модели не может открыть файл или сокет: в flang действие с миром — это значение-описание (план), которое исполняет запустившая программа. Поэтому один и тот же файл даёт одинаковый результат в песочнице, в Node.js и в CI. Когда именно решение превращается в действие, решает приложение: retry, идемпотентность и очередь сообщений — работа кода, который получил ответ.

Расчёт и допуск — два вида правил

Правило-расчёт возвращает число: скидку, тариф, бонус. Его проверяют примеры и обещания вида «скидка не больше 15 000».

Правило-допуск возвращает признак (да/нет) или тип с вариантами вроде «Разрешено / Отказано с причиной». Его главное обещание — импликация: «если заказ не оплачен, то ответ — нет». Такие обещания компилятор доказывает сам, по условию ветви если, без единой теоремы.

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

Три уровня уверенности

Отчёт flang check --proof называет каждое обещание одним из трёх слов, и они не взаимозаменяемы:

  • «доказано» — верно для всех входов. Код возврата 0;
  • «сетка N» — проверено только на N примерах автора. Это не доказательство. Код возврата 3;
  • «объявлено, не доказано» — нет ни доказательства, ни примеров. Код возврата 3.

Вот функция с ошибкой в теле: неоплаченному заказу она отвечает «да».

модуль «Исполнение заказа»

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

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  пример «оплачен, но склад молчит»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается нет
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе да
$ flang check shipment-wrong.flang
модуль «Исполнение заказа»: функций 1, из них с доказанным завершением 1; типов 1
shipment-wrong.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

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

Это главный урок главы. Без --proof ответ зелёный: обещание не опровергнуто ни одним примером. С --proof видно, что оно не доказано, — код 3. Ложь ещё не поймана, но и за правду не выдана.

Поймать её помогает пример на нужной ветке:

модуль «Исполнение заказа»

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

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  пример «оплачен, но склад молчит»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается нет
  пример «неоплаченный заказ»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7782" и «оплачен» равным нет и «склад подтвердил» равным да
    ожидается да
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе да
$ flang check shipment-wrong.flang
модуль «Исполнение заказа»: функций 1, из них с доказанным завершением 1; типов 1
FLANG_EXAMPLE: пример «неоплаченный заказ» функции «Можно отгрузить»: FLANG_PROPERTY: нарушено свойство «неоплаченный заказ не отгружается» функции «Можно отгрузить»
shipment-wrong.flang: не проверено — замечаний 1

Ни один уровень не делает бизнес-правило истинным «из воздуха». Компилятор доказывает, что код держит обещание. Верно ли само обещание — решают политика, договор или владелец правила.

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

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

Добавьте функции «Рассчитать скидку» пример с суммой ровно 10000 без постоянного клиента. Посчитайте ожидаемое число вручную по функции «Большая покупка» и добейтесь, чтобы все примеры сошлись.

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

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

FLANG_EXAMPLE — пример вычислился не в то значение, которое в нём ожидается. Сообщение называет пример, функцию и оба значения: значение не совпало с ожидаемым: ожидалось true, получено false. Правка — исправить тело или ожидание; решает тот, кто знает правило.

Принять код 3 за успех. flang check без --proof про доказательства не спрашивает и отвечает 0 даже на ложное обещание, если примеры его не задели. В CI нужен flang check --proof, и код 3 в нём — не зелёный.

Принять "holds": false за сбой. Код 1 у flang facts значит «опровергнуто», а не «сломалось». Сбой вызова — код 2. Опровергнутое утверждение — нормальный ответ: например, отказ в отгрузке.

Чек-лист

  • Я могу разложить любое правило своей системы на данные, правило, вывод и эффект — по отдельности.
  • Я отличаю правило-расчёт от правила-допуска и знаю, какие обещания компилятор доказывает сам.
  • Я читаю отчёт --proof и не путаю «доказано», «сетка N» и «объявлено, не доказано».
  • Я объясняю, почему граница эффекта — решение приложения, а не языка.

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

Дальше: инструменты и JSON

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

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

Доска запросов
Дальше