Спеки: бизнес-правило, которое доказано

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

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

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

Как выглядит правило

Вот функция из службы корзины — целиком, как она лежит в дереве (examples/web/marketplace/cart.flang):

тотальная функция «Скидка в процентах»
  принимает сумма: число
  возвращает число
  для всех сумма обеспечивает «скидка бывает только нулевая, пятипроцентная или десятипроцентная» ((результат равен 0) или (результат равен 5)) или (результат равен 10)
  пример «мелкая покупка без скидки»
    дано сумма равно 100000
    ожидается 0
  пример «от пяти тысяч — пять процентов»
    дано сумма равно 500000
    ожидается 5
  пример «от двадцати тысяч — десять процентов»
    дано сумма равно 2000000
    ожидается 10
  если сумма не меньше 2000000
    то 10
    иначе (если сумма не меньше 500000 то 5 иначе 0)

Четыре части, и каждая делает работу:

Имя утверждения — опознавательный знак. По паре «функция плюс имя» правила и сверяются между собой: переименовали утверждение — связь порвалась, и проверка об этом скажет.

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

Сквозной пример: API маркетплейса

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

examples/web/marketplace/
  catalog.flang   136   товары, цена, остаток, «сколько выдать»
  cart.flang      130   позиции, счёт, скидка ступенями
  orders.flang    245   состояния заказа и переходы между ними
  gateway.flang   482   коды ответа, маршруты, байты пришли — байты ушли
                  ─────
                  993   строки, и все на flang

Что отвечает шлюз:

Отказы названы: 400 негодный запрос, 404 нет пути, товара или заказа, 405 метод не тот для известного пути (а не 404 — служба не врёт о причине), 409 на складе меньше, чем просят, 413 тело длиннее предела, 422 переход по состояниям запрещён.

Где проходит граница языка

Вход шлюза — тот самый текст, который хозяин прочитал из соединения; выход — тот самый текст, который хозяин пошлёт обратно:

тотальная функция «Обслужить»
  принимает витрина: «Витрина», текст: строка
  возвращает «Обслуживание»

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

Граница проведена не из бедности языка, а по расчёту: на flang пишется то, что решить, а не то, как дождаться байтов из сети. Зато всё, что написано, — проверяется примером, без единого поднятого сервера.

Что это не заготовка, видно рядом: в examples/web/shortener/ та же граница доведена до конца — служба на 1 150 строк, которую хозяин водит по настоящему сокету, и curl получает от неё 200, 201, 301 и 204.

Спека не написана, а проверена

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

Вот что отвечает проверка по службе заказов:

flang check examples/web/marketplace/orders.flang --proof

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

итог:
  функций 7: тотальных 7, обычных 0
  утверждений 3: доказано 2 (из них индукцией 2), сетка 1, объявлено, не доказано 0 (шагов в термах 12)

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

Разница видна и в том, откуда она берётся. Состояния заказа объявлены суммой:

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

Состояние строкой ("paid", "shipped") такой возможности не даёт вовсе: множество строк бесконечно, и разбор случаев по нему не исчерпывающий.

Что доказано во всём примере

Четыре файла примера проверяются одной и той же программой, и каждый отвечает своей строкой итога:

$ flang check examples/web/marketplace/catalog.flang --proof
  функций 8: тотальных 8, обычных 0
  утверждений 1: доказано 1 (из них без теоремы 1), сетка 0, объявлено, не доказано 0

$ flang check examples/web/marketplace/cart.flang --proof
  функций 16: тотальных 16, обычных 0
  утверждений 6: доказано 3 (из них без теоремы 3), сетка 3, объявлено, не доказано 0

$ flang check examples/web/marketplace/orders.flang --proof
  функций 7: тотальных 7, обычных 0
  утверждений 3: доказано 2 (из них индукцией 2), сетка 1, объявлено, не доказано 0 (шагов в термах 12)

$ flang check examples/web/marketplace/gateway.flang --proof
  функций 106: тотальных 106, обычных 0
  утверждений 146: доказано 70 (из них индукцией 10) (из них без теоремы 58, объявленным типом 2), сетка 76, объявлено, не доказано 0 (шагов в термах 32)

Числа шлюза выделяются, и причина простая: gateway.flang тянет за собой библиотеку разбора HTTP, а отчёт считает всё, что проверено вместе с ним, — 106 функций против восьми у каталога. Своих утверждений у шлюза два, и оба доказаны индукцией по объявленной сумме исходов:

  постусловие «код ответа из объявленного набора» функции «Код исхода» — доказано индукцией по «Исход»: база 9 случаев, шаг при допущении на частях (0 случаев) — утверждение обо ВСЕХ входах типа «Исход», а не о написанных
  постусловие «пояснение кода непусто» функции «Код исхода» — доказано индукцией по «Исход»: база 9 случаев, шаг при допущении на частях (0 случаев) — утверждение обо ВСЕХ входах типа «Исход», а не о написанных

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

Почему именно эти четыре — компилятор говорит сам, если написать при них теорему. Он отвечает, что заключение случая читает из двух форм тела и ниоткуда больше: с ветви разбор по той же переменной и с начала и шага свёртка по той же переменной. У всех четырёх тело сворачивает не саму переменную, а вычисленный из неё список («Переходы из» от откуда, корзина.«позиции»), — цеплять доказательство не к чему. Развернуть их в разбор по переменной можно, но для службы заказов это значит завести вторую копию таблицы переходов, а разъезд двух копий — ровно та беда, от которой этот пример предостерегает. Цена доказательства выше цены честной пометки, и пометка оставлена.

Что мешает соврать

Спека, которую нельзя подделать, — не обещание, а свойство, и проверяется оно прогоном. Испортим одну строку в таблице кодов шлюза — пусть «Товара не хватает» отвечает не 409, а 500:

flang check examples/web/marketplace/gateway.flang --proof

место указано строкой и столбцом, но без файла: вместе с импортами проверено файлов 7, а диагностика компилятора имени файла не несёт
FLANG_PROOF_STEP, строка 129, столбец 10: шаг 1, база «Товара не хватает» теоремы «код ответа из объявленного набора»: пример «товара не хватает — четыреста девять» не проходит: нарушено свойство «код ответа из объявленного набора» функции «Код исхода». Утверждение на этом значении неверно, значит случай им не закрывается. к этому месту не известно ничего, кроме гипотез «дано»
место указано строкой и столбцом, но без файла: вместе с импортами проверено файлов 7, а диагностика компилятора имени файла не несёт
FLANG_PROOF_STEP, строка 156, столбец 10: шаг 1, база «Товара не хватает» теоремы «пояснение кода непусто»: пример «товара не хватает — четыреста девять» не проходит: нарушено свойство «код ответа из объявленного набора» функции «Код исхода». Утверждение на этом значении неверно, значит случай им не закрывается. к этому месту не известно ничего, кроме гипотез «дано»
examples/web/marketplace/gateway.flang: не проверено — ведомость не печатается у программы с замечаниями

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

Так же ловится и порча примера. Поменяем в каталоге ожидаемое значение — пусть из остатка 5 при запросе 2 выдаётся 3:

flang check examples/web/marketplace/catalog.flang --proof

FLANG_EXAMPLE: пример «остатка хватает» функции «Сколько выдать»: значение не совпало с ожидаемым: ожидалось 3, получено 2
examples/web/marketplace/catalog.flang: не проверено — ведомость не печатается у программы с замечаниями

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

Фронтенд на React снаружи, а контракт проверяем

Браузерный код обычный. На flang его никто не пишет и писать не собирается:

// Обычный React, ни строки на flang.
function Cart() {
  const [bill, setBill] = useState("");
  const [error, setError] = useState("");

  async function add(sku, qty) {
    const res = await fetch("/корзина", {
      method: "POST",
      headers: { "Content-Type": "application/x-www-form-urlencoded" },
      body: `артикул=${sku}&количество=${qty}`,
    });
    const text = await res.text();
    switch (res.status) {
      case 201: setBill(text); setError(""); break;      // положено, счёт пересчитан
      case 400: setError("количество не число"); break;
      case 404: setError("нет товара с таким артикулом"); break;
      case 409: setError("на складе меньше, чем просят"); break;
      case 413: setError("тело запроса длиннее предела"); break;
    }
  }
  // …
}

Интересно здесь не то, что React зовёт службу, а то, что список случаев в switch не соглашение, а следствие. Набор кодов объявлен в службе типом:

тип «Исход»
  вариант «Готово»
  вариант «Создано»
  вариант «Очищено»
  вариант «Запрос негоден»
  вариант «Нет такого»
  вариант «Метод не тот»
  вариант «Товара не хватает»
  вариант «Тело велико»
  вариант «Переход запрещён»

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

Спецификация здесь — не документ рядом с кодом, а сам код: перечень исходов, таблица кодов и теорема, связавшая их. Фронтенд её не проверяет и не обязан — она проверена там, где написана.

Правило, которое приходит вторым

Тест отвечает про те входы, которые в нём записаны. Доказанное обещание отвечает про все. Разница видна на первом же требовании, которое приходит вторым.

В каталоге fspec/spec/ первая спека записывает правило «скидка не больше 30». Через месяц приходит «промо-заказу скидка больше», кто-то пишет вторую функцию и вторую спеку. Вопрос не в том, работает ли новая, — вопрос, осталось ли верным первое правило. Тестами на это отвечают чтением кода двумя людьми. Здесь — одной командой:

./ярлык спеки:проверка

спеки согласны: спек 42, утверждений 295, и каждое доказано из нуля аксиом

«Из нуля аксиом» значит, что ничего не принято на веру: под каждым утверждением цепочка, доходящая до правил самого языка.

Первые две спеки каталога показывают именно СВЯЗЬ двух правил, а не сильное утверждение: у них верхняя граница, а такая граница подмену тела на ноль переживает. За сильными утверждениями надо смотреть спеки 3–27 и пример маркетплейса выше.

Рядом со спеками лежит подлог: набор случаев, где спека нарочно испорчена, и проверка обязана покраснеть на каждом.

./ярлык спеки:подлог

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

Правило на другом языке — то же самое правило

Обещание можно записать на языке той команды, которая им пользуется:

обеспечивает «zh: 折扣不超过 30» результат не больше 30

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

Названная цена: двоеточие в имени обещания теперь значит метку языка. И названный предел: сам перевод проверка прочитать не может — если китайский вид назван неверно при верной цели, она промолчит.

Что почитать дальше

• Разбор: задачи с leetcode — пять решений целиком и то, что о них доказано.
• Что вообще доказано — числа по дереву, а не обещания.
• Отказы доказательства — почему ядро отказывает и что с этим делать.
• Уточняющие вопросы — как из недоказанного обещания получается вопрос к автору требования.
• examples/web/marketplace/README.md в дереве — тот же пример подробнее, вместе с устройством файлов.
• fspec/README.md — устройство каталога спек.