Executable specifications in flang You don't need lodash — but not where you think
0%

You don't need lodash — but not where you think

You don’t need lodash — but not where you think

“Let’s rewrite lodash in flang” is a proposal that sounds reasonable. flang has lists and functions over them: отобразить instead of map, отфильтровать instead of filter, свёртка instead of reduce, taking a list apart into пусто and голова и хвост, records and types with variants. Technically, most of lodash can be expressed. The question is not whether it can be done, but what of it is worth moving.

Open the list of real lodash calls in your project and split it into two groups. The first group will hold clamp, inRange, round in a price calculation, defaultTo, sumBy with a condition, maxBy by a threshold, chains of get with a fallback value. This is not data handling — these are business rules written as function arguments. The second group will hold everything else, and it will stay in JavaScript. The thesis of the chapter: lodash leaves the project not because flang appeared, but because half of its calls were logic without a model, and the other half has long been in the language’s standard library. flang takes the first half — and it is worth taking, because that half has to be checkable.

Minimal example

Writing off bonuses when an order is paid. In application code this is usually one line: clamp(defaultTo(customer.bonus, 0), 0, round(order.amount * 0.3, 2)).

модуль «Ценообразование»

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

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

тотальная функция «Списать бонусы»
  принимает списание: «Списание бонусов»
  возвращает число
  обеспечивает «списание не превышает потолка» результат не больше 30000
  обеспечивает «мелкий заказ бонусами не оплачивается» если списание.«сумма заказа» меньше 500 то результат равен 0 иначе да
  пример «баланс ниже предела»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 2000 и «баланс бонусов» равным 300
    ожидается 300
  пример «баланс ровно на пределе»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 2000 и «баланс бонусов» равным 600
    ожидается 600
  пример «баланс выше предела»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 2000 и «баланс бонусов» равным 1000
    ожидается 600
  пример «мелкий заказ»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 400 и «баланс бонусов» равным 1000
    ожидается 0
  пример «отрицательный баланс не списывается»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 2000 и «баланс бонусов» равным -50
    ожидается 0
  пример «заказ ровно на потолке списания»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 100000 и «баланс бонусов» равным 50000
    ожидается 30000
  пример «крупный заказ упирается в потолок»
    дано списание равно запись «Списание бонусов» с «сумма заказа» равным 200000 и «баланс бонусов» равным 100000
    ожидается 30000
  пусть предел равно «Предел списания» от списание.«сумма заказа»
  если списание.«сумма заказа» меньше 500
    то 0
    иначе если списание.«баланс бонусов» не больше 0
      то 0
      иначе если списание.«баланс бонусов» больше предел
        то предел
        иначе списание.«баланс бонусов»

The lodash line unfolded into two functions, three promises and eight examples. This is not verbosity: clamp did not answer what to do with a negative balance, and defaultTo did not answer where the decision to substitute zero came from. Now both answers are written down and checked: a negative balance is the branch не больше 0, and a missing balance cannot happen at all — the «баланс бонусов» field is required.

Both bounds of clamp became branches of the body, and the limit became a separate named function. The promises answer what is guaranteed: a cap of 30,000, zero for a small order, and that a large order hits exactly the cap.

What the compiler does

  1. The branches of если … иначе если are tried top to bottom, and the first true one wins. The order of branches is part of the rule: a small order is cut off before the limit is computed.
  2. The promise «крупный заказ упирается в потолок» (a large order hits the cap) is proved for all inputs: the condition of the promise matches the condition of a branch, and the kernel reduces the goal with the rule “split the goal by the condition”. The same goes for «мелкий заказ бонусами не оплачивается» (a small order is not paid with bonuses).
  3. The promise «списание не превышает потолка» (the write-off does not exceed the cap) is not proved, and the report says so directly: “grid 7 values (the function’s examples) … This is not a proof”. The kernel does not derive that thirty percent of an amount is at most 30,000 when the amount is at most 100,000: it does not prove arithmetic with percentages. That is why flang check --proof exits with code 3, and the printed code checks this promise on every call.
  4. A violated promise stops the call with FLANG_PROPERTY; the value does not leave and is not adjusted.
  5. Examples run on every check, and in the service the computation is done by the function printed by flang emit from the same file. The chapter, the sandbox and the application code cannot diverge.
  постусловие «крупный заказ упирается в потолок» функции «Предел списания» — доказано сведением цели с телом функции: правило «разбор цели по условию», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
  постусловие «списание не превышает потолка» функции «Списать бонусы» — сетка 7 значений (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет
  постусловие «мелкий заказ бонусами не оплачивается» функции «Списать бонусы» — доказано сведением цели с телом функции: правило «разбор цели по условию», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
static/spec/models/pricing-rules.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 3: доказано 2, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

What moves into the model and what stays in JavaScript

lodash call What it really is Where it goes
clamp(x, lo, hi) over an input field the lower and upper bounds of a rule если branches in the model + a promise with an absolute cap
inRange(x, a, b) a range condition a branch condition joined with и притом
round/ceil/floor in a price calculation a rule threshold + a money representation the threshold goes to the model, rounding to the application
defaultTo(v, d) the decision “what replaces absence” a required object field + normalization at the boundary
sumBy(items, fn) with a condition inside fn the condition is a rule, the summing is iteration the condition to the model, the summing wherever is handier: свёртка or reduce
maxBy(items, fn) by a threshold the threshold is a rule, finding the maximum is iteration the threshold to the model, iteration to the model or to JS
get(o, 'a.b', d) a missing data contract a model object + one normalization function
map, filter over a rule the rule is applied to each item отобразить, отфильтровать in the model, if a promise concerns the whole list
groupBy, chunk, zip data handling stay in JS
debounce, throttle time management stay in JS
cloneDeep, merge, isEqual structure handling stay in JS (structuredClone, Object.assign)

The top of the table is what becomes readable and checkable in the model. The bottom is what would get worse in the model, even though the language can do it. The middle is iteration: it is worth moving only when a promise about the list moves with it, for example «у каждой позиции своя скидка» (every item has its own discount).

get(order, 'customer.tier', 'basic') — not a rule but a symptom

This chain shows up in any mature frontend, and it hides three different statements, none of which is written down.

The first: “the customer field may be missing”. The second: “if it is missing, the customer counts as basic”. The third, and the most expensive: “the difference between a missing profile and a basic-tier profile does not matter for the calculation”. The first is about the data format, the second is a business decision, the third is a hypothesis nobody tested. get records all three as one default argument, in fourteen places of the code, each of which can be changed independently.

The model does not settle this question — it makes it mandatory. The «уровень клиента» (customer tier) field in examples/spec/lodash/pricing.flang has a type with three variants: «Базовый», «Серебро», «Золото». The string “платина” cannot be passed into the model, let alone a missing tier. The decision “what replaces absence” has to move to the boundary and get a name:

export function normalizeTier(cart) {
  const raw = cart?.customer?.tier;
  if (typeof raw === 'string' && TIERS.has(raw)) return { tier: raw, assumed: false };
  return { tier: 'базовый', assumed: true };
}

The function returns not only the tier but also the assumed flag. It is a cheap line, but it turns a silent assumption into a measurable one: now you can count how many carts were priced with a guessed tier. While the decision lived as the third argument of get, there was nobody to ask that question.

If the absence of a field is a legitimate state rather than a hole in the data, flang has иногда является for it: the field becomes optional, and this is visible in the model. Even then the model will not substitute a default.

Rounding: there is a rule, there is no round

For ordinary numbers (число) flang has no rounding. The built-in form целая часть exists, but only for exact fractions, not for floating-point numbers. An attempt to round a number with it (file round.flang) fails the check:

модуль «Копейки»

тотальная функция «До копеек»
  принимает рубли: число
  возвращает число
  пример «одиннадцать и двадцать пять тысячных»
    дано рубли равно 11.025
    ожидается 11.03
  (целая часть ((рубли умножить на 100) плюс 0.5)) делить на 100
FLANG_BUILTIN_ARGS в файле round.flang, строка 9, столбец 41: аргумент 1 формы «целая часть»: ожидался точное дробное, получен число

Hence an honest conclusion rather than a workaround. The model computes the exact value: 7 percent of 157.50 is 11.025 and no other number. The application brings it to kopecks — exactly once, at the boundary, with the same round it used before. The rule “how many percent” moves into the model; the rule “at which moment money becomes kopecks” stays in the code, because it is a property of the representation, not of the tariff.

In flang, money as a whole number of kopecks is written with the type сотых, and the sum of two such values does not lose a kopeck. But a percentage of an amount still produces a fraction, and deciding which way to round it still belongs to someone who knows the currency, the direction (in whose favour) and the place in the calculation chain. The model does not know this and should not.

Walkthrough: before.mjs → pricing.flang → after.mjs

The set lives in examples/spec/lodash/. It computes the discount on a cart item: a percentage for the customer tier, a bulk bonus from ten pieces, a promo code and an upper limit of 13 percent.

before.mjs is lodash style (the library itself is not included, five of its functions are reproduced locally, round word for word, exponent shift included):

let discount = 0;
if (percent > 0) discount += round((base * percent) / 100, 2);
if (quantity >= 10) discount += round((base * 5) / 100, 2);
if (line.promo === 'ЛЕТО') discount += round((base * 2) / 100, 2);
discount = round(clamp(discount, 0, round((base * MAX_DISCOUNT_PERCENT) / 100, 2)), 2);

pricing.flang — the same decisions as functions, the limit as a promise:

модуль «Ценообразование корзины»

тип «Уровень клиента»
  вариант «Базовый»
  вариант «Серебро»
  вариант «Золото»

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

тотальная функция «Процент уровня»
  принимает уровень: «Уровень клиента»
  возвращает неотрицательное
  обеспечивает «процент уровня не больше семи» результат не больше 7
  пример «серебро — четыре процента»
    дано уровень равно вариант «Серебро»
    ожидается 4
  разбор уровень
    случай «Базовый»
      то 0
    случай «Серебро»
      то 4
    случай «Золото»
      то 7

тотальная функция «Процент скидки»
  принимает позиция: «Позиция корзины»
  возвращает число
  пример «золото на границе опта»
    дано позиция равно запись «Позиция корзины» с «стоимость» равным 1000 и «количество» равным 10 и «уровень клиента» равным (вариант «Золото») и «промокод» равным ""
    ожидается 12
  пусть опт равно (если позиция.«количество» не меньше 10 то 5 иначе 0)
  пусть промо равно (если позиция.«промокод» равен "ЛЕТО" то 2 иначе 0)
  («Процент уровня» от позиция.«уровень клиента») плюс опт плюс промо

тотальная функция «Скидка на позицию»
  принимает позиция: «Позиция корзины»
  возвращает число
  обеспечивает «скидка не превышает 13 процентов» результат не больше ((позиция.«стоимость» умножить на 13) делить на 100)
  пример «базовый уровень, розничная позиция»
    дано позиция равно запись «Позиция корзины» с «стоимость» равным 1000 и «количество» равным 1 и «уровень клиента» равным (вариант «Базовый») и «промокод» равным ""
    ожидается 0
  пример «серебро без опта»
    дано позиция равно запись «Позиция корзины» с «стоимость» равным 1000 и «количество» равным 1 и «уровень клиента» равным (вариант «Серебро») и «промокод» равным ""
    ожидается 40
  пример «опт без уровня»
    дано позиция равно запись «Позиция корзины» с «стоимость» равным 1000 и «количество» равным 10 и «уровень клиента» равным (вариант «Базовый») и «промокод» равным ""
    ожидается 50
  пример «серебро, опт и промокод»
    дано позиция равно запись «Позиция корзины» с «стоимость» равным 1000 и «количество» равным 10 и «уровень клиента» равным (вариант «Серебро») и «промокод» равным "ЛЕТО"
    ожидается 110
  (позиция.«стоимость» умножить на («Процент скидки» от позиция)) делить на 100

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

Here the cap is deliberately written as a percentage of a field: the whole point of the walkthrough is that the old clamp cut the result by the same formula, and the implementations must be compared by it. The kernel does not prove this promise (grid of 4 values), while it proves the promise about the tier percentage by induction over the three variants of the type. The last function shows that the cart can be iterated in the model too: the promise «у каждой позиции своя скидка» is proved for any list.

after.mjs — the model is printed into JavaScript once; after that the rule is an ordinary function, and iterating over items is an ordinary map:

const printed = await importModel(MODEL_FILE);
const discountFor = printed.functions.get('Скидка на позицию');
const variant = printed.module.$PROGRAM.variant;

export function lineDiscount({ base, quantity, tier, promo }) {
  const exact = discountFor({
    стоимость: base,
    количество: quantity,
    'уровень клиента': variant(TIERS.get(tier)),
    промокод: promo,
  });
  return round(exact, 2);
}

importModel from examples/spec/lib/flang.mjs calls flang emit --target js and loads the printed module; its functions are looked up by their names from the model.

equivalence.test.mjs runs both implementations on a deterministic grid of 350 inputs — seven prices with kopecks, five quantities around the threshold, five tier values (including a missing profile and an unknown “platinum”) and two promo codes:

входов: 350; совпало: 318; расхождений: 32 (Потолок вместо отказа — 14; Двойное округление процентов — 18)
позиций в корзине: 65; итог: 815563.4; скидка: 76715.39
✔ модель проходит проверку, и её собственные примеры сходятся
✔ lodash-версия и модель совпадают на всей сетке, кроме объявленных расхождений
✔ каждое объявленное расхождение подтверждается сеткой и объяснено
✔ перебор корзины в JavaScript: многопозиционная корзина считается одинаково
✔ модель отказывается считать без поля, а не подставляет умолчание
ℹ tests 5
ℹ pass 5
ℹ fail 0

Thirty-two divergences are not a migration defect but two findings, and both are described by a predicate in KNOWN_DIVERGENCES rather than fitted away.

Cap instead of refusal (14 inputs). Gold plus bulk plus a promo code give 14 percent against the declared limit of 13. clamp silently cut the result: at a price of 1234.55 for ten pieces the old code returns a discount of 1604.92 — a number no rule describes. The printed model stops on the same input with FLANG_PROPERTY. This is the difference between “limit” as a function argument and “limit” as a promise: in the second case someone has to decide whether such a combination may be sold at all, instead of silently selling it at 13.

Double rounding of percentages (18 inputs). In the lodash version round sat inside each term. Base 157.50: 7 percent is 11.025, 5 percent is 7.875, both half-kopecks round up, and the sum comes to 18.91. The model adds the percentages and computes 157.50 · 12 / 100 = 18.9, the application rounds once — 18.90. The kopeck of difference did not come from a business rule: the number of round calls was a consequence of how the if was written. The new version has the right answer here, but you could only learn that by comparing the implementations on a grid.

What flang will not replace

  • Time management. debounce and throttle are about clocks and a scheduler. A flang function does not read the clock and keeps no state between calls; otherwise its examples would stop being tests. Actions on the world are described in flang with a планом (plan), but that is a different task.
  • Data of unknown shape. get over an arbitrary path and isEqual over a structure of unknown depth work with JSON that nobody has described yet. In flang every record has declared fields and types, so such work stays at the boundary — where data is brought to the shape of the model.
  • Rounding numbers. There is no rounding form for число; kopecks are the application’s job.
  • Input checks inside the printed function. A function from flang emit does not check its input types itself: the runner flang_cli.js does that at the process boundary, and so does flang run. When you call the function directly from JavaScript, normalize the input before the call — as normalizeTier does.

Iterating over lists is not on this list: flang has it. It is worth moving when a promise about the result moves with it.

Practice in the sandbox

  1. Add an example to «Списать бонусы»: an order of 2000 and a balance of 900. What should you expect? Check it — the expectation 600 matches: the limit applies.
  2. Put the branch если списание.«баланс бонусов» больше предел first, above the small-order branch, and check. The example «мелкий заказ» (small order) violates the promise «мелкий заказ бонусами не оплачивается»: the compiler answers FLANG_EXAMPLE … FLANG_PROPERTY with code 1. The order of branches is part of the rule, and the promise guards it.
  3. Tighten the promise to результат не больше 500 and check. Four examples at once show FLANG_PROPERTY — where clamp would have shown a plausible number.

Common mistakes

  • Hiding the limit in the body instead of a promise. The branch “if above the cap, then the cap” looks like a rule but does what clamp does: it silently returns a number that no rule describes. If the limit is a requirement rather than a business decision to “cut”, write it as an обеспечивает promise, and a violation will stop the calculation.
  • Moving round into the model. There is no rounding for число, and целая часть accepts only exact fractions. The model computes the exact value; kopecks are the application’s job.
  • Leaving defaultTo silently in the adapter. Substituting a value at the boundary is acceptable, but it must be visible: a separate function, a name, a flag “the value was substituted”. Otherwise the default has simply moved from lodash into the adapter.
  • Keeping the customer tier as a string. A string lets “platinum” and typos through. A type with variants does not, and a разбор over it must name every variant — the compiler rejects a forgotten tier.
  • Treating FLANG_PROPERTY as a regression. The promise fired exactly where the old code quietly cut the result. This is not a broken calculation but the first time anyone asked it.
  • Treating code 3 as either failure or success. flang check --proof with code 3 says: the model is checked, but some promises rest on examples. That is the normal state of a model with percentages — and it is also why the printed code checks such promises on every call.

Checklist

  • The list of lodash calls is split in two — business rules and data handling — before the first line of the model is written.
  • Thresholds, percentages, bounds and conditions moved into the model; cloning, comparison, timers and parsing data of unknown shape stayed in the code.
  • No get(o, 'a.b', d) chain moved into the model as is: the field became required, and the decision about the default became a named function at the boundary.
  • Values from a closed list (tiers, statuses) are a type with variants, not a string.
  • Rounding is called once at the boundary, not inside every term.
  • Upper limits are written as promises, and it is known that violating a promise stops the calculation rather than correcting it.
  • There is an equivalence test on a deterministic grid, and the divergences found are declared as a list with explanations rather than fitted to a match.
  • The old code is switched off only after the owner of the rule has gone through the list of divergences.

Catalogue cases on this topic

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

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

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

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