Executable specifications in flang A rule inside Node.js: the model printed to JavaScript and the HTTP boundary
Русский
 0%

A rule inside Node.js: the model printed to JavaScript and the HTTP boundary

11 min 2256 words
#flang#nodejs#http#backend#typescript

A rule inside Node.js: the model printed to JavaScript and the HTTP boundary

The flang model computes the rule. Everything else — the socket, routes, response codes, the request body limit — is ordinary Node.js code. In this chapter the boundary runs through a real file of the course: examples/spec/discount-api/server.mjs. It is an HTTP service on the built-in node:http, with no framework. It starts with the command npm run spec:api.

Minimal example

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

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

тотальная функция «Большая покупка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка за объём не отрицательна» результат не меньше 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
  «Рассчитать скидку» от (запись «Покупка» с «сумма» равным сумма и «постоянный клиент» равным постоянный)

This file lives in static/spec/models/order-discount.flang, and server.mjs reads the same file. There is one model: the sandbox on the site opens it, the HTTP service computes with it, and the service tests check it.

The rules are separate functions: «Большая покупка» (large purchase), «Постоянный клиент» (regular customer), «Очень крупная покупка» (very large purchase). The total is their sum in «Рассчитать скидку». The last function, «Скидка по сумме», takes two scalars instead of a record. It is there for a command-line call, covered in the chapter on clients in other languages.

What the compiler does when the service starts

There is no JavaScript library of the compiler. The model reaches the service another way: flang prints it into an ordinary JavaScript module (flang emit --target js), and the service imports that module. At run time the rule is an ordinary function; the compiler takes no part in requests.

On start server.mjs takes two steps:

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) };
}

The first step is flang test: all examples of the model are run. If even one does not match, the function throws and the port is never opened. A rule that fails its own examples does not reach production.

The second step is importModel from examples/spec/lib/flang.mjs. It prints the model to JavaScript, puts the result into node_modules/.cache/spec-course/ and imports the module. The model’s functions are looked up by their flang names: functions.get('Рассчитать скидку').

The order of the steps matters. flang emit does not run examples itself, and it says so plainly:

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

That is why flang test comes first.

The compiler behind lib/flang.mjs is the binary when FLANG_BIN=<путь к flang> is set. Without it, it is the same compiler in WebAssembly that runs the sandbox. Both give the same answers.

What flang emit prints

The printed module is self-contained: no dependencies, it runs in Node and in the browser. The model’s functions are reachable two ways — by a transliterated name and by the flang name:

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

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

The model’s promises are printed along with it. The promise «скидка ограничена» (discount is capped) is not proved by the compiler — the flang check --proof report lists it as «сетка 5 значений». A grid means the promise was checked only on the five values from the examples; it is not a proof. Such a promise goes into the code as a check:

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;
}

A proved promise does not go into the code: «за очень крупную покупку не больше потолка» is proved by the compiler for every input, and the line «проверок при работе снято 1» refers to exactly that.

The HTTP handler and the contract

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 is not described by hand in the code. It comes from the parsed program — flang ast returns the model’s objects with their fields and types:

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) }));
}

When the model changes, the contract changes with it; there is no second place to edit. Try it locally:

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"
}

The model’s function does not read request and does not write response. It takes a record and returns a number or throws an error. So the rule is checked without a single HTTP call — that is what flang test does.

Why a bad input is a 400 and not a 500

The printed function does not check input types on its own. It will not reject a string in place of a number by type; it fails somewhere inside, on the first comparison:

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

A negative amount for an ordinary customer is silently computed as 0. Checking the input against the declared types is the boundary’s job. In the service that is 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;
}

The check uses the same fields from flang ast as the contract. An extra field is an error too, not a silently ignored value.

A bad input is a request error: the client sent the wrong thing. Answering it with 500 would mean saying “we broke”. So the handler returns 400 with the reason and a code:

} 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

If a model promise is broken on a real input, the printed function throws FLANG_PROPERTY, and the client gets 400 with that code. server.test.mjs checks a bad input explicitly:

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, /«сумма»: ждали неотрицательное целое/);
});

If the boundary is not a Node service but a separate process, input types are checked by the runner flang_cli.js, printed next to the module. The request is one JSON line, and so is the answer:

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

TypeScript instead of JavaScript

If the project is in TypeScript, the print target is different: flang emit --target ts. The course shows it in examples/spec/typescript-codegen: the printed module is kept in the repository, and the command with the --check key compares it with what the model would print anew, and fails if the code was edited by hand bypassing the model. Details are in the chapter on generation and CI.

Mistakes to avoid

  • Do not read the request body without a limit: server.mjs stops reading after 64 KB, before calling JSON.parse.
  • Do not pass the whole request object to the model function. Check the fields against the contract: the printed function will not do it.
  • Do not make a payment or a charge directly from the answer of calculate. First get the rule’s result, then perform the effect as a separate call that can be retried or rolled back.
  • Do not keep a second, hand-written implementation of the rule in TypeScript “just in case”. Without a test that compares it with the model, the two drift apart quietly.
  • Do not print the model without running its examples: flang emit does not run them.

Practice in the sandbox

  1. In the sandbox, read the proof report. Find the promise that is proved and the three that rest only on examples.
  2. Run npm run spec:api locally and curl -s localhost:8788/discount -d '{"сумма":"много","постоянный клиент":true}'. Check the response code and the code field.
  3. Add the field «вес»: неотрицательное to the «Покупка» record, adjust the examples and restart the service. See how the GET /contract answer changed — with no edit to the server code.

Common errors

  • INPUT — the input does not fit the contract: wrong type, an extra or a missing field. This is the code of the service boundary itself, not of the compiler. It is returned as 400.
  • FLANG_PROPERTY — a model promise is broken on a real input. The check was put there by flang emit, because the promise is not proved. Also 400.
  • The service does not start — flang test found an example that does not match. createCalculator throws with the flang test output, and npm run spec:api exits without opening the port.

Checklist

  • The model’s examples run once at process start, before the port opens.
  • The model is printed to JavaScript at start or at build time; the compiler takes no part in requests.
  • The HTTP handler holds no business conditions — only routes, body parsing and response codes.
  • The input contract is built from flang ast, not duplicated by hand.
  • The input is checked against field types before the model function is called.
  • Bad inputs and broken promises are returned as 4xx, not as 500.
  • There is a request body size limit before JSON.parse.

Catalog cases on this topic

Next: React

Spotted a mistake? Select a fragment of the text — a bug icon will appear next to it.

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

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

Доска запросов
Next