Executable specifications in flang Two surfaces: the same rule in Russian and English
0%

Two surfaces: the same rule in Russian and English

Two surfaces: the same rule in Russian and English

This chapter settles the question that usually comes first: if a model is written both by a Russian-speaking analyst and by a developer more at home in English, does that mean two languages and two compilers? No: one compiler and the same checks, two spellings of the keywords.

Minimal example

The rule in Russian:

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

тотальная функция «Скидка»
  принимает сумма: неотрицательное, постоянный: признак
  возвращает число
  обеспечивает «за мелкую покупку скидки нет» если сумма меньше 10000 то результат равен 0 иначе да
  пример «мелкая покупка»
    дано сумма равно 5000
    дано постоянный равно да
    ожидается 0
  пример «большая покупка постоянного клиента»
    дано сумма равно 20000
    дано постоянный равно да
    ожидается 3000
  если сумма не меньше 10000
    то (если постоянный то (сумма умножить на 15) делить на 100 иначе (сумма умножить на 10) делить на 100)
    иначе 0

The same rule in English:

module «Sales»

total function «Discount»
  accepts amount: nat, regular: flag
  returns number
  ensures «no discount on a small purchase» if amount is less than 10000 then result equals 0 else yes
  example «small purchase»
    given amount equals 5000
    given regular equals yes
    expected 0
  example «large purchase by a regular customer»
    given amount equals 20000
    given regular equals yes
    expected 3000
  if amount is at least 10000
    then (if regular then (amount times 15) divided by 100 else (amount times 10) divided by 100)
    else 0

Both files give the same answer: a function with proved termination, two examples passed, the promise proved, flang run computes 3000.

$ flang run sales.en.flang --function Discount --args '{"amount": 20000, "regular": true}'
доказано: утверждений 1
3000

What the compiler does

Every flang keyword has a Russian and an English spelling. принимает and accepts, не меньше and is at least, тотальная функция and total function are one word of the language. The lexer turns both spellings into one token, and from then on parsing, types and proofs do not know which notation the author used.

You can see this right in the token stream. Line 4 of the Russian file and line 4 of the English one:

$ flang tokens sales.flang | sed -n '8,16p'
4:3	>
4:3	слово accepts
4:13	имя сумма
4:18	знак :
4:20	имя неотрицательное
4:35	знак ,
4:37	имя постоянный
4:47	знак :
4:49	слово tFlag

$ flang tokens sales.en.flang | sed -n '8,16p'
4:3	>
4:3	слово accepts
4:11	имя amount
4:17	знак :
4:19	имя nat
4:22	знак ,
4:24	имя regular
4:31	знак :
4:33	слово tFlag

The word принимает became the token accepts, признак and flag became the token tFlag. The parameter names stayed as the author wrote them.

You can find out what a phrase turns into without any file:

$ flang tokens --keyword 'не меньше'
«не меньше» — ключевое слово, конструкция «cmpGte»

$ flang tokens --keyword 'is at least'
«is at least» — ключевое слово, конструкция «cmpGte»

There is no translation through a dictionary or a model here. It is one table of keywords, and line numbers in errors point to your file the same way in either notation.

The English notation of the course model

The sandbox has two versions of the discount model: order-discount.flang and order-discount.en.flang. The functions, conditions, percentages and examples in them match one to one. The proof reports match too: in each model one promise is proved, three rest only on examples, all ten examples pass.

The names differ: «Продажи» and «Sales», «Покупка» and «Purchase», «сумма» and «amount». This is not an automatic translation — the author names them. Only the keywords are translated. So a Russian and an English model are free to describe different domain vocabularies, but with the same rule structure they behave the same.

Two things are never translated:

  • compiler messages — they are in Russian in either notation;
  • number type names — the English name of неотрицательное is nat, not nonnegative (see the errors below).

The compiler does not forbid mixing notations in one file: module on the first line and принимает on the fifth pass the check. But such a file is hard to read. Keep one notation per file.

Two ways to write a field

An object field is written in two ways, and both are equal:

модуль «Счета»

объект «Строка счёта»
  номер является строкой
  «сумма»: неотрицательное
  комментарий иногда является строкой

тотальная функция «Номер строки»
  принимает строка: «Строка счёта»
  возвращает строка
  пример «комментарий можно не задавать»
    дано строка равно запись «Строка счёта» с номер равным "СЧ-1" и «сумма» равным 900
    ожидается "СЧ-1"
  строка.номер

«сумма»: неотрицательное and номер является строкой give the same kind of field. The words иногда является make a field optional: in the example the record is built without a comment, and the check passes. flang ast marks such a field "optional": true.

Names and quotes

A one-word name can be written without guillemets: номер, amount, Счёт. A name with a space is written in guillemets: «постоянный клиент», «Строка счёта». Guillemets are the boundary of a name: inside them the lexer sees one name, not a set of words. In an object declaration and in a parameter type the compiler also accepts straight quotes, but in an expression "…" is a string. Keep guillemets for names, and there will be no confusion.

CamelCase is not needed. If analysts and developers read the model together, «готов к отгрузке» is clearer than ReadyForShipment.

Names are compared byte by byte, without Unicode normalization. The letter “й” as one code point and “и” with a separate combining mark look the same on screen, but for the compiler these are two different names. The function is declared with the first spelling and called with the second — and here is the start of the answer:

$ flang check names.flang
FLANG_UNKNOWN_NAME в файле names.flang, строка 11, столбец 3: имя «Мой» не связано

If names come from different editors or are copied from documents, normalize the files to NFC before checking: uconv -x any-nfc or unicodedata.normalize('NFC', …) in Python.

Values

A flag is written да/нет or yes/no; true/false work as well. Numbers are written in digits, strings in straight quotes. There is no empty value: where an answer may be missing, you declare a type with variants.

Sandbox practice

Press “Check” and note the final line of the report. Then open the English model below and compare: do the numbers of proved promises and examples match?

Rename object «Purchase» to object «Order», but leave the functions that refer to it alone. Check and find FLANG_UNKNOWN_NAME — the compiler does not rename references for the author, it names every line where the old name remained.

Rewrite the fields of the object «Строка счёта» with является: for example, номер является строкой. Make sure the check and the examples give the same answer.

Common mistakes

A typo in the first word. A file must start with модуль or module:

$ flang check typo.flang
FLANG_PARSE в файле typo.flang, строка 1, столбец 1: не разобрана конструкция: неожиданное 'модль'
typo.flang: не проверено — замечаний 1

Guessing an English type name. The English name of неотрицательное is nat:

$ flang check nonneg.flang
модуль «Sales»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_UNKNOWN_NAME в файле nonneg.flang, строка 3, столбец 1: неизвестный тип «nonnegative»
nonneg.flang: не проверено — замечаний 1

A typo in a field name. Field access is checked against the object declaration: FLANG_TYPE … запись «Счёт» не имеет поля «номер счёта». The fix is the same name as in the declaration, letter for letter.

Checklist

  • I explain that the Russian and English notations are one compiler and the same checks, not a translation.
  • I know that only keywords are translated, and the author chooses the names of objects, fields and functions.
  • I write multi-word names in guillemets and know that "…" in an expression is a string.
  • I know names are compared byte by byte, and I normalize files to NFC.

Catalogue cases on this topic

Next: objects and types

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

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

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

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