Исполняемые спецификации на flang Правило в Node.js: модель, напечатанная в JavaScript, и граница HTTP
English
 0%

Правило в Node.js: модель, напечатанная в JavaScript, и граница HTTP

10 мин 1966 слов
#flang#nodejs#http#backend#typescript

Правило в Node.js: модель, напечатанная в JavaScript, и граница HTTP

Модель на flang считает правило. Всё остальное — сокет, маршруты, коды ответа, лимит тела запроса — обычный код Node.js. В этой главе граница проходит по реальному файлу курса: examples/spec/discount-api/server.mjs. Это HTTP-сервис на встроенном node:http без фреймворка. Запускается он командой npm run spec:api.

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

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

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

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

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

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

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка ограничена» результат не больше 15000
  пример «обычная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 5000 и «постоянный клиент» равным нет
    ожидается 0
  пример «постоянный клиент на пять тысяч»
    дано покупка равно запись «Покупка» с «сумма» равным 5000 и «постоянный клиент» равным да
    ожидается 250
  пример «большая покупка постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным да
    ожидается 3000
  пример «покупка на потолок скидки»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 15000
  пример «очень крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 200000 и «постоянный клиент» равным нет
    ожидается 15000
  («Большая покупка» от покупка) плюс («Постоянный клиент» от покупка) плюс («Очень крупная покупка» от покупка)

тотальная функция «Скидка по сумме»
  принимает сумма: неотрицательное, постоянный: признак
  возвращает число
  пример «тот же расчёт без записи на входе»
    дано сумма равно 20000
    дано постоянный равно да
    ожидается 3000
  «Рассчитать скидку» от (запись «Покупка» с «сумма» равным сумма и «постоянный клиент» равным постоянный)

Этот файл лежит в static/spec/models/order-discount.flang, и его же читает server.mjs. Модель одна: её открывает песочница на сайте, считает HTTP-сервис и проверяют его тесты.

Правила — отдельные функции: «Большая покупка», «Постоянный клиент», «Очень крупная покупка». Итог — их сумма в «Рассчитать скидку». Последняя функция, «Скидка по сумме», принимает два скаляра вместо записи. Она нужна вызову из командной строки, о нём — в главе про клиенты на других языках.

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

JS-библиотеки компилятора нет. Модель в сервис попадает другим путём: flang печатает её в обычный модуль JavaScript (flang emit --target js), и сервис этот модуль подключает. Правило в рантайме — обычная функция, компилятор при запросах не участвует.

На старте server.mjs делает два шага:

export async function createCalculator(modelFile = MODEL_FILE) {
  const compiler = await flang();
  const tests = await compiler.test(modelFile);
  if (tests.code !== 0) throw new Error(`примеры модели не прошли:\n${tests.output}`);
  const passed = /примеров (\d+), прошло (\d+)/u.exec(tests.output);
  const { functions } = await importModel(modelFile);
  return { examples: passed ? `${passed[2]}/${passed[1]}` : '?', calculate: functions.get(FUNCTION) };
}

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

Второй шаг — importModel из examples/spec/lib/flang.mjs. Он печатает модель в JavaScript, кладёт результат в node_modules/.cache/spec-course/ и подключает модуль. Функции модели достаются по их именам во flang: functions.get('Рассчитать скидку').

Порядок шагов не случаен. flang emit сам примеры не гоняет, он об этом прямо пишет:

$ flang emit static/spec/models/order-discount.flang --target js --out js
проверок при работе снято 1: постусловие доказано ядром обо всех входах и
проверено примерами функции — в напечатанный код оно не едет.
напечатано файлов 3, байт 52564, в js
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>

Поэтому flang test идёт первым.

Компилятор lib/flang.mjs берёт двоичный, если задан FLANG_BIN=<путь к flang>. Без него — тот же компилятор в WebAssembly, на котором работает песочница. Ответы у них одинаковые.

Что печатает flang emit

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

import { $PROGRAM } from './js/prodazhi.js';

const calculate = $PROGRAM.functions.get('Рассчитать скидку');
console.log(calculate({ 'сумма': 20000, 'постоянный клиент': true }));
// 3000

Обещания модели печатаются вместе с ней. Обещание «скидка ограничена» компилятор не доказал — в отчёте flang check --proof оно стоит как «сетка 5 значений». Сетка значит: обещание проверено только на пяти значениях из примеров, это не доказательство. Такое обещание уезжает в код проверкой:

export function rasschitatSkidku(pokupka) {
  const $t1 = $add(
    $add(bolshayaPokupka(pokupka), postoyannyyKlient(pokupka)),
    ochenKrupnayaPokupka(pokupka),
  );
  // постусловие «скидка ограничена»
  if (!$post($lte($t1, 15000), "скидка ограничена", "Рассчитать скидку")) {
    $fail(
      "FLANG_PROPERTY",
      "нарушено свойство «скидка ограничена» функции «Рассчитать скидку»",
      { line: 46, column: 3 },
    );
  }
  return $t1;
}

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

HTTP-обработчик и контракт

if (request.method === 'GET' && request.url === '/contract') {
  return send(response, 200, { function: FUNCTION, input: fields, output: 'number' });
}
if (request.method !== 'POST' || request.url !== '/discount') {
  return send(response, 404, { error: 'используйте POST /discount' });
}
const purchase = readPurchase(await readBody(request), fields);
return send(response, 200, { discount: calculate(purchase) });

fields не описан в коде руками. Он берётся из разобранной программы — flang ast отдаёт объекты модели с полями и типами:

export async function contractOf(modelFile = MODEL_FILE) {
  const ast = await (await flang()).ast(modelFile);
  const purchase = ast.types.find((type) => type.name === 'Покупка');
  return purchase.fields.map((field) => ({ name: field.name, type: typeWord(field.type) }));
}

Поменялась модель — поменялся и контракт, второго места для правки нет. Проверить локально:

npm run spec:api
curl -s localhost:8788/discount -d '{"сумма":20000,"постоянный клиент":true}'
curl -s localhost:8788/contract
curl -s localhost:8788/health

{
  "discount": 3000
}
{
  "function": "Рассчитать скидку",
  "input": [
    {
      "name": "сумма",
      "type": "неотрицательное"
    },
    {
      "name": "постоянный клиент",
      "type": "признак"
    }
  ],
  "output": "number"
}
{
  "ok": true,
  "model": "Продажи",
  "examples": "10/10"
}

Функция модели не читает request и не пишет response. Она принимает запись и возвращает число или бросает ошибку. Поэтому правило проверяется без единого HTTP-вызова — это делает flang test.

Почему ошибка входа — это 400, а не 500

Напечатанная функция сама типы входа не сверяет. Строку вместо числа она не отвергнет по типу, а упадёт где-то внутри, на первом сравнении:

FLANG_TYPE сравнения порядка допустимы только для чисел

Отрицательную сумму у обычного клиента она молча посчитает как 0. Сверять вход с объявленными типами — работа границы. В сервисе это readPurchase:

export function readPurchase(body, fields) {
  const purchase = JSON.parse(body);
  const problems = [];
  for (const field of fields) {
    const value = purchase?.[field.name];
    if (field.type === 'признак' && typeof value !== 'boolean') problems.push(`«${field.name}»: ждали да или нет`);
    if (field.type === 'неотрицательное' && !(Number.isInteger(value) && value >= 0)) problems.push(`«${field.name}»: ждали неотрицательное целое`);
  }
  for (const name of Object.keys(purchase ?? {})) {
    if (!fields.some((field) => field.name === name)) problems.push(`«${name}»: такого поля у «Покупки» нет`);
  }
  if (problems.length) {
    const error = new Error(`вход не подходит к «Покупке»: ${problems.join('; ')}`);
    error.code = 'INPUT';
    throw error;
  }
  return purchase;
}

Проверка идёт по тем же полям из flang ast, что и контракт. Лишнее поле — тоже ошибка, а не молча проигнорированное значение.

Ошибка входа — ошибка запроса: клиент прислал не то. Отвечать на неё 500 значило бы сказать «мы сломались». Поэтому обработчик возвращает 400 с причиной и кодом:

} catch (error) {
  return send(response, 400, {
    error: error instanceof Error ? error.message : String(error),
    code: error?.code ?? 'INPUT',
  });
}

$ curl -s -w '%{http_code}\n' localhost:8788/discount -d '{"сумма":"много","постоянный клиент":true}'
{
  "error": "вход не подходит к «Покупке»: «сумма»: ждали неотрицательное целое",
  "code": "INPUT"
}
400

Если на настоящем входе нарушится обещание модели, напечатанная функция бросит FLANG_PROPERTY, и клиент получит 400 с этим кодом. server.test.mjs проверяет неверный вход явно:

test('неверный тип входа — 400 с причиной, а не 500', async () => {
  const response = await fetch(`${origin}/discount`, { method: 'POST', body: JSON.stringify({ 'сумма': 'много', 'постоянный клиент': true }) });
  assert.equal(response.status, 400);
  const body = await response.json();
  assert.equal(body.code, 'INPUT');
  assert.match(body.error, /«сумма»: ждали неотрицательное целое/);
});

Если граница — не сервис на Node, а отдельный процесс, типы сверяет прогонщик flang_cli.js, который печатается рядом с модулем. Запрос — строка JSON, ответ — тоже:

$ echo '{"fn":"Рассчитать скидку","args":[{"r":[["сумма",{"s":"много"}],["постоянный клиент",true]]}]}' | node flang_cli.js ./prodazhi.js
{"ok":false,"code":"FLANG_TYPE","message":"вызов функции «Рассчитать скидку»: аргумент «покупка».сумма не соответствует типу неотрицательное"}

TypeScript вместо JavaScript

Если проект на TypeScript, цель печати другая: flang emit --target ts. Курс показывает это в examples/spec/typescript-codegen: напечатанный модуль лежит в репозитории, а команда с ключом --check сравнивает его с тем, что напечатала бы модель заново, и падает, если код поправили руками мимо модели. Подробности — в главе про генерацию и CI.

Ошибки, которых следует избежать

  • Не читайте тело запроса без лимита: server.mjs останавливает чтение после 64 КБ до вызова JSON.parse.
  • Не передавайте в функцию модели объект запроса целиком. Сверьте поля с контрактом: напечатанная функция этого не сделает.
  • Не выполняйте платёж или списание прямо по ответу calculate. Сначала получите результат правила, затем выполните эффект отдельным вызовом, который можно повторить или откатить.
  • Не держите вторую, ручную реализацию правила на TypeScript «на всякий случай». Без теста, который сверяет её с моделью, они разойдутся тихо.
  • Не печатайте модель, не прогнав её примеры: flang emit их не считает.

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

  1. В песочнице прочитайте отчёт о доказательствах. Найдите обещание, которое доказано, и три, которые держатся только на примерах.
  2. Запустите локально npm run spec:api и curl -s localhost:8788/discount -d '{"сумма":"много","постоянный клиент":true}'. Проверьте код ответа и поле code.
  3. Добавьте в запись «Покупка» поле «вес»: неотрицательное, поправьте примеры и перезапустите сервис. Посмотрите, как поменялся ответ GET /contract — без правки серверного кода.

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

  • INPUT — вход не подходит к контракту: не тот тип, лишнее или отсутствующее поле. Это код самой границы сервиса, а не компилятора. Возвращается как 400.
  • FLANG_PROPERTY — обещание модели нарушено на настоящем входе. Проверку поставил flang emit, потому что обещание не доказано. Тоже 400.
  • Сервис не стартует — flang test нашёл несошедшийся пример. createCalculator бросает исключение с выводом flang test, и npm run spec:api завершается, не открыв порт.

Чек-лист

  • Примеры модели прогоняются один раз при старте процесса, до открытия порта.
  • Модель печатается в JavaScript при старте или при сборке; при запросах компилятор не участвует.
  • Обработчик HTTP не содержит бизнес-условий — только маршруты, разбор тела и коды ответа.
  • Контракт входа строится из flang ast, а не дублируется вручную.
  • Вход сверяется с типами полей до вызова функции модели.
  • Ошибки входа и нарушенные обещания возвращаются как 4xx, а не как 500.
  • Есть лимит на размер тела запроса до JSON.parse.

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

Дальше: React

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

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

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

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