Rules, order, and promises: how a decision is computed

A business rule in flang is a pure function: a tariff, a discount, a classifier, a limit. It does not go to the network and does not write to a database. This chapter shows how to write several rules so that their order is predictable, and how to make the compiler stop if the result goes beyond the allowed bounds.

Minimal example

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

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

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  пример «ниже порога»
    дано покупка равно запись «Покупка» с «сумма» равным 5000
    ожидается 0
  пример «выше порога»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  если покупка.«сумма» не меньше 10000
    то (покупка.«сумма» умножить на 10) делить на 100
    иначе 0

The object describes the shape of the input. The function names the input (принимает), the result type (возвращает) and the body — last, as a single form. The word тотальная is a promise that the function terminates on every input; the compiler proves it. There is no zero “by default”: иначе 0 was written by the rule’s author.

What the compiler does

1. It parses the file and checks the types: the fields in the body and in the examples exist, не меньше compares numbers, and the branches of если give one type.
2. It proves тотальная. There is no recursion here, and the report says exactly that: “proved by composition: no recursion”.
3. It evaluates every пример and compares the result with ожидается. A mismatch is a check error, code 1.
4. With --proof it judges every обеспечивает promise: proved for all inputs, checked only on examples, or not proved at all.

The same order holds in the printed code (flang emit): the code generator may not skip the check of a promise the kernel did not prove.

Rules are functions, not an if/else chain

Several rules are convenient to write as separate functions and add up. Each rule is responsible for its own share and knows nothing about its neighbours:

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

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

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

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

тотальная функция «Промокод на крупный заказ»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«промокод» равен "ЛЕТО2026" и притом покупка.«сумма» не меньше 15000 и притом покупка.«сумма» не больше 100000
    то (покупка.«сумма» умножить на 7) делить на 100
    иначе 0

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

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка ограничена» результат не больше 22000
  пример «обычная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 5000 и «постоянный клиент» равным нет и «промокод» равным "НЕТ"
    ожидается 0
  пример «крупная покупка без промокода»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным нет и «промокод» равным "ЗИМА"
    ожидается 2000
  пример «крупная покупка постоянного клиента с промокодом»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным да и «промокод» равным "ЛЕТО2026"
    ожидается 4400
  пример «покупка ровно на потолок скидки»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да и «промокод» равным "ЛЕТО2026"
    ожидается 22000
  («Большая покупка» от покупка) плюс («Постоянный клиент» от покупка) плюс («Промокод на крупный заказ» от покупка) плюс («Очень крупная покупка» от покупка)

For the example with twenty thousand, three rules out of four fire: 10 % + 5 %

• 7 % of 20,000 give 4,400. No rule cancels another — their results are added together.

The order does not matter here at all: a sum does not change when its terms are rearranged. Each rule is a separate named function, and it can be given its own examples at the boundaries.

If the rules must exclude one another — “the first one that fits” — it is no longer a sum but a single function with если … иначе если:

модуль «Тарифы»

тотальная функция «Ставка доставки»
  принимает вес: неотрицательное
  возвращает число
  обеспечивает «ставка не больше тысячи» результат не больше 1000
  пример «тяжёлое отправление»
    дано вес равно 25
    ожидается 1000
  пример «среднее отправление»
    дано вес равно 12
    ожидается 600
  если вес больше 20
    то 1000
    иначе если вес больше 10
      то 600
      иначе 300

Here the order matters, and it is visible in the text: the branches are read from top to bottom, and the first true one wins. When there are more than two branches and they all compare the same value, a type with variants and a разбор are better — then the compiler checks that every case is handled.

Comparisons and percentages

There are six comparisons: равен, не равен, больше, меньше, не больше, не меньше. равен and не равен work for a number, a string and a flag. The other four work only for numbers, and this is checked before anything runs:

FLANG_TYPE … левый операнд сравнения «lt» имеет тип строка: сравнения порядка допустимы только для чисел

Conditions are joined with the words и притом. Strings are compared with равен; dates only after the application has turned them into numbers (there is no calendar type, see the chapter on types).

A percentage can be written in two ways: 10 процентов от сумма or (сумма умножить на 10) делить на 100. The course models use the second — it shows every operation. Numbers are IEEE 754, so for money without rounding errors there is the сотых type: a whole number of cents.

A promise is a postcondition, not an auto-correction

обеспечивает is a statement about the result on any input. If an example breaks it, the compiler does not trim the discount down to the limit. It stops the check. Tighten the cap in the model above to 3000:

FLANG_EXAMPLE: пример «крупная покупка постоянного клиента с промокодом» функции «Рассчитать скидку»: FLANG_PROPERTY: нарушено свойство «скидка ограничена» функции «Рассчитать скидку»
FLANG_EXAMPLE: пример «покупка ровно на потолок скидки» функции «Рассчитать скидку»: FLANG_PROPERTY: нарушено свойство «скидка ограничена» функции «Рассчитать скидку»

flang check exits with code 1. The printed function behaves the same way: a call with an amount of 20,000 throws an error with the code FLANG_PROPERTY. It does not return 4,400 and does not trim the discount to 3,000.

This is a boundary, not a shortcoming. A silent correction would hide an error in the rule or in the input. An error that surfaces forces you to see it and fix it in the rule itself.

If the cap really is part of the rule — “the discount is at most 22,000, even if the add-ons came to more” — it is written in the body, not in the promise. Then the reader sees that trimming is a business decision, and the promise about the cap is proved:

модуль «Потолок»

тотальная функция «Скидка с потолком»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше потолка» результат не больше 22000
  пример «крупная сумма упирается в потолок»
    дано сумма равно 500000
    ожидается 22000
  пусть итог равно (сумма умножить на 22) делить на 100
  если итог не больше 22000
    то итог
    иначе 22000

The condition is placed so that it matches the promise: in the то branch it is known that the total is at most 22,000. The reversed form если итог больше 22000 то 22000 иначе итог is not proved. The total has the type число, and IEEE 754 numbers include NaN. For it both comparisons are false: the иначе branch would return NaN, and NaN is neither below nor above the cap.

What the kernel proves and what it does not

flang check --proof judges every promise separately. For the model above:

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

The first promise is proved for all inputs: every branch of the body holds a number no greater than 22,000. The second is “сетка 4 значения” (a grid of 4 values): it is checked only on the function’s four examples, and that is not a proof. The final line of the report:

discount-promo.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 2: доказано 1, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

Code 3 is not a program error. It means “not everything is proved”. What is proved on its own:

• если branches where each one holds a number within the limit (a cap, a threshold);
• implications over flags: “if not paid, the result is no”;
• the length of the result of отобразить and отфильтровать;
• bounds that follow from the argument types (неотрицательное).

What is not proved: percentage arithmetic under a cap. That 22 % of an amount is at most 22,000 when the amount is at most 100,000 is not something the kernel derives — such a promise stays checked on examples, and in the printed code it becomes a check on every call. Linking the promises of two functions through addition with a theorem is not possible either: the kernel answers FLANG_PROOF_STEP.

Determinism and the bounds of a rule

The same input always gives the same result: the function does not read the clock, does not go outside and keeps no state between calls. That is why it is tested without mocks, and why the sandbox, flang run and the printed code must agree.

Good candidates for a rule: a discount, a tariff, a fee, a classifier, a limit, an “allow / reject” decision by clear thresholds. Bad ones: “send an email”, “fetch exchange rates from the network”, “write the order in a transaction”. For work with the outside world flang has план: a function returns a description of the action, and whoever started the program carries it out. The rule itself stays pure.

Practice in the sandbox

1. Work out in your head the discount for 12,000 without regular customer status, then add an example with that input and run the check. Add the status — the result grows by exactly 5 % of the same amount.
2. Change the cap 22000 in the “discount is capped” promise to 3000 and read the answer: two examples name the broken promise.
3. Find in the proof report which of the two promises is proved and which is only checked on examples.

Find the promise that the base tariff is at least three hundred and explain why it is proved while the promise about the total tariff is not.

Common mistakes

• FLANG_PARSE … у 'если' нет ветки 'то' — conditions are joined with и instead of и притом, and the parser took the rest of the line for something else.
• FLANG_TYPE … объявлена как неотрицательное, а тело даёт число — division and multiplication give a число. Declare the result as число or restructure the expression.
• FLANG_EXAMPLE … FLANG_PROPERTY: нарушено свойство — an example breaks a promise. This is not syntax but a signal: the rule or the input pushes the result beyond the declared bound. Fix the rule or change the limit on purpose.
• Code 3 taken for success. flang check --proof with code 3 means that some promises are only checked on examples. A build must tell it apart from code 0.

Checklist

• The function has принимает, возвращает and a body; тотальная is proved.
• Independent add-ons are separate functions that are added up.
• “The first one that fits” is a single function with если … иначе если or разбор.
• Ordering comparisons are for numbers only; strings go through равен.
• A promise checks the result, it does not trim it. Trimming, if needed, is a branch of the body.
• I know which promises of the model are proved and which rest only on examples — from the flang check --proof report.

Catalog cases on this topic

Next: examples as tests