DigitableCourses

FTS & flang · открытый исходный код · BSD-2

Бизнес-правило, которое исполняется, тестируется и печатается в код.

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

  1. категория «Продажи» Предметная область и первая строка файла. Всё остальное лежит внутри неё отступом: скобок и точек с запятой в языке нет.
  2. объект Покупка Данные и их типы. Встроенных типов пять — строка, число, дата, деньги, признак; иногда является делает поле необязательным.
  3. утилита «Рассчитать скидку» Расчёт. Вход, тип результата и стартовое значение обязательны: пропустите начинает с — компилятор откажет с FTS_UTILITY_INITIAL, а не подставит ноль сам.
  4. правило «Большая покупка» Условие и одно действие. Срабатывают все правила, чьи условия истинны, и складываются: это не цепочка if / else if.
  5. свойство «Скидка ограничена» Постусловие: проверяется после всех правил. Нарушено — остановка с FTS_UTILITY_PROPERTY, а не тихая подрезка до «безопасного» числа.
  6. пример «Двадцать тысяч» Тест внутри спецификации: те же две строки читает человек и выполняет fts test — отсюда подпись под кодом.
discount.fts
категория «Продажи»

  объект Покупка
    сумма является деньгами

  утилита «Рассчитать скидку»
    принимает Покупка
    возвращает деньги
    начинает с 0

    правило «Большая покупка»
      если сумма не меньше 10000
      то добавить 10 процентов от поля сумма

    свойство «Скидка ограничена»
      результат не больше 15000

    пример «Двадцать тысяч»
      дано сумма равна 20000
      ожидается результат равен 2000
discount.en.fts
category "Sales"

  object Purchase
    amount is money

  utility "Calculate discount"
    accepts Purchase
    returns money
    starts with 0

    rule "Large purchase"
      if amount is at least 10000
      then add 10 percent of field amount

    property "Discount is capped"
      result is at most 15000

    example "Twenty thousand purchase"
      given amount equals 20000
      expected result equals 2000
fts test discount.fts1/1 passed

Как читать код на этой странице девять видов лексем, один словарь цветов на все языки

  • утилитаобъявление
  • принимаетключевое слово
  • «Рассчитать скидку»предметное имя
  • деньгитип
  • не меньшесравнение
  • далитерал
  • "постоянный"строка
  • 20000число
  • // пояснениекомментарий

Раскраска FTS снята настоящим лексером языка при сборке (npm run fts:highlight), напечатанный JavaScript, C, Go, Rust, Python и файлы проектов красит Chroma, встроенный в Hugo. Ни то, ни другое не ходит в сеть и не грузит библиотек в браузер: страница остаётся раскрашенной с выключенным JavaScript и в оффлайн-поставке.

От правила к модели

Язык прибавляется по одной конструкции, и каждая покупает компилятору новую проверку.

Четыре ступени на одном и том же примере. Первые три — куски файла из первого экрана, четвёртая — из модели «Отгрузка заказа», её можно открыть в песочнице на шаге 3.

ступень 1 · правило

Условие и одно действие

правило «Большая покупка»
  если сумма не меньше 10000
  то добавить 10 процентов от поля сумма

Сравнений в языке ровно шесть: равен, не равен, больше, меньше, не больше, не меньше. Седьмое даст FTS_UTILITY_COMPARISON с номером строки. Правил может быть сколько угодно, и работают они не как if / else if: выполняются все, чьи условия истинны, и складываются.

ступень 2 · утилита

Правила становятся функцией

утилита «Рассчитать скидку»
  принимает Покупка
  возвращает деньги
  начинает с 0

Три строки обязательны — вход, тип результата и стартовое значение. Ноль в начинает с написал автор модели, а не подставил рантайм: без строки компилятор откажет с FTS_UTILITY_INITIAL. С ней fts run считает утилиту на JSON, а flang emit печатает её в пять языков.

ступень 3 · свойство и пример

Проверка на все входы и проверка на один

свойство «Скидка ограничена»
  результат не больше 15000

пример «Двадцать тысяч»
  дано сумма равна 20000
  ожидается результат равен 2000

Свойство — постусловие: проверяется после всех правил, и нарушенное останавливает выполнение с FTS_UTILITY_PROPERTY, а не подрезает результат до «безопасного» числа втихую. Пример — тест, лежащий внутри спецификации: те же строки читает человек и выполняет fts test. Разойтись документации и коду здесь нечем — файл один.

ступень 4 · морфизм и теорема

Категорная часть, и она маленькая

морфизм «Готовый заказ можно отгрузить»
  если «Готов к отгрузке»
  то «Отгрузить заказ разрешено»

теорема «Заказ ЗК-7781 можно отгрузить»
  дано Заказ имеет «готов к отгрузке» равное да
  в данных заказы найти где номер равен «ЗК-7781»
  по морфизму «Готовый заказ можно отгрузить»
  следовательно «Отгрузить заказ разрешено»

Объекты категории — типы: структура Заказ и именованные состояния. Морфизм — стрелка A → B с именем и объявленным законом; он не выполняет переход, а утверждает его допустимость. Композиция разрешена ровно тогда, когда кодомен предыдущей стрелки совпал с доменом следующей, а равенство типов номинальное — по имени. Строка в данных — самая важная: она превращает рассуждение в проверяемое утверждение, называя, где искать свидетельство.

fts check · проверено статически
Имена не дублируются, поля объектов существуют, домен и кодомен каждого морфизма — реальные типы, объявленный вывод совпал с вычисленным. Данных на этом уровне ещё нет.
fts test · выполнено
Примеры утилиты сошлись с текущей семантикой. Это тест, а не доказательство: сходятся ровно те входы, что написаны в файле, — отсюда три примера на одно правило вокруг границы.
flang check · доказано
У функции со словом тотальная компилятор принял доказательство структурного убывания: она не может зациклиться. Анализ консервативен и отвергает часть действительно завершающихся программ — FLANG_NOT_TOTAL.
чего не даёт ни один уровень
Истинности самого правила, полноты модели и актуальности снимка данных. «FTS доказал, что заказ можно отгружать» — неверно; верно: «проверил свидетельство и типизируемость вывода при объявленных законах». Где проходит эта граница.

Одна модель · пять языков

Спецификация не описывает код проекта — она в него печатается.

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

order-discount.fts · тот же файл, что открыт в песочницеисходник
    правило «Очень крупная покупка»
      если сумма больше 100000
      то добавить 15000

    свойство «Скидка ограничена»
      результат не больше 15000
prodazhi.js · хвост функции «Рассчитать скидку»flang emit order-discount.fts --target js
  let $t6
  if ($cond($gt($field(vhod, "сумма"), 100000))) {
    $t6 = $add(rezultat2, 15000)
  } else {
    $t6 = rezultat2
  }
  const rezultat3 = $t6
  // постусловие «Скидка ограничена»
  if (!$post($lte(rezultat3, 15000), "Скидка ограничена", "Рассчитать скидку")) {
    $fail("FTS_UTILITY_PROPERTY", "нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»")
  }
  return rezultat3
}
prodazhi.c · хвост функции «Рассчитать скидку»flang emit order-discount.fts --target c
  fl_value fl_t26 = fl_nothing();
  FL_TRY(fl_field_get(ctx, vhod, "сумма", &fl_t26, error));
  fl_value fl_t27 = fl_nothing();
  FL_TRY(fl_gt(ctx, fl_t26, fl_number(100000.0), &fl_t27, error));
  bool fl_t28 = false;
  FL_TRY(fl_cond(ctx, fl_t27, &fl_t28, error));
  fl_value fl_t29 = fl_nothing();
  if (fl_t28) {
    fl_value fl_t30 = fl_nothing();
    FL_TRY(fl_add(ctx, rezultat2, fl_number(15000.0), &fl_t30, error));
    fl_t29 = fl_t30;
  } else {
    fl_t29 = rezultat2;
  }
  const fl_value rezultat3 = fl_t29; /* пусть «результат3» */
  (void)rezultat3;
  const fl_value fl_t31 = rezultat3;
  fl_value fl_t32 = fl_nothing();
  FL_TRY(fl_lte(ctx, fl_t31, fl_number(15000.0), &fl_t32, error));
  /* постусловие «Скидка ограничена» */
  bool fl_t33 = false;
  FL_TRY(fl_post(ctx, fl_t32, "Скидка ограничена", "Рассчитать скидку", &fl_t33, error));
  if (!fl_t33) {
    return fl_fail(ctx, error, "FTS_UTILITY_PROPERTY", "%s", "нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»");
  }
  *result = fl_t31;
  return FL_OK;
}
prodazhi.go · хвост функции «Рассчитать скидку»flang emit order-discount.fts --target go
	t46, e47 := rt.FieldGet(ctx, vhod, "сумма")
	if e47 != nil {
		return rt.Value{}, e47
	}
	t48, e49 := rt.Gt(ctx, t46, rt.Number(100000.0))
	if e49 != nil {
		return rt.Value{}, e49
	}
	t50, e51 := rt.Cond(ctx, t48)
	if e51 != nil {
		return rt.Value{}, e51
	}
	var t52 rt.Value
	if t50 {
		t53, e54 := rt.Add(ctx, rezultat2, rt.Number(15000.0))
		if e54 != nil {
			return rt.Value{}, e54
		}
		t52 = t53
	} else {
		t52 = rezultat2
	}
	// пусть «результат3»
	rezultat3 := t52
	_ = rezultat3
	t55 := rezultat3
	t56, e57 := rt.Lte(ctx, t55, rt.Number(15000.0))
	if e57 != nil {
		return rt.Value{}, e57
	}
	// постусловие «Скидка ограничена»
	t58, e59 := rt.Post(ctx, t56, "Скидка ограничена", "Рассчитать скидку")
	if e59 != nil {
		return rt.Value{}, e59
	}
	if !t58 {
		return rt.Value{}, rt.Fail("FTS_UTILITY_PROPERTY", "%s", "нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»")
	}
	return t55, nil
}
prodazhi.rs · хвост функции «Рассчитать скидку»flang emit order-discount.fts --target rust
    let t26 = rt::field_get(ctx, vhod.clone(), "сумма")?;
    let t27 = rt::gt(ctx, t26, rt::number(100000.0))?;
    let t28 = rt::cond(ctx, t27)?;
    let t29 = if t28 {
        let t30 = rt::add(ctx, rezultat2.clone(), rt::number(15000.0))?;
        t30
    } else {
        rezultat2.clone()
    };
    // пусть «результат3»
    let rezultat3 = t29;
    let t31 = rezultat3.clone();
    // постусловие «Скидка ограничена»
    let t32 = rt::lte(ctx, t31.clone(), rt::number(15000.0))?;
    let t33 = rt::post(ctx, t32, "Скидка ограничена", "Рассчитать скидку")?;
    if !t33 {
        return Err(rt::fail("FTS_UTILITY_PROPERTY", "нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»".to_string()));
    }
    Ok(t31)
}
prodazhi.py · хвост функции «Рассчитать скидку»flang emit order-discount.fts --target python
    if rt.cond(ctx, rt.gt(ctx, rt.field_get(ctx, vhod, "сумма"), rt.number(100000.0))):
        _t6 = rt.add(ctx, rezultat2, rt.number(15000.0))
    else:
        _t6 = rezultat2
    # пусть «результат3»
    rezultat3 = _t6
    _t7 = rezultat3
    # постусловие «Скидка ограничена»
    if not rt.post(ctx, rt.lte(ctx, _t7, rt.number(15000.0)), "Скидка ограничена", "Рассчитать скидку"):
        raise rt.fail("FTS_UTILITY_PROPERTY", "нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»")
    return _t7
свойство исполняется
«Скидка ограничена» в каждом языке — проверка с кодом FTS_UTILITY_PROPERTY, а не комментарий рядом.
совпадает с интерпретатором
Собранный C, собранный Rust, напечатанные JavaScript и Python на входе «сумма 20000, постоянный клиент да» отвечают 3000 — столько же, сколько песочница на шаге 3.
ядро FTS написано на flang
Лексер, парсер, вычислитель и печать JSON — 300 функций, все тотальные; цепочка «из текста в JSON» сходится байт в байт с эталонным ядром на TypeScript.
собирается без Node
Ядро печатается в C и собирается cc -Werror -pedantic; в зависимостях только libc и libm.

Быстрый старт

Node.js 20, клон репозитория — и правило считается.

Пакета в npm пока нет, поэтому CLI собирается из исходников. У ядра нет рантайм-зависимостей, а flang запускается прямо из клона, без сборки. Чтобы просто посмотреть, ставить ничего не нужно: песочница ниже считает тем же компилятором прямо во вкладке.

1 · поставитьbash
git clone https://github.com/digitable-lol/flang.git
cd flang
npm ci
npm run build
2 · выполнить первое правилоbash
# типы, ссылки, композиция
node dist/src/cli.js check examples/utilities/discount.fts --pretty

# примеры, записанные внутри правила
node dist/src/cli.js test examples/utilities/discount.fts --pretty

# напечатать в код: c | go | rust | python | js
node flang/bin/flang.mjs emit examples/utilities/discount.fts \
  --target go --out ./out-go

Каждая команда печатает JSON в stdout, диагностику в stderr и возвращает ненулевой код на провале — один контракт для CI, редактора и агента.

Живая песочница

Отредактируйте правило — результат пересчитается в вашей вкладке.

Тот же компилятор @digitable-lol/fts@0.4.0, что и в Node.js: всё считается локально, без единого запроса на сервер. Вкладки справа — это команды CLI: «Проверка» — fts check, «Примеры» — fts test, «Выполнить» — fts run, «Доказательство» — fts prove.

Что песочница не делает. prove — символьный вывод: он показывает, что цепочка морфизмов типизируется, но данные при этом не проверяет и даёт тот же ответ с контекстом и без него. Проверенный сертификат выпускает fts certify и пересчитывает fts verify — они считают дайджесты через node:crypto и живут на серверной стороне. Чем символьный вывод отличается от проверенного.

order-discount.fts

Компилятор загрузится, когда секция появится на экране.

Компилятор загружается…

На чём это уже написано

26 задач LeetCode на flang: у 20 завершение доказано компилятором.

Алгоритмическая задача не даёт предметной опоры — это проверка языка на чужой территории. Файлы читаются из репозитория языка при сборке страницы, числа сняты запуском flang check и flang test.

26
решений в репозитории языка
20
с доказанным завершением
62/77
тотальных функций
135/135
примеров сходится
Пришли учиться? Каждая строчка карточки объясняется главой курса. Ниже в каждом решении: техника, две гарантии компилятора, список функций с отметкой тотальности и полный исходник. Вот где про это написано — по одной главе на каждый элемент.
  1. Отступы, слова, примерыЧем запись решения отличается от псевдокода и почему пример — часть исходника.
  2. Записи, варианты, спискиОткуда в решениях деревьев берутся запись и вариант и почему их не приходится объявлять дважды.
  3. ТотальностьЧто стоит за значком «завершение доказано» и у скольких решений его нет: 6 из 26.
  4. Свёртки вместо цикловТа самая «свёртка», с которой начинается техника почти каждого решения ниже.
  5. flang check и flang testДве команды, которыми сняты все числа на карточках; те же коды выхода в CI.
  6. Границы языкаНевыразимых задач в наборе — 12: почему они не пишутся вовсе и почему это записано, а не спрятано.
1 Две суммы Two Sum завершение доказано списки 6/6 примеров 3/3 функций тотальны 65 строк

Вместо словаря «значение → номер» — вложенный проход: для каждой головы ищем дополнение в хвосте. O(n²) как прямая цена отсутствия хеш-таблиц.

flang check
модуль «Две суммы» проходит проверку типов. Главная функция «Две суммы» тотальна: компилятор принял доказательство завершения.
flang test
6 примеров в файле, сошлось 6, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Позиция значениятотальная
  • Поиск пары с позициитотальная
  • Две суммытотальная
examples/flang/leetcode/001-two-sum.flang3500 байт · sha256 8f1a940cc7b84f1c
модуль «Две суммы»

// LeetCode 1. Two Sum.
// Дан список чисел и цель. Найти два разных элемента, дающих в сумме цель,
// и вернуть их номера. Номера — с нуля, как в условии задачи; язык нумерует
// строки с единицы, поэтому пересчёт делается один раз, в конце.
//
// Тотальная. Хеш-таблиц в языке нет, поэтому вместо словаря «значение → номер»
// работает вложенный проход: для каждой головы ищем дополнение в хвосте.
// Это O(n²) вместо O(n) — прямая цена отсутствия ассоциативного массива.

тотальная функция «Позиция значения»
  принимает элементы: список числа, нужное: число
  возвращает число
  пример «Найдено вторым»
    дано элементы равно [5, 7]
    дано нужное равно 7
    ожидается 2
  пример «Не найдено»
    дано элементы равно [5, 7]
    дано нужное равно 9
    ожидается 0
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      если голова равен нужное
        то 1
        иначе
          пусть дальше равно «Позиция значения» от хвост и нужное
          если дальше равен 0 то 0 иначе дальше плюс 1

тотальная функция «Поиск пары с позиции»
  принимает элементы: список числа, цель: число, позиция: число
  возвращает список числа
  пример «Пара в начале»
    дано элементы равно [2, 7, 11]
    дано цель равно 9
    дано позиция равно 0
    ожидается [0, 1]
  разбор элементов
    случай пусто
      то пустой список
    случай голова и хвост
      пусть смещение равно «Позиция значения» от хвост и (цель минус голова)
      если смещение больше 0
        то [позиция, позиция плюс смещение]
        иначе «Поиск пары с позиции» от хвост и цель и (позиция плюс 1)

тотальная функция «Две суммы»
  принимает элементы: список числа, цель: число
  возвращает список числа
  пример «Пример 1 из условия»
    дано элементы равно [2, 7, 11, 15]
    дано цель равно 9
    ожидается [0, 1]
  пример «Пример 2 из условия»
    дано элементы равно [3, 2, 4]
    дано цель равно 6
    ожидается [1, 2]
  пример «Пример 3 из условия»
    дано элементы равно [3, 3]
    дано цель равно 6
    ожидается [0, 1]
  «Поиск пары с позиции» от элементы и цель и 0
104 Глубина дерева Maximum Depth of Binary Tree завершение доказано деревья 3/3 примеров 4/4 функций тотальны 61 строк

Поле варианта — часть значения, поэтому рекурсия по поддеревьям доказывается сразу. Дерево в примерах строится из списка: вариант в «дано» не записать.

flang check
модуль «Глубина дерева» проходит проверку типов, объявлено типов: 1. Главная функция «Глубина из списка» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Вставить в деревототальная
  • Дерево из спискатотальная
  • Глубинатотальная
  • Глубина из спискатотальная
examples/flang/leetcode/104-maximum-depth-of-binary-tree.flang3734 байт · sha256 9077b460f11f9041
модуль «Глубина дерева»

// LeetCode 104. Maximum Depth of Binary Tree.
// Найти длину самого длинного пути от корня до листа.
//
// Тотальная. Дерево — сумма типов, а поле варианта анализ завершаемости
// считает частью значения, поэтому рекурсия по поддеревьям доказывается
// сразу и без ухищрений. Деревья язык принимает лучше, чем строки и числа.
//
// Дерево в примерах строится из списка: значение варианта нельзя записать
// в «дано» (парсер теряет имя конструктора), поэтому вход задаётся списком,
// а «Дерево из списка» превращает его в дерево поиска.

тип «Дерево»
  вариант Лист
  вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»

тотальная функция «Вставить в дерево»
  принимает дерево: «Дерево», число: число
  возвращает «Дерево»
  разбор дерева
    случай Лист
      то Узел с значение равным число и левое равным вариант Лист и правое равным вариант Лист
    случай вариант Узел с значение как зн и левое как л и правое как п
      если число меньше зн
        то
          пусть новое равно «Вставить в дерево» от л и число
          Узел с значение равным зн и левое равным новое и правое равным п
        иначе
          пусть новое равно «Вставить в дерево» от п и число
          Узел с значение равным зн и левое равным л и правое равным новое

тотальная функция «Дерево из списка»
  принимает элементы: список числа
  возвращает «Дерево»
  свёртка элементы начиная с вариант Лист как акк и эл  «Вставить в дерево» от акк и эл

тотальная функция «Глубина»
  принимает дерево: «Дерево»
  возвращает число
  разбор дерева
    случай Лист
      то 0
    случай вариант Узел с левое как л и правое как п
      пусть слева равно «Глубина» от л
      пусть справа равно «Глубина» от п
      1 плюс (если слева больше справа то слева иначе справа)

тотальная функция «Глубина из списка»
  принимает элементы: список числа
  возвращает число
  пример «Сбалансированное дерево»
    дано элементы равно [2, 1, 3]
    ожидается 2
  пример «Цепочка»
    дано элементы равно [1, 2, 3, 4]
    ожидается 4
  пример «Пустое дерево»
    дано элементы равно пустой список
    ожидается 0
  «Глубина» от («Дерево из списка» от элементы)
35 Место вставки Search Insert Position завершение доказано поиск 3/3 примеров 1/1 функций тотальны 27 строк

Одна свёртка: счёт элементов меньше цели. O(n) вместо требуемого O(log n) — двоичный поиск в тотальном классе требует приёма с топливом.

flang check
модуль «Место вставки» проходит проверку типов. Главная функция «Место вставки» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Место вставкитотальная
examples/flang/leetcode/035-search-insert-position.flang1601 байт · sha256 222865fab75e7418
модуль «Место вставки»

// LeetCode 35. Search Insert Position.
// В отсортированном списке найти номер цели, а если её нет — номер, куда её
// следовало бы вставить. Номера с нуля, как в условии.
//
// Тотальная. Условие требует O(log n), здесь же один линейный проход:
// двоичный поиск в тотальном классе требует особого приёма (см. 704), а
// линейная свёртка доказывается сама. Ответ тот же, сложность хуже —
// и это честная цена, а не недосмотр.

тотальная функция «Место вставки»
  принимает элементы: список числа, цель: число
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [1, 3, 5, 6]
    дано цель равно 5
    ожидается 2
  пример «Пример 2 из условия»
    дано элементы равно [1, 3, 5, 6]
    дано цель равно 2
    ожидается 1
  пример «Пример 3 из условия»
    дано элементы равно [1, 3, 5, 6]
    дано цель равно 7
    ожидается 4
  свёртка элементы начиная с 0 как акк и эл  если эл меньше цель то акк плюс 1 иначе акк
509 Фибоначчи Fibonacci Number доказательства нет числа 6/6 примеров 0/2 функций тотальны 42 строк

Линейный вариант с двумя накопителями. Нетотальна ровно из-за счётчика: убывания по числу анализ не знает.

flang check
модуль «Фибоначчи» проходит проверку типов. Главная функция «Фибоначчи» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
6 примеров в файле, сошлось 6, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Фибоначчи шагомбез доказательства
  • Фибоначчибез доказательства
examples/flang/leetcode/509-fibonacci-number.flang2067 байт · sha256 f097f2cbd55895fe
модуль «Фибоначчи»

// LeetCode 509. Fibonacci Number.
// F(0) = 0, F(1) = 1, дальше сумма двух предыдущих.
//
// Обычная. Прямое определение F(n) = F(n−1) + F(n−2) не проходит анализ
// завершаемости по той же причине, что и всё остальное на числах: убывания
// по числовому аргументу он не знает. Здесь взят линейный вариант с двумя
// накопителями — он и работает быстрее, и делает нетотальность заметной:
// единственное, что мешает доказать конец, — счётчик.

функция «Фибоначчи шагом»
  принимает осталось: число, предыдущее: число, текущее: число
  возвращает число
  пример «Ноль шагов»
    дано осталось равно 0
    дано предыдущее равно 7
    дано текущее равно 9
    ожидается 7
  если осталось не больше 0
    то предыдущее
    иначе «Фибоначчи шагом» от (осталось минус 1) и текущее и (предыдущее плюс текущее)

функция «Фибоначчи»
  принимает н: число
  возвращает число
  пример «Пример 1 из условия»
    дано н равно 2
    ожидается 1
  пример «Пример 2 из условия»
    дано н равно 3
    ожидается 2
  пример «Пример 3 из условия»
    дано н равно 4
    ожидается 3
  пример «Нулевое»
    дано н равно 0
    ожидается 0
  пример «Тридцатое»
    дано н равно 30
    ожидается 832040
  «Фибоначчи шагом» от н и 0 и 1

Остальные решения по категориям: 22 из 26

Раскройте карточку — под ней полный файл из flang/examples/leetcode. Связывания модулей в языке нет, поэтому решение самодостаточно и запускается как есть. Раскраска этих 22 файлов лежит отдельным файлом и приезжает при раскрытии карточки: код в разметке есть всегда, цвета — по требованию.

26 Удалить повторы Remove Duplicates from Sorted Array завершение доказано списки 4/4 примеров 2/2 функций тотальны 32 строк

Свёртка с проверкой «содержит». Изменения на месте нет: значения flang неизменяемы, возвращается новый список.

flang check
модуль «Удалить повторы» проходит проверку типов. Главная функция «Без повторов» тотальна: компилятор принял доказательство завершения.
flang test
4 примеров в файле, сошлось 4, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Без повторовтотальная
  • Сколько уникальныхтотальная
examples/flang/leetcode/026-remove-duplicates-from-sorted-array.flang1891 байт · sha256 0307f8287403d080
модуль «Удалить повторы»

// LeetCode 26. Remove Duplicates from Sorted Array.
// Из отсортированного списка убрать повторы. В условии просят изменить массив
// на месте и вернуть число уникальных; изменяемых массивов в языке нет и быть
// не может — значения flang неизменяемы, — поэтому возвращается новый список,
// а «число уникальных» вынесено отдельной функцией.
//
// Тотальная: свёртка по списку, рекурсии нет вовсе.

тотальная функция «Без повторов»
  принимает элементы: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано элементы равно [1, 1, 2]
    ожидается [1, 2]
  пример «Пример 2 из условия»
    дано элементы равно [0, 0, 1, 1, 1, 2, 2, 3, 3, 4]
    ожидается [0, 1, 2, 3, 4]
  свёртка элементы начиная с пустой список как акк и эл
    если акк содержит эл то акк иначе добавить эл к акк

тотальная функция «Сколько уникальных»
  принимает элементы: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [1, 1, 2]
    ожидается 2
  пример «Пустой список»
    дано элементы равно пустой список
    ожидается 0
  длина («Без повторов» от элементы)
66 Прибавить единицу Plus One завершение доказано списки 6/6 примеров 3/3 функций тотальны 57 строк

Перенос идёт справа налево, свёртка — слева направо, поэтому список обращается дважды. Обращение выражено свёрткой: встроенного «в начало» нет.

flang check
модуль «Прибавить единицу» проходит проверку типов, объявлено типов: 1. Главная функция «Прибавить единицу» тотальна: компилятор принял доказательство завершения.
flang test
6 примеров в файле, сошлось 6, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать в началототальная
  • Обратитьтотальная
  • Прибавить единицутотальная
examples/flang/leetcode/066-plus-one.flang3502 байт · sha256 216e595fc3dfe89e
модуль «Прибавить единицу»

// LeetCode 66. Plus One.
// Список цифр — большое число. Прибавить к нему единицу.
//
// Тотальная. Перенос идёт справа налево, а свёртка идёт слева направо,
// поэтому список сначала обращается, потом сворачивается, потом обращается
// обратно. Обращение выражается свёрткой, а не встроенной формой: приписать
// элемент в начало списка встроенным «добавить … к …» нельзя — оно
// дописывает в конец.

объект «Перенос»
  перенос является числом
  цифры является список числа

тотальная функция «Приписать в начало»
  принимает первый: число, элементы: список числа
  возвращает список числа
  пример «В непустой»
    дано первый равно 1
    дано элементы равно [2]
    ожидается [1, 2]
  свёртка элементы начиная с [первый] как акк и эл → добавить эл к акк

тотальная функция «Обратить»
  принимает элементы: список числа
  возвращает список числа
  пример «Три элемента»
    дано элементы равно [1, 2, 3]
    ожидается [3, 2, 1]
  свёртка элементы начиная с пустой список как акк и эл → «Приписать в начало» от эл и акк

тотальная функция «Прибавить единицу»
  принимает цифры: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано цифры равно [1, 2, 3]
    ожидается [1, 2, 4]
  пример «Пример 2 из условия»
    дано цифры равно [4, 3, 2, 1]
    ожидается [4, 3, 2, 2]
  пример «Пример 3 из условия»
    дано цифры равно [9]
    ожидается [1, 0]
  пример «Сплошные девятки»
    дано цифры равно [9, 9, 9]
    ожидается [1, 0, 0, 0]
  пусть начальное равно запись «Перенос» с перенос равным 1 и цифры равным пустой список
  пусть итог равно свёртка («Обратить» от цифры) начиная с начальное как акк и цифра
    пусть сумма равно цифра плюс акк.перенос
    пусть новая равно сумма остаток от 10
    пусть дальше равно если сумма не меньше 10 то 1 иначе 0
    запись «Перенос» с перенос равным дальше и цифры равным (добавить новая к акк.цифры)
  пусть результат равно «Обратить» от итог.цифры
  если итог.перенос равен 1
    то «Приписать в начало» от 1 и результат
    иначе результат
88 Слияние отсортированных Merge Sorted Array завершение доказано списки 6/6 примеров 3/3 функций тотальны 59 строк

Не классическое слияние (оно убывает то по одному списку, то по другому и получает FLANG_NOT_TOTAL), а вставка в свёртке: O(n·m), зато доказуемо конечно.

flang check
модуль «Слияние отсортированных» проходит проверку типов. Главная функция «Слить отсортированные» тотальна: компилятор принял доказательство завершения.
flang test
6 примеров в файле, сошлось 6, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать в началототальная
  • Вставить по порядкутотальная
  • Слить отсортированныетотальная
examples/flang/leetcode/088-merge-sorted-array.flang3595 байт · sha256 c42dbe9146cd8a55
модуль «Слияние отсортированных»

// LeetCode 88. Merge Sorted Array.
// Слить два отсортированных списка в один отсортированный.
//
// Тотальная — но не тем алгоритмом, каким её пишут обычно. Классическое
// слияние рекурсирует то по первому списку, то по второму, и анализ
// завершаемости такой цикл отвергает: он требует ОДНУ позицию аргумента,
// убывающую на каждом рекурсивном вызове (totality.mjs, контрпример в шапке
// файла). Слияние даёт две разные позиции и получает FLANG_NOT_TOTAL.
//
// Поэтому здесь слияние вставками: «Вставить по порядку» рекурсирует ровно
// по хвосту второго аргумента, а внешний проход — свёртка. Результат тот же,
// сложность O(n·m) вместо O(n+m).

тотальная функция «Приписать в начало»
  принимает первый: число, элементы: список числа
  возвращает список числа
  пример «В непустой»
    дано первый равно 1
    дано элементы равно [2]
    ожидается [1, 2]
  свёртка элементы начиная с [первый] как акк и эл → добавить эл к акк

тотальная функция «Вставить по порядку»
  принимает значение: число, элементы: список числа
  возвращает список числа
  пример «В середину»
    дано значение равно 2
    дано элементы равно [1, 3]
    ожидается [1, 2, 3]
  пример «В пустой»
    дано значение равно 2
    дано элементы равно пустой список
    ожидается [2]
  разбор элементов
    случай пусто
      то [значение]
    случай голова и хвост
      если значение не больше голова
        то «Приписать в начало» от значение и элементы
        иначе «Приписать в начало» от голова и («Вставить по порядку» от значение и хвост)

тотальная функция «Слить отсортированные»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано первый равно [1, 2, 3]
    дано второй равно [2, 5, 6]
    ожидается [1, 2, 2, 3, 5, 6]
  пример «Пример 2 из условия»
    дано первый равно [1]
    дано второй равно пустой список
    ожидается [1]
  пример «Пример 3 из условия»
    дано первый равно пустой список
    дано второй равно [1]
    ожидается [1]
  свёртка второй начиная с первый как акк и эл → «Вставить по порядку» от эл и акк
136 Одиночное число Single Number завершение доказано списки 4/4 примеров 2/2 функций тотальны 36 строк

Побитового исключающего ИЛИ в языке нет вовсе, поэтому подсчёт вхождений: O(n²) вместо O(n).

flang check
модуль «Одиночное число» проходит проверку типов. Главная функция «Одиночное число» тотальна: компилятор принял доказательство завершения.
flang test
4 примеров в файле, сошлось 4, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Считать вхождениятотальная
  • Одиночное числототальная
examples/flang/leetcode/136-single-number.flang2013 байт · sha256 81a03d914c827526
модуль «Одиночное число»

// LeetCode 136. Single Number.
// В списке каждое число встречается дважды, кроме одного. Найти его.
//
// Тотальная. Канонического решения «сложить всё исключающим ИЛИ» здесь нет:
// побитовых операций в языке нет вообще (SPEC, раздел 4 перечисляет только
// арифметику и сравнения). Поэтому — подсчёт вхождений, O(n²) вместо O(n).

тотальная функция «Считать вхождения»
  принимает элементы: список числа, значение: число
  возвращает число
  пример «Два вхождения»
    дано элементы равно [4, 1, 4]
    дано значение равно 4
    ожидается 2
  свёртка элементы начиная с 0 как акк и эл → если эл равен значение то акк плюс 1 иначе акк

тотальная функция «Одиночное число»
  принимает элементы: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [2, 2, 1]
    ожидается 1
  пример «Пример 2 из условия»
    дано элементы равно [4, 1, 2, 1, 2]
    ожидается 4
  пример «Пример 3 из условия»
    дано элементы равно [1]
    ожидается 1
  пусть одиночные равно отфильтровать элементы где эл → («Считать вхождения» от элементы и эл) равен 1
  разбор одиночные
    случай пусто
      то 0
    случай голова и хвост
      голова
169 Мажоритарный элемент Majority Element завершение доказано списки 3/3 примеров 2/2 функций тотальны 34 строк

Прямой подсчёт вхождений и фильтр. Бойер — Мур без изменяемых счётчиков всё равно свёлся бы к свёртке с записью.

flang check
модуль «Мажоритарный элемент» проходит проверку типов. Главная функция «Мажоритарный элемент» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Считать вхождениятотальная
  • Мажоритарный элементтотальная
examples/flang/leetcode/169-majority-element.flang1974 байт · sha256 8b6fd2c62b01052f
модуль «Мажоритарный элемент»

// LeetCode 169. Majority Element.
// Найти элемент, встречающийся более чем в половине позиций списка.
//
// Тотальная. Алгоритм Бойера — Мура здесь не нужен: без изменяемых счётчиков
// он всё равно свёлся бы к свёртке с записью-состоянием, а прямой подсчёт
// вхождений короче и очевидно верен. Цена — O(n²).

тотальная функция «Считать вхождения»
  принимает элементы: список числа, значение: число
  возвращает число
  пример «Три тройки»
    дано элементы равно [3, 3, 3, 1]
    дано значение равно 3
    ожидается 3
  свёртка элементы начиная с 0 как акк и эл → если эл равен значение то акк плюс 1 иначе акк

тотальная функция «Мажоритарный элемент»
  принимает элементы: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [3, 2, 3]
    ожидается 3
  пример «Пример 2 из условия»
    дано элементы равно [2, 2, 1, 1, 1, 2, 2]
    ожидается 2
  пусть половина равно (длина элементы) делить на 2
  пусть частые равно отфильтровать элементы где эл → («Считать вхождения» от элементы и эл) больше половина
  разбор частые
    случай пусто
      то 0
    случай голова и хвост
      голова
217 Есть повторы Contains Duplicate завершение доказано списки 3/3 примеров 1/1 функций тотальны 26 строк

Рекурсия по хвосту плюс «хвост содержит голову». Множеств нет, отсюда O(n²).

flang check
модуль «Есть повторы» проходит проверку типов. Главная функция «Есть повторы» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Есть повторытотальная
examples/flang/leetcode/217-contains-duplicate.flang1340 байт · sha256 2c175e173292198d
модуль «Есть повторы»

// LeetCode 217. Contains Duplicate.
// Есть ли в списке хотя бы одно значение, встречающееся дважды.
//
// Тотальная: рекурсия строго по хвосту списка. Множества в языке нет,
// поэтому проверка «голова встречается дальше» — линейный поиск,
// и всё решение получается O(n²).

тотальная функция «Есть повторы»
  принимает элементы: список числа
  возвращает признак
  пример «Пример 1 из условия»
    дано элементы равно [1, 2, 3, 1]
    ожидается да
  пример «Пример 2 из условия»
    дано элементы равно [1, 2, 3, 4]
    ожидается нет
  пример «Пример 3 из условия»
    дано элементы равно [1, 1, 1, 3, 3, 4, 3, 2, 4, 2]
    ожидается да
  разбор элементов
    случай пусто
      то нет
    случай голова и хвост
      если хвост содержит голова то да иначе «Есть повторы» от хвоста
283 Сдвинуть нули Move Zeroes завершение доказано списки 3/3 примеров 2/2 функций тотальны 30 строк

Два фильтра и склейка, без рекурсии. «На месте» не выражается: значения неизменяемы.

flang check
модуль «Сдвинуть нули» проходит проверку типов. Главная функция «Сдвинуть нули» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Соединить спискитотальная
  • Сдвинуть нулитотальная
examples/flang/leetcode/283-move-zeroes.flang1765 байт · sha256 cea31b85798acb39
модуль «Сдвинуть нули»

// LeetCode 283. Move Zeroes.
// Перенести все нули в конец, сохранив порядок остальных.
//
// Тотальная и без единой рекурсии: два фильтра и склейка. В условии просят
// работать «на месте», но изменяемых массивов в языке нет — возвращается
// новый список того же содержания.

тотальная функция «Соединить списки»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  пример «Склейка»
    дано первый равно [1]
    дано второй равно [0, 0]
    ожидается [1, 0, 0]
  свёртка второй начиная с первый как акк и эл → добавить эл к акк

тотальная функция «Сдвинуть нули»
  принимает элементы: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано элементы равно [0, 1, 0, 3, 12]
    ожидается [1, 3, 12, 0, 0]
  пример «Пример 2 из условия»
    дано элементы равно [0]
    ожидается [0]
  пусть ненулевые равно отфильтровать элементы где эл → эл не равен 0
  пусть нули равно отфильтровать элементы где эл → эл равен 0
  «Соединить списки» от ненулевые и нули
344 Обратить строку Reverse String завершение доказано списки 5/5 примеров 3/3 функций тотальны 41 строк

Условие даёт массив символов — то есть список, а список разбирается структурно. Та же операция над строкой тотальной быть не может.

flang check
модуль «Обратить строку» проходит проверку типов. Главная функция «Обратить символы» тотальна: компилятор принял доказательство завершения.
flang test
5 примеров в файле, сошлось 5, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать строку в началототальная
  • Обратить символытотальная
  • Строка из символовтотальная
examples/flang/leetcode/344-reverse-string.flang2658 байт · sha256 ae630ae685dd937a
модуль «Обратить строку»

// LeetCode 344. Reverse String.
// Условие даёт массив символов и просит обратить его на месте. Массив
// символов — это список строки, и здесь это удача: список flang разбирается
// структурно, а строка нет. Поэтому задача остаётся тотальной, тогда как
// та же операция над строкой (модуль stdlib/strings.flang) тотальной быть
// не может — по строке нельзя рекурсировать с доказательством убывания.
//
// Изменения на месте нет и не будет: значения flang неизменяемы.

тотальная функция «Приписать строку в начало»
  принимает первая: строка, элементы: список строки
  возвращает список строки
  пример «В непустой»
    дано первая равно "а"
    дано элементы равно ["б"]
    ожидается ["а", "б"]
  свёртка элементы начиная с [первая] как акк и эл → добавить эл к акк

тотальная функция «Обратить символы»
  принимает символы: список строки
  возвращает список строки
  пример «Пример 1 из условия»
    дано символы равно ["h", "e", "l", "l", "o"]
    ожидается ["o", "l", "l", "e", "h"]
  пример «Пример 2 из условия»
    дано символы равно ["H", "a", "n", "n", "a", "h"]
    ожидается ["h", "a", "n", "n", "a", "H"]
  пример «Пустой список»
    дано символы равно пустой список
    ожидается пустой список
  свёртка символы начиная с пустой список как акк и буква → «Приписать строку в начало» от буква и акк

тотальная функция «Строка из символов»
  принимает символы: список строки
  возвращает строка
  пример «Склейка»
    дано символы равно ["o", "l", "l", "e", "h"]
    ожидается "olleh"
  свёртка символы начиная с "" как акк и буква → соединить акк с буква
349 Пересечение списков Intersection of Two Arrays завершение доказано списки 3/3 примеров 2/2 функций тотальны 29 строк

Уникальные из первого, фильтр по вхождению во второй. Множеств нет, уникальность строится вручную.

flang check
модуль «Пересечение списков» проходит проверку типов. Главная функция «Пересечение» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Уникальныетотальная
  • Пересечениетотальная
examples/flang/leetcode/349-intersection-of-two-arrays.flang1642 байт · sha256 5523a0c8114257ab
модуль «Пересечение списков»

// LeetCode 349. Intersection of Two Arrays.
// Вернуть уникальные значения, встречающиеся в обоих списках.
//
// Тотальная: два прохода свёрткой и фильтром, рекурсии нет.
// Множеств в языке нет, «уникальность» строится вручную через «содержит».

тотальная функция «Уникальные»
  принимает элементы: список числа
  возвращает список числа
  пример «С повторами»
    дано элементы равно [1, 1, 2]
    ожидается [1, 2]
  свёртка элементы начиная с пустой список как акк и эл
    если акк содержит эл то акк иначе добавить эл к акк

тотальная функция «Пересечение»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано первый равно [1, 2, 2, 1]
    дано второй равно [2, 2]
    ожидается [2]
  пример «Пример 2 из условия»
    дано первый равно [4, 9, 5]
    дано второй равно [9, 4, 9, 8, 4]
    ожидается [4, 9]
  отфильтровать («Уникальные» от первый) где эл → второй содержит эл
13 Римское в число Roman to Integer доказательства нет строки 9/9 примеров 2/4 функций тотальны 94 строк

Свёртка с записью-состоянием (сумма и предыдущая цифра). Нетотальна только из-за разложения строки в список символов.

flang check
модуль «Римские числа» проходит проверку типов, объявлено типов: 1. Главная функция «Римское в число» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
9 примеров в файле, сошлось 9, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать строку в началототальная
  • Значение цифрытотальная
  • Символы с позициибез доказательства
  • Римское в числобез доказательства
examples/flang/leetcode/013-roman-to-integer.flang4973 байт · sha256 604a4018427517ef
модуль «Римские числа»

// LeetCode 13. Roman to Integer.
// Перевести римскую запись в число.
//
// Обычная, не тотальная — и виновата только строка. Сам разбор («если
// предыдущая цифра меньше текущей, вычесть её дважды») выражается свёрткой
// с записью-состоянием и тотален; но чтобы получить символы строки, её надо
// обойти по одному, а убывание «строка стала короче на символ» анализ
// завершаемости не признаёт: часть значения — это хвост списка, голова,
// поле записи или поле варианта, и ничего больше.
//
// Была бы встроенная форма «символы строки», задача стала бы тотальной
// целиком.

объект «Разбор римского»
  сумма является числом
  предыдущее является числом

тотальная функция «Приписать строку в начало»
  принимает первая: строка, элементы: список строки
  возвращает список строки
  пример «В непустой»
    дано первая равно "I"
    дано элементы равно ["V"]
    ожидается ["I", "V"]
  свёртка элементы начиная с [первая] как акк и эл → добавить эл к акк

тотальная функция «Значение цифры»
  принимает буква: строка
  возвращает число
  пример «Единица»
    дано буква равно "I"
    ожидается 1
  пример «Тысяча»
    дано буква равно "M"
    ожидается 1000
  пример «Не римская цифра»
    дано буква равно "щ"
    ожидается 0
  если буква равен "I"
    то 1
    иначе
      если буква равен "V"
        то 5
        иначе
          если буква равен "X"
            то 10
            иначе
              если буква равен "L"
                то 50
                иначе
                  если буква равен "C"
                    то 100
                    иначе
                      если буква равен "D"
                        то 500
                        иначе
                          если буква равен "M" то 1000 иначе 0

функция «Символы с позиции»
  принимает текст: строка, позиция: число
  возвращает список строки
  пример «С последнего символа»
    дано текст равно "IV"
    дано позиция равно 2
    ожидается ["V"]
  если позиция больше (длина текст)
    то пустой список
    иначе
      пусть буква равно подстрока текст с позиция по позиция
      «Приписать строку в начало» от буква и («Символы с позиции» от текст и (позиция плюс 1))

функция «Римское в число»
  принимает текст: строка
  возвращает число
  пример «Пример 1 из условия»
    дано текст равно "III"
    ожидается 3
  пример «Пример 2 из условия»
    дано текст равно "LVIII"
    ожидается 58
  пример «Пример 3 из условия»
    дано текст равно "MCMXCIV"
    ожидается 1994
  пример «Вычитание»
    дано текст равно "IV"
    ожидается 4
  пусть начальное равно запись «Разбор римского» с сумма равным 0 и предыдущее равным 0
  пусть итог равно свёртка («Символы с позиции» от текст и 1) начиная с начальное как акк и буква
    пусть значение равно «Значение цифры» от буква
    пусть поправка равно если акк.предыдущее меньше значение то (2 умножить на акк.предыдущее) иначе 0
    запись «Разбор римского» с сумма равным (акк.сумма плюс значение минус поправка) и предыдущее равным значение
  итог.сумма
14 Наибольший общий префикс Longest Common Prefix доказательства нет строки 7/7 примеров 0/3 функций тотальны 60 строк

Свёртка по словам поверх посимвольного сравнения двух слов. Сравнение идёт рекурсией по номеру позиции — её анализ убывания не принимает.

flang check
модуль «Общий префикс» проходит проверку типов. Главная функция «Наибольший общий префикс» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
7 примеров в файле, сошлось 7, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Общий префикс до позициибез доказательства
  • Общий префикс двухбез доказательства
  • Наибольший общий префиксбез доказательства
examples/flang/leetcode/014-longest-common-prefix.flang3506 байт · sha256 8a6a21d6882218db
модуль «Общий префикс»

// LeetCode 14. Longest Common Prefix.
// Найти наибольший общий начальный кусок для списка слов.
//
// Обычная. Свёртка по списку слов тотальна, а вот сравнение двух слов идёт
// по позициям — рекурсия по числу, которую анализ завершаемости не
// принимает: «позиция плюс 1» не является частью значения «позиция».
// Ни один известный приём здесь не спасает: топливо (см. задачу 704) можно
// было бы взять из списка слов, но длина слова с длиной списка не связана.

функция «Общий префикс до позиции»
  принимает первое: строка, второе: строка, позиция: число
  возвращает строка
  пример «Совпало два символа»
    дано первое равно "flower"
    дано второе равно "flow"
    дано позиция равно 1
    ожидается "flow"
  пусть предел равно если (длина первое) меньше (длина второе) то (длина первое) иначе (длина второе)
  если позиция больше предел
    то подстрока первое с 1 по предел
    иначе
      если (подстрока первое с позиция по позиция) равен (подстрока второе с позиция по позиция)
        то «Общий префикс до позиции» от первое и второе и (позиция плюс 1)
        иначе подстрока первое с 1 по (позиция минус 1)

функция «Общий префикс двух»
  принимает первое: строка, второе: строка
  возвращает строка
  пример «Общее начало»
    дано первое равно "flower"
    дано второе равно "flight"
    ожидается "fl"
  пример «Ничего общего»
    дано первое равно "dog"
    дано второе равно "racecar"
    ожидается ""
  «Общий префикс до позиции» от первое и второе и 1

функция «Наибольший общий префикс»
  принимает слова: список строки
  возвращает строка
  пример «Пример 1 из условия»
    дано слова равно ["flower", "flow", "flight"]
    ожидается "fl"
  пример «Пример 2 из условия»
    дано слова равно ["dog", "racecar", "car"]
    ожидается ""
  пример «Одно слово»
    дано слова равно ["abc"]
    ожидается "abc"
  пример «Пустой список»
    дано слова равно пустой список
    ожидается ""
  разбор слова
    случай пусто
      то ""
    случай голова и хвост
      свёртка хвост начиная с голова как акк и слово → «Общий префикс двух» от акк и слово
20 Правильные скобки Valid Parentheses доказательства нет строки 12/12 примеров 3/5 функций тотальны 99 строк

Стек живёт строкой в накопителе свёртки, поломка запоминается префиксом «!». Списочная версия тотальна, строковая — нет.

flang check
модуль «Правильные скобки» проходит проверку типов. Главная функция «Скобки в строке» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
12 примеров в файле, сошлось 12, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать строку в началототальная
  • Парная открывающаятотальная
  • Скобки в спискетотальная
  • Символы с позициибез доказательства
  • Скобки в строкебез доказательства
examples/flang/leetcode/020-valid-parentheses.flang5305 байт · sha256 12cb0b94859ab787
модуль «Правильные скобки»

// LeetCode 20. Valid Parentheses.
// Проверить, что скобки трёх видов закрываются в правильном порядке.
//
// Две функции нарочно. «Скобки в списке» принимает список символов и
// тотальна: стек живёт в накопителе свёртки (обычной строкой — стек строк
// потребовал бы отдельного типа), а свёртка конечна по построению.
// «Скобки в строке» принимает строку, как в условии, и тотальной быть не
// может: чтобы получить символы, строку надо обойти, а убывание строки
// анализ завершаемости не признаёт — «пусто» и «голова и хвост» работают
// только со списком.
//
// Прерывать свёртку нельзя, поэтому ошибка запоминается в самом стеке:
// строка, начинающаяся с «!», означает «уже сломано».

тотальная функция «Приписать строку в начало»
  принимает первая: строка, элементы: список строки
  возвращает список строки
  пример «В непустой»
    дано первая равно "а"
    дано элементы равно ["б"]
    ожидается ["а", "б"]
  свёртка элементы начиная с [первая] как акк и эл → добавить эл к акк

тотальная функция «Парная открывающая»
  принимает закрывающая: строка
  возвращает строка
  пример «Круглая»
    дано закрывающая равно ")"
    ожидается "("
  пример «Квадратная»
    дано закрывающая равно "]"
    ожидается "["
  если закрывающая равен ")"
    то "("
    иначе
      если закрывающая равен "]" то "[" иначе "{"

тотальная функция «Скобки в списке»
  принимает символы: список строки
  возвращает признак
  пример «Пример 1 из условия»
    дано символы равно ["(", ")"]
    ожидается да
  пример «Пример 2 из условия»
    дано символы равно ["(", ")", "[", "]", "{", "}"]
    ожидается да
  пример «Пример 3 из условия»
    дано символы равно ["(", "]"]
    ожидается нет
  пример «Незакрытая скобка»
    дано символы равно ["(", "["]
    ожидается нет
  пусть стек равно свёртка символы начиная с "" как акк и буква
    если акк начинается с "!"
      то акк
      иначе
        если "([{" содержит буква
          то соединить акк с буква
          иначе
            если (длина акк) равен 0
              то "!"
              иначе
                пусть верх равно подстрока акк с (длина акк) по (длина акк)
                если верх равен («Парная открывающая» от буква)
                  то подстрока акк с 1 по ((длина акк) минус 1)
                  иначе "!"
  стек равен ""

функция «Символы с позиции»
  принимает текст: строка, позиция: число
  возвращает список строки
  пример «С последнего символа»
    дано текст равно "()"
    дано позиция равно 2
    ожидается [")"]
  если позиция больше (длина текст)
    то пустой список
    иначе
      пусть буква равно подстрока текст с позиция по позиция
      «Приписать строку в начало» от буква и («Символы с позиции» от текст и (позиция плюс 1))

функция «Скобки в строке»
  принимает текст: строка
  возвращает признак
  пример «Пример 1 из условия»
    дано текст равно "()"
    ожидается да
  пример «Пример 2 из условия»
    дано текст равно "()[]{}"
    ожидается да
  пример «Пример 3 из условия»
    дано текст равно "(]"
    ожидается нет
  пример «Вложенные скобки»
    дано текст равно "{[()]}"
    ожидается да
  «Скобки в списке» от («Символы с позиции» от текст и 1)
49 Группировка анаграмм Group Anagrams завершение доказано строки 6/6 примеров 5/5 функций тотальны 70 строк

Подпись слова — свёртка по алфавиту с подсчётом через «разделить»; словарь заменён списком записей «Группа» с линейным поиском.

flang check
модуль «Группировка анаграмм» проходит проверку типов, объявлено типов: 1. Главная функция «Группировать анаграммы» тотальна: компилятор принял доказательство завершения.
flang test
6 примеров в файле, сошлось 6, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Счёт буквытотальная
  • Подписьтотальная
  • Есть группатотальная
  • Добавить словототальная
  • Группировать анаграммытотальная
examples/flang/leetcode/049-group-anagrams.flang4499 байт · sha256 3aab7957b768667b
модуль «Группировка анаграмм»

// LeetCode 49. Group Anagrams.
// Разложить слова по группам: в одной группе — слова из одних и тех же букв.
//
// Тотальная. Каноническое решение — словарь «подпись → список слов», а
// ассоциативных массивов в языке нет. Замена: список записей «Группа» и
// линейный поиск по ключу. Подпись слова тоже строится без обхода символов —
// свёрткой по алфавиту с подсчётом через «разделить» (тот же приём, что в
// задаче 242). Порядок групп — порядок первого появления.
//
// Цена отсутствия словаря: O(слов × групп × 26) вместо O(суммарной длины).

объект «Группа»
  ключ является строкой
  слова является список строки

тотальная функция «Счёт буквы»
  принимает текст: строка, буква: строка
  возвращает число
  пример «Две буквы a»
    дано текст равно "abac"
    дано буква равно "a"
    ожидается 2
  (длина (разделить текст по буква)) минус 1

тотальная функция «Подпись»
  принимает слово: строка
  возвращает строка
  пример «Анаграммы дают одну подпись»
    дано слово равно "eat"
    ожидается "1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,"
  пример «Другое слово — другая подпись»
    дано слово равно "bat"
    ожидается "1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,"
  свёртка ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z"] начиная с "" как акк и буква
    соединить (соединить акк с (к строке («Счёт буквы» от слово и буква))) с ","

тотальная функция «Есть группа»
  принимает группы: список «Группа», ключ: строка
  возвращает признак
  свёртка группы начиная с нет как акк и группа
    если акк равен да то да иначе группа.ключ равен ключ

тотальная функция «Добавить слово»
  принимает группы: список «Группа», ключ: строка, слово: строка
  возвращает список «Группа»
  если «Есть группа» от группы и ключ
    то
      отобразить группы как группа
        если группа.ключ равен ключ
          то запись «Группа» с ключ равным ключ и слова равным (добавить слово к группа.слова)
          иначе группа
    иначе добавить (запись «Группа» с ключ равным ключ и слова равным [слово]) к группы

тотальная функция «Группировать анаграммы»
  принимает слова: список строки
  возвращает список список строки
  пример «Пример 1 из условия»
    дано слова равно ["eat", "tea", "tan", "ate", "nat", "bat"]
    ожидается [["eat", "tea", "ate"], ["tan", "nat"], ["bat"]]
  пример «Пример 2 из условия»
    дано слова равно [""]
    ожидается [[""]]
  пример «Пример 3 из условия»
    дано слова равно ["a"]
    ожидается [["a"]]
  пусть группы равно свёртка слова начиная с пустой список как акк и слово
    «Добавить слово» от акк и («Подпись» от слово) и слово
  отобразить группы как группа → группа.слова
125 Палиндром Valid Palindrome доказательства нет строки 12/12 примеров 3/7 функций тотальны 98 строк

Нижний регистр — таблицей из двух алфавитов: встроенной формы «код символа» нет. Нетотальна из-за обхода символов; кириллица решением не покрыта.

flang check
модуль «Палиндром» проходит проверку типов. Главная функция «Палиндром» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
12 примеров в файле, сошлось 12, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Приписать строку в началототальная
  • Позиция подстрокитотальная
  • Значащий символтотальная
  • Символы с позициибез доказательства
  • Очиститьбез доказательства
  • Обратить строкубез доказательства
  • Палиндромбез доказательства
examples/flang/leetcode/125-valid-palindrome.flang5382 байт · sha256 32d4e4edd19b9034
модуль «Палиндром»

// LeetCode 125. Valid Palindrome.
// Строка считается палиндромом, если после выбрасывания всего, кроме букв и
// цифр, и приведения к нижнему регистру она читается одинаково в обе стороны.
//
// Обычная. Причина та же, что у остальных строковых задач: чтобы пройти по
// символам, нужна рекурсия по строке, а её анализ завершаемости не признаёт.
// Заметно и второе ограничение: нижний регистр приходится делать таблицей
// из двух алфавитов — встроенной формы «код символа» в языке нет, поэтому
// связать «A» и «a» иначе нечем. Кириллица этим решением не покрыта.

тотальная функция «Приписать строку в начало»
  принимает первая: строка, элементы: список строки
  возвращает список строки
  пример «В непустой»
    дано первая равно "a"
    дано элементы равно ["b"]
    ожидается ["a", "b"]
  свёртка элементы начиная с [первая] как акк и эл → добавить эл к акк

тотальная функция «Позиция подстроки»
  принимает текст: строка, часть: строка
  возвращает число
  пример «В середине»
    дано текст равно "abcd"
    дано часть равно "c"
    ожидается 3
  пример «Нет вхождения»
    дано текст равно "abc"
    дано часть равно "z"
    ожидается 0
  если текст содержит часть
    то (длина (голова (разделить текст по часть))) плюс 1
    иначе 0

тотальная функция «Значащий символ»
  принимает буква: строка
  возвращает строка
  пример «Заглавная становится строчной»
    дано буква равно "P"
    ожидается "p"
  пример «Цифра остаётся»
    дано буква равно "7"
    ожидается "7"
  пример «Знак препинания выбрасывается»
    дано буква равно ","
    ожидается ""
  пусть позиция равно «Позиция подстроки» от "ABCDEFGHIJKLMNOPQRSTUVWXYZ" и буква
  если позиция больше 0
    то подстрока "abcdefghijklmnopqrstuvwxyz" с позиция по позиция
    иначе
      если "abcdefghijklmnopqrstuvwxyz0123456789" содержит буква то буква иначе ""

функция «Символы с позиции»
  принимает текст: строка, позиция: число
  возвращает список строки
  пример «С последнего символа»
    дано текст равно "ab"
    дано позиция равно 2
    ожидается ["b"]
  если позиция больше (длина текст)
    то пустой список
    иначе
      пусть буква равно подстрока текст с позиция по позиция
      «Приписать строку в начало» от буква и («Символы с позиции» от текст и (позиция плюс 1))

функция «Очистить»
  принимает текст: строка
  возвращает строка
  пример «Знаки и регистр»
    дано текст равно "A man, a plan"
    ожидается "amanaplan"
  свёртка («Символы с позиции» от текст и 1) начиная с "" как акк и буква
    соединить акк с («Значащий символ» от буква)

функция «Обратить строку»
  принимает текст: строка
  возвращает строка
  пример «Слово»
    дано текст равно "abc"
    ожидается "cba"
  свёртка («Символы с позиции» от текст и 1) начиная с "" как акк и буква → соединить буква с акк

функция «Палиндром»
  принимает текст: строка
  возвращает признак
  пример «Пример 1 из условия»
    дано текст равно "A man, a plan, a canal: Panama"
    ожидается да
  пример «Пример 2 из условия»
    дано текст равно "race a car"
    ожидается нет
  пример «Пример 3 из условия»
    дано текст равно " "
    ожидается да
  пусть чистое равно «Очистить» от текст
  чистое равен («Обратить строку» от чистое)
242 Анаграмма Valid Anagram завершение доказано строки 5/5 примеров 2/2 функций тотальны 47 строк

Тотальная задача про строки: счёт буквы = число частей «разделить» минус один, перебор идёт по литеральному алфавиту из 26 букв, а не по символам слова.

flang check
модуль «Анаграмма» проходит проверку типов. Главная функция «Анаграмма» тотальна: компилятор принял доказательство завершения.
flang test
5 примеров в файле, сошлось 5, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Счёт буквытотальная
  • Анаграмматотальная
examples/flang/leetcode/242-valid-anagram.flang2622 байт · sha256 af1a5f7701a87e60
модуль «Анаграмма»

// LeetCode 242. Valid Anagram.
// Проверить, что второе слово — перестановка первого. По условию буквы
// только строчные латинские.
//
// Тотальная — и это неожиданно, потому что задача про строки. Приём:
// считать буквы не обходом строки, а встроенной «разделить». Число вхождений
// буквы равно числу частей минус один, а перебирать надо не символы слова,
// а заранее известный алфавит из 26 букв — конечный список, записанный
// литералом. Свёртка по литеральному списку тотальна всегда.

тотальная функция «Счёт буквы»
  принимает текст: строка, буква: строка
  возвращает число
  пример «Две буквы a»
    дано текст равно "abac"
    дано буква равно "a"
    ожидается 2
  пример «Буквы нет»
    дано текст равно "bbb"
    дано буква равно "a"
    ожидается 0
  (длина (разделить текст по буква)) минус 1

тотальная функция «Анаграмма»
  принимает первое: строка, второе: строка
  возвращает признак
  пример «Пример 1 из условия»
    дано первое равно "anagram"
    дано второе равно "nagaram"
    ожидается да
  пример «Пример 2 из условия»
    дано первое равно "rat"
    дано второе равно "car"
    ожидается нет
  пример «Разная длина»
    дано первое равно "a"
    дано второе равно "ab"
    ожидается нет
  если (длина первое) не равен (длина второе)
    то нет
    иначе
      свёртка ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z"] начиная с да как акк и буква
        если акк равен нет
          то нет
          иначе («Счёт буквы» от первое и буква) равен («Счёт буквы» от второе и буква)
53 Максимальная подпоследовательность Maximum Subarray завершение доказано динамика 4/4 примеров 1/1 функций тотальны 41 строк

Кадане: состояние из двух чисел укладывается в запись, запись — в накопитель свёртки. Единственная динамика, которая ложится на язык без сопротивления.

flang check
модуль «Максимальная подпоследовательность» проходит проверку типов, объявлено типов: 1. Главная функция «Наибольшая сумма куска» тотальна: компилятор принял доказательство завершения.
flang test
4 примеров в файле, сошлось 4, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Наибольшая сумма кускатотальная
examples/flang/leetcode/053-maximum-subarray.flang2740 байт · sha256 914be0f166ec0690
модуль «Максимальная подпоследовательность»

// LeetCode 53. Maximum Subarray.
// Найти наибольшую сумму непрерывного куска списка (алгоритм Кадане).
//
// Тотальная. Это самая «динамическая» из задач, которые язык принимает без
// сопротивления: состояние Кадане — два числа, а два числа складываются в
// запись, и запись отлично живёт накопителем свёртки. Настоящая динамика
// с таблицей (Coin Change, Edit Distance) так не переносится — там нужен
// массив с произвольным доступом по индексу, которого в языке нет.

объект «Состояние Кадане»
  текущая является числом
  лучшая является числом

тотальная функция «Наибольшая сумма куска»
  принимает элементы: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [-2, 1, -3, 4, -1, 2, 1, -5, 4]
    ожидается 6
  пример «Пример 2 из условия»
    дано элементы равно [1]
    ожидается 1
  пример «Пример 3 из условия»
    дано элементы равно [5, 4, -1, 7, 8]
    ожидается 23
  пример «Пустой список»
    дано элементы равно пустой список
    ожидается 0
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      пусть начальное равно запись «Состояние Кадане» с текущая равным голова и лучшая равным голова
      пусть итог равно свёртка хвост начиная с начальное как акк и эл
        пусть продолженная равно акк.текущая плюс эл
        пусть текущая равно если продолженная больше эл то продолженная иначе эл
        пусть лучшая равно если текущая больше акк.лучшая то текущая иначе акк.лучшая
        запись «Состояние Кадане» с текущая равным текущая и лучшая равным лучшая
      итог.лучшая
70 Ступени Climbing Stairs доказательства нет динамика 5/5 примеров 0/2 функций тотальны 45 строк

Линейный проход с двумя накопителями. Нетотальна: счётчик «осталось минус 1» — результат арифметики, а не часть значения.

flang check
модуль «Ступени» проходит проверку типов. Главная функция «Ступени» не тотальна: убывание не доказано, конечность держится на входных данных.
flang test
5 примеров в файле, сошлось 5, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Ступени шагомбез доказательства
  • Ступенибез доказательства
examples/flang/leetcode/070-climbing-stairs.flang2441 байт · sha256 f96bbfdf4c77750f
модуль «Ступени»

// LeetCode 70. Climbing Stairs.
// Сколькими способами подняться на n ступеней шагами по одной и по две.
//
// Обычная. Ответ — число Фибоначчи, и считается он за один проход с двумя
// накопителями; тотальной функция всё равно не становится, потому что
// «осталось минус 1» не является частью значения «осталось». Это та же
// граница, что в модуле stdlib/numbers.flang: рекурсия по числу анализу
// недоступна в принципе, ей нужна мера, а мер он не знает.
//
// Обход существует: передать список из n элементов и рекурсировать по нему.
// Но список из n элементов сам по себе строится рекурсией по n — то есть
// обычной функцией, и тотальность не спасена, а лишь передвинута.

функция «Ступени шагом»
  принимает осталось: число, предыдущее: число, текущее: число
  возвращает число
  пример «Один шаг»
    дано осталось равно 1
    дано предыдущее равно 1
    дано текущее равно 1
    ожидается 2
  если осталось не больше 0
    то текущее
    иначе «Ступени шагом» от (осталось минус 1) и текущее и (предыдущее плюс текущее)

функция «Ступени»
  принимает н: число
  возвращает число
  пример «Пример 1 из условия»
    дано н равно 2
    ожидается 2
  пример «Пример 2 из условия»
    дано н равно 3
    ожидается 3
  пример «Одна ступень»
    дано н равно 1
    ожидается 1
  пример «Десять ступеней»
    дано н равно 10
    ожидается 89
  если н не больше 1
    то 1
    иначе «Ступени шагом» от (н минус 1) и 1 и 1
121 Лучшая сделка Best Time to Buy and Sell Stock завершение доказано динамика 3/3 примеров 1/1 функций тотальны 36 строк

Один проход свёрткой, состояние — запись «минимальная цена, лучшая прибыль».

flang check
модуль «Лучшая сделка» проходит проверку типов, объявлено типов: 1. Главная функция «Лучшая прибыль» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Лучшая прибыльтотальная
examples/flang/leetcode/121-best-time-to-buy-and-sell-stock.flang2118 байт · sha256 0cdee4c952c344b5
модуль «Лучшая сделка»

// LeetCode 121. Best Time to Buy and Sell Stock.
// По списку цен по дням найти наибольшую прибыль от одной покупки и одной
// последующей продажи. Если прибыли нет — ноль.
//
// Тотальная: один проход свёрткой, состояние — запись из двух чисел
// (минимальная цена и лучшая прибыль).

объект «Сделка»
  минимум является числом
  прибыль является числом

тотальная функция «Лучшая прибыль»
  принимает цены: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано цены равно [7, 1, 5, 3, 6, 4]
    ожидается 5
  пример «Пример 2 из условия»
    дано цены равно [7, 6, 4, 3, 1]
    ожидается 0
  пример «Пустой список»
    дано цены равно пустой список
    ожидается 0
  разбор цены
    случай пусто
      то 0
    случай голова и хвост
      пусть начальное равно запись «Сделка» с минимум равным голова и прибыль равным 0
      пусть итог равно свёртка хвост начиная с начальное как акк и цена
        пусть минимум равно если цена меньше акк.минимум то цена иначе акк.минимум
        пусть сегодня равно цена минус акк.минимум
        пусть прибыль равно если сегодня больше акк.прибыль то сегодня иначе акк.прибыль
        запись «Сделка» с минимум равным минимум и прибыль равным прибыль
      итог.прибыль
110 Сбалансированное дерево Balanced Binary Tree завершение доказано деревья 3/3 примеров 5/5 функций тотальны 76 строк

Конъюнкция трёх условий записана вложенными «если»: логических «и» и «или» в языке нет.

flang check
модуль «Сбалансированное дерево» проходит проверку типов, объявлено типов: 1. Главная функция «Сбалансировано для списка» тотальна: компилятор принял доказательство завершения.
flang test
3 примеров в файле, сошлось 3, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Вставить в деревототальная
  • Дерево из спискатотальная
  • Глубинатотальная
  • Сбалансированототальная
  • Сбалансировано для спискатотальная
examples/flang/leetcode/110-balanced-binary-tree.flang4385 байт · sha256 2f753c379df468ba
модуль «Сбалансированное дерево»

// LeetCode 110. Balanced Binary Tree.
// Проверить, что для каждого узла глубины поддеревьев отличаются не более
// чем на единицу.
//
// Тотальная. Логических «и» и «или» в языке нет (SPEC перечисляет только
// арифметику и сравнения), поэтому конъюнкция трёх условий записана
// вложенными «если» — читается длиннее, но означает ровно то же.

тип «Дерево»
  вариант Лист
  вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»

тотальная функция «Вставить в дерево»
  принимает дерево: «Дерево», число: число
  возвращает «Дерево»
  разбор дерева
    случай Лист
      то Узел с значение равным число и левое равным вариант Лист и правое равным вариант Лист
    случай вариант Узел с значение как зн и левое как л и правое как п
      если число меньше зн
        то
          пусть новое равно «Вставить в дерево» от л и число
          Узел с значение равным зн и левое равным новое и правое равным п
        иначе
          пусть новое равно «Вставить в дерево» от п и число
          Узел с значение равным зн и левое равным л и правое равным новое

тотальная функция «Дерево из списка»
  принимает элементы: список числа
  возвращает «Дерево»
  свёртка элементы начиная с вариант Лист как акк и эл → «Вставить в дерево» от акк и эл

тотальная функция «Глубина»
  принимает дерево: «Дерево»
  возвращает число
  разбор дерева
    случай Лист
      то 0
    случай вариант Узел с левое как л и правое как п
      пусть слева равно «Глубина» от л
      пусть справа равно «Глубина» от п
      1 плюс (если слева больше справа то слева иначе справа)

тотальная функция «Сбалансировано»
  принимает дерево: «Дерево»
  возвращает признак
  разбор дерева
    случай Лист
      то да
    случай вариант Узел с левое как л и правое как п
      если («Сбалансировано» от л) равен нет
        то нет
        иначе
          если («Сбалансировано» от п) равен нет
            то нет
            иначе
              пусть разница равно («Глубина» от л) минус («Глубина» от п)
              если разница меньше 0
                то (0 минус разница) не больше 1
                иначе разница не больше 1

тотальная функция «Сбалансировано для списка»
  принимает элементы: список числа
  возвращает признак
  пример «Сбалансированное дерево»
    дано элементы равно [2, 1, 3]
    ожидается да
  пример «Цепочка не сбалансирована»
    дано элементы равно [1, 2, 3, 4]
    ожидается нет
  пример «Пустое дерево сбалансировано»
    дано элементы равно пустой список
    ожидается да
  «Сбалансировано» от («Дерево из списка» от элементы)
226 Развернуть дерево Invert Binary Tree завершение доказано деревья 5/5 примеров 7/7 функций тотальны 88 строк

Само «Развернуть» примера иметь не может — оно возвращает вариант. Проверяется наблюдаемое следствие: обход по порядку до и после разворота.

flang check
модуль «Развернуть дерево» проходит проверку типов, объявлено типов: 1. Главная функция «Обход после разворота» тотальна: компилятор принял доказательство завершения.
flang test
5 примеров в файле, сошлось 5, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Соединить спискитотальная
  • Вставить в деревототальная
  • Дерево из спискатотальная
  • Развернутьтотальная
  • Обход по порядкутотальная
  • Обход дерева из спискатотальная
  • Обход после разворотатотальная
examples/flang/leetcode/226-invert-binary-tree.flang5578 байт · sha256 0e9b6530589aa7e5
модуль «Развернуть дерево»

// LeetCode 226. Invert Binary Tree.
// Поменять местами левое и правое поддерево у каждого узла.
//
// Тотальная. Само «Развернуть» примера иметь не может: оно возвращает
// вариант, а значение варианта в «ожидается» не записывается — парсер
// разворачивает конструктор в запись из его полей и теряет имя варианта.
// Поэтому проверяется наблюдаемое следствие: обход по возрастанию до и после
// разворота. У дерева поиска обход по порядку отсортирован, у развёрнутого —
// отсортирован в обратную сторону.

тип «Дерево»
  вариант Лист
  вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»

тотальная функция «Соединить списки»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  пример «Склейка»
    дано первый равно [1]
    дано второй равно [2, 3]
    ожидается [1, 2, 3]
  свёртка второй начиная с первый как акк и эл → добавить эл к акк

тотальная функция «Вставить в дерево»
  принимает дерево: «Дерево», число: число
  возвращает «Дерево»
  разбор дерева
    случай Лист
      то Узел с значение равным число и левое равным вариант Лист и правое равным вариант Лист
    случай вариант Узел с значение как зн и левое как л и правое как п
      если число меньше зн
        то
          пусть новое равно «Вставить в дерево» от л и число
          Узел с значение равным зн и левое равным новое и правое равным п
        иначе
          пусть новое равно «Вставить в дерево» от п и число
          Узел с значение равным зн и левое равным л и правое равным новое

тотальная функция «Дерево из списка»
  принимает элементы: список числа
  возвращает «Дерево»
  свёртка элементы начиная с вариант Лист как акк и эл → «Вставить в дерево» от акк и эл

тотальная функция «Развернуть»
  принимает дерево: «Дерево»
  возвращает «Дерево»
  разбор дерева
    случай Лист
      то вариант Лист
    случай вариант Узел с значение как зн и левое как л и правое как п
      пусть слева равно «Развернуть» от п
      пусть справа равно «Развернуть» от л
      Узел с значение равным зн и левое равным слева и правое равным справа

тотальная функция «Обход по порядку»
  принимает дерево: «Дерево»
  возвращает список числа
  разбор дерева
    случай Лист
      то пустой список
    случай вариант Узел с значение как зн и левое как л и правое как п
      пусть слева равно «Обход по порядку» от л
      пусть справа равно «Обход по порядку» от п
      «Соединить списки» от (добавить зн к слева) и справа

тотальная функция «Обход дерева из списка»
  принимает элементы: список числа
  возвращает список числа
  пример «Дерево поиска обходится по возрастанию»
    дано элементы равно [4, 2, 7, 1, 3, 6, 9]
    ожидается [1, 2, 3, 4, 6, 7, 9]
  «Обход по порядку» от («Дерево из списка» от элементы)

тотальная функция «Обход после разворота»
  принимает элементы: список числа
  возвращает список числа
  пример «Пример 1 из условия»
    дано элементы равно [4, 2, 7, 1, 3, 6, 9]
    ожидается [9, 7, 6, 4, 3, 2, 1]
  пример «Пример 2 из условия»
    дано элементы равно [2, 1, 3]
    ожидается [3, 2, 1]
  пример «Пустое дерево»
    дано элементы равно пустой список
    ожидается пустой список
  «Обход по порядку» от («Развернуть» от («Дерево из списка» от элементы))
704 Двоичный поиск Binary Search завершение доказано поиск 5/5 примеров 3/3 функций тотальны 75 строк

Приём «топливо»: рядом с настоящими аргументами едет список, у которого на каждом шаге берётся хвост. Топливо убывает структурно, значит цикл доказуемо конечен.

flang check
модуль «Двоичный поиск» проходит проверку типов. Главная функция «Двоичный поиск» тотальна: компилятор принял доказательство завершения.
flang test
5 примеров в файле, сошлось 5, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Элементтотальная
  • Поиск в диапазонетотальная
  • Двоичный поисктотальная
examples/flang/leetcode/704-binary-search.flang4309 байт · sha256 631cb89f7a5336ab
модуль «Двоичный поиск»

// LeetCode 704. Binary Search.
// В отсортированном списке найти номер цели (с нуля) или −1.
//
// Тотальная — но приёмом, который стоит запомнить, потому что он показывает
// границу анализа завершаемости. Двоичный поиск сужает пару чисел «низ» и
// «верх», а убывание по числам totality.mjs не признаёт: «середина плюс 1» —
// результат арифметики, а не часть значения. Прямая запись даёт
// FLANG_NOT_TOTAL.
//
// Обход: рядом с настоящими аргументами едет «топливо» — список, у которого
// на каждом шаге берётся хвост. Топливо убывает структурно, значит цикл
// доказуемо конечен; а поскольку топливом служит сам список, шагов заведомо
// хватает (их нужно log₂n, а есть n). Приём честный, но это именно приём:
// в языке не хватает убывания по мере.

тотальная функция «Элемент»
  принимает элементы: список числа, номер: число
  возвращает число
  пример «Второй элемент»
    дано элементы равно [10, 20, 30]
    дано номер равно 2
    ожидается 20
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      если номер не больше 1
        то голова
        иначе «Элемент» от хвост и (номер минус 1)

тотальная функция «Поиск в диапазоне»
  принимает топливо: список числа, элементы: список числа, цель: число, низ: число, верх: число
  возвращает число
  пример «Нашли середину»
    дано топливо равно [1, 2, 3]
    дано элементы равно [1, 2, 3]
    дано цель равно 2
    дано низ равно 1
    дано верх равно 3
    ожидается 1
  разбор топливо
    случай пусто
      то -1
    случай голова и хвост
      если низ больше верх
        то -1
        иначе
          пусть сумма равно низ плюс верх
          пусть середина равно (сумма минус (сумма остаток от 2)) делить на 2
          пусть значение равно «Элемент» от элементы и середина
          если значение равен цель
            то середина минус 1
            иначе
              если значение меньше цель
                то «Поиск в диапазоне» от хвост и элементы и цель и (середина плюс 1) и верх
                иначе «Поиск в диапазоне» от хвост и элементы и цель и низ и (середина минус 1)

тотальная функция «Двоичный поиск»
  принимает элементы: список числа, цель: число
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [-1, 0, 3, 5, 9, 12]
    дано цель равно 9
    ожидается 4
  пример «Пример 2 из условия»
    дано элементы равно [-1, 0, 3, 5, 9, 12]
    дано цель равно 2
    ожидается -1
  пример «Один элемент»
    дано элементы равно [5]
    дано цель равно 5
    ожидается 0
  «Поиск в диапазоне» от элементы и элементы и цель и 1 и (длина элементы)
268 Пропущенное число Missing Number завершение доказано числа 4/4 примеров 2/2 функций тотальны 32 строк

Сумма прогрессии минус сумма списка. Единственная задача набора, где язык не мешает ничем.

flang check
модуль «Пропущенное число» проходит проверку типов. Главная функция «Пропущенное число» тотальна: компилятор принял доказательство завершения.
flang test
4 примеров в файле, сошлось 4, разошлось 0. Примеры — часть исходника, а не отдельный тестовый файл.
  • Сумматотальная
  • Пропущенное числототальная
examples/flang/leetcode/268-missing-number.flang1703 байт · sha256 d3b27a7b0110e525
модуль «Пропущенное число»

// LeetCode 268. Missing Number.
// В списке лежат все числа от 0 до n, кроме одного. Найти пропущенное.
//
// Тотальная и без рекурсии: сумма арифметической прогрессии минус сумма
// списка. Здесь язык не мешает вовсе — вся задача выражается двумя свёртками
// и арифметикой.

тотальная функция «Сумма»
  принимает элементы: список числа
  возвращает число
  пример «Сумма трёх»
    дано элементы равно [1, 2, 3]
    ожидается 6
  свёртка элементы начиная с 0 как акк и эл → акк плюс эл

тотальная функция «Пропущенное число»
  принимает элементы: список числа
  возвращает число
  пример «Пример 1 из условия»
    дано элементы равно [3, 0, 1]
    ожидается 2
  пример «Пример 2 из условия»
    дано элементы равно [0, 1]
    ожидается 2
  пример «Пример 3 из условия»
    дано элементы равно [9, 6, 4, 2, 3, 5, 7, 0, 1]
    ожидается 8
  пусть предел равно длина элементы
  пусть полная равно (предел умножить на (предел плюс 1)) делить на 2
  полная минус («Сумма» от элементы)

Рабочие примеры

Сервис, допуск агента, кодогенерация, форма и готовый CI.

Файлы лежат в репозитории курса, покрыты тестами и запускаются одной командой: npm run fts:examples. Ниже их настоящее содержимое.

Скидка как HTTP-сервис

Node.js отвечает за сокет и коды ответа, FTS — за правило. Примеры модели выполняются на старте: не прошёл предметный тест — сервис не поднялся.

Запуск
npm run fts:api
Проверка
node --test examples/fts/discount-api/server.test.mjs
examples/fts/discount-api/server.mjs
/**
 * HTTP-сервис расчёта скидки поверх FTS.
 *
 * Разделение ответственности, ради которого всё и затевалось:
 *   — FTS отвечает за бизнес-правило (какая скидка положена);
 *   — Node.js отвечает за эффекты (сокет, маршруты, коды ответа, лимит тела).
 *
 * Примеры из модели выполняются на старте: если предметный тест не проходит,
 * сервис не поднимается вообще. Правило, которое не проходит собственные
 * примеры, до продакшена не доезжает.
 *
 * Запуск:  node examples/fts/discount-api/server.mjs
 * Проверка: curl -s localhost:8788/discount -d '{"сумма":20000,"постоянный клиент":true}'
 */
import { createServer } from 'node:http';
import { readFile } from 'node:fs/promises';
import { fileURLToPath, pathToFileURL } from 'node:url';
import { resolve } from 'node:path';

import { assertValid, compile, executeUtility, testUtilities } from '../../../static/js/vendor/fts/browser.js';

const here = fileURLToPath(new URL('.', import.meta.url));
export const MODEL_FILE = resolve(here, '../../../static/fts/models/order-discount.fts');
const UTILITY = 'Рассчитать скидку';
const MAX_BODY = 64 * 1024;

export async function createCalculator(modelFile = MODEL_FILE) {
  const document = assertValid(compile(await readFile(modelFile, 'utf8')));
  const tests = testUtilities(document);
  if (!tests.valid) {
    const failed = tests.results.filter((result) => !result.passed);
    throw new Error(
      `FTS-примеры не прошли (${failed.length} из ${tests.total}): ` +
        failed.map((result) => `«${result.example}» ожидалось ${result.expected}, получено ${result.actual}`).join('; '),
    );
  }
  return { document, tests, calculate: (purchase) => executeUtility(document, UTILITY, purchase) };
}

export async function createDiscountServer(modelFile = MODEL_FILE) {
  const { calculate, tests, document } = await createCalculator(modelFile);
  const fields = document.structures.find((structure) => structure.name === 'Покупка').fields;

  return createServer(async (request, response) => {
    try {
      if (request.method === 'GET' && request.url === '/health') {
        return send(response, 200, { ok: true, model: document.category, examples: `${tests.passed}/${tests.total}` });
      }
      if (request.method === 'GET' && request.url === '/contract') {
        return send(response, 200, { utility: UTILITY, input: fields, output: 'Деньги' });
      }
      if (request.method !== 'POST' || request.url !== '/discount') {
        return send(response, 404, { error: 'используйте POST /discount' });
      }
      const purchase = JSON.parse(await readBody(request));
      return send(response, 200, { discount: calculate(purchase) });
    } catch (error) {
      /* Нарушенное свойство и неизвестное поле — это ошибка запроса, а не сбой
         сервиса: клиенту возвращается причина, диагностика FTS не теряется. */
      return send(response, 400, {
        error: error instanceof Error ? error.message : String(error),
        diagnostics: error?.diagnostics ?? [],
      });
    }
  });
}

async function readBody(request) {
  const chunks = [];
  let size = 0;
  for await (const chunk of request) {
    size += chunk.length;
    if (size > MAX_BODY) throw new Error('тело запроса больше 64 КБ');
    chunks.push(chunk);
  }
  return Buffer.concat(chunks).toString('utf8');
}

function send(response, status, body) {
  response.writeHead(status, { 'content-type': 'application/json; charset=utf-8' });
  response.end(`${JSON.stringify(body, null, 2)}\n`);
}

if (process.argv[1] && import.meta.url === pathToFileURL(process.argv[1]).href) {
  const port = Number.parseInt(process.env.FTS_HTTP_PORT ?? '8788', 10);
  const server = await createDiscountServer();
  server.listen(port, '127.0.0.1', () => {
    process.stdout.write(`Discount API: http://127.0.0.1:${port} (POST /discount, GET /contract, GET /health)\n`);
  });
}
Ответ на неверный тип входа400 · FTS_UTILITY_INPUT_TYPEне 500

Агент предлагает, движок решает

Модель формулирует утверждение на FTS, а допуск команды выдаёт доказательство на реальных данных заказа. Убедительность текста здесь ничего не решает.

Разрешено
node examples/fts/shipment-guard/guard.mjs ЗК-7781
Отклонено
… ЗК-7781 --blocked, код выхода 1
examples/fts/shipment-guard/guard.mjs
/**
 * Допуск команды «отгрузить заказ» через доказательство на реальных данных.
 *
 * Это шаблон для агентских сценариев: модель (или человек) формулирует
 * утверждение на FTS, а решение принимает не текст ответа, а движок. Если факт
 * в данных не подтверждается, prove() отклоняет теорему и команда не выполняется.
 * Эффект (реальная отгрузка) живёт снаружи и вызывается только после allow.
 *
 * Запуск: node examples/fts/shipment-guard/guard.mjs ЗК-7781
 *         node examples/fts/shipment-guard/guard.mjs ЗК-7781 --blocked
 */
import { readFile } from 'node:fs/promises';
import { fileURLToPath, pathToFileURL } from 'node:url';
import { resolve } from 'node:path';

import { compile, prove } from '../../../static/js/vendor/fts/browser.js';

const here = fileURLToPath(new URL('.', import.meta.url));
const models = resolve(here, '../../../static/fts/models');

/* Кавычки внутри имени сломали бы разбор, поэтому номер заказа проверяется
   до подстановки: в теорему попадают только допустимые идентификаторы. */
const ORDER_NUMBER = /^[\p{L}\p{N}-]{1,32}$/u;

export function shipmentTheorem(orderNumber) {
  if (!ORDER_NUMBER.test(orderNumber)) throw new Error(`недопустимый номер заказа: ${orderNumber}`);
  return `категория «Исполнение заказа»

  объект Заказ
    номер является строкой
    клиент является строкой
    оплачен является признаком
    «склад подтвердил» является признаком
    «готов к отгрузке» является состоянием «Готов к отгрузке»

  морфизм «Готовый заказ можно отгрузить»
    если «Готов к отгрузке»
    то «Отгрузить заказ разрешено»

  теорема «Заказ ${orderNumber} можно отгрузить»
    дано Заказ имеет «готов к отгрузке» равное да
    в данных заказы найти где номер равен «${orderNumber}»
    по морфизму «Готовый заказ можно отгрузить»
    следовательно «Отгрузить заказ разрешено»
`;
}

export function decideShipment(orderNumber, context) {
  const source = shipmentTheorem(orderNumber);
  try {
    const proof = prove(compile(source), context);
    return { allowed: true, source, proof };
  } catch (error) {
    return {
      allowed: false,
      source,
      reason: error instanceof Error ? error.message : String(error),
      diagnostics: error?.diagnostics ?? [],
    };
  }
}

export async function loadContext(blocked = false) {
  const file = resolve(models, blocked ? 'order-shipment.blocked.context.json' : 'order-shipment.context.json');
  return JSON.parse(await readFile(file, 'utf8'));
}

if (process.argv[1] && import.meta.url === pathToFileURL(process.argv[1]).href) {
  const orderNumber = process.argv[2] ?? 'ЗК-7781';
  const decision = decideShipment(orderNumber, await loadContext(process.argv.includes('--blocked')));
  process.stdout.write(`${JSON.stringify(decision, null, 2)}\n`);
  /* Ненулевой код возврата делает guard пригодным для shell и CI. */
  process.exit(decision.allowed ? 0 : 1);
}
Причина отказаFTS_WITNESS_MISMATCHсклад не подтвердил

Сгенерированный код не расходится с моделью

Из модели получаются реализация и тесты на node:test. Режим --check роняет сборку, если правило поправили в TypeScript мимо модели.

Сгенерировать
node examples/fts/typescript-codegen/generate.mjs
Сверить
… generate.mjs --check
examples/fts/typescript-codegen/generated/fts.utilities.ts
// Generated by FTS. Do not edit by hand.

export interface FtsInput0 {
  "сумма": number
  "постоянный клиент": boolean
}

export const ftsUtilities = {
  "Рассчитать скидку": (input: FtsInput0): number => {
    let result: number = 0
    if (input["сумма"] >= 10000 && input["сумма"] <= 100000) {
      result += (10 / 100) * input["сумма"]
    }
    if (input["постоянный клиент"] === true && input["сумма"] > 0 && input["сумма"] <= 100000) {
      result += (5 / 100) * input["сумма"]
    }
    if (input["сумма"] > 100000) {
      result += 15000
    }
    if (!(result <= 15000)) throw new Error("Нарушено свойство «Скидка ограничена»")
    return result
  },
} as const
Из того же файлаfts.utilities.test.ts3 предметных теста

Форма знает поля, потому что их объявила модель

Схема формы выводится из объекта FTS: контрол, тип, обязательность. Компонент React не дублирует контракт, который уже проверяет бэкенд.

Схема
node examples/fts/form-schema/schema.mjs Покупка
Необязательность
иногда является отображается в required: false
examples/fts/react-form/DiscountForm.jsx
/**
 * Форма скидки на React.
 *
 * Компонент не знает, что покупка состоит из суммы и признака постоянного
 * клиента: поля приходят из той же FTS-модели, которую проверяет бэкенд.
 * Добавили в модель поле — форма получила контрол без правки JSX.
 *
 * Предпросчёт скидки выполняется прямо в браузере тем же компилятором, поэтому
 * пользователь видит результат без сетевого запроса. Сервер всё равно считает
 * заново: браузеру доверять нельзя, но и ждать его не нужно.
 */
import { useMemo, useState } from 'react';
import { compile, executeUtility } from '@digitable-lol/fts/browser';

import { ftsFormSchema } from '../form-schema/schema.mjs';

export function DiscountForm({ source, objectName = 'Покупка', utility = 'Рассчитать скидку', onSubmit }) {
  const document = useMemo(() => compile(source), [source]);
  const schema = useMemo(() => ftsFormSchema(document, objectName), [document, objectName]);
  const [value, setValue] = useState(() =>
    Object.fromEntries(schema.fields.map((field) => [field.name, field.control === 'checkbox' ? false : ''])),
  );

  const preview = useMemo(() => {
    try {
      const input = Object.fromEntries(
        schema.fields.map((field) => [
          field.name,
          field.control === 'checkbox' ? Boolean(value[field.name]) : Number(value[field.name] || 0),
        ]),
      );
      return { ok: true, amount: executeUtility(document, utility, input) };
    } catch (error) {
      /* Нарушенное свойство модели — это нормальный ответ формы, а не падение UI. */
      return { ok: false, reason: error.message };
    }
  }, [document, schema, utility, value]);

  return (
    <form
      onSubmit={(event) => {
        event.preventDefault();
        onSubmit?.(value);
      }}
    >
      <h2>{schema.title}</h2>

      {schema.fields.map((field) => (
        <label key={field.name}>
          <span>{field.label}</span>
          <input
            type={field.control === 'checkbox' ? 'checkbox' : field.control === 'text' ? 'text' : 'number'}
            required={field.required}
            checked={field.control === 'checkbox' ? Boolean(value[field.name]) : undefined}
            value={field.control === 'checkbox' ? undefined : value[field.name]}
            onChange={(event) =>
              setValue((current) => ({
                ...current,
                [field.name]: field.control === 'checkbox' ? event.target.checked : event.target.value,
              }))
            }
          />
        </label>
      ))}

      <output>
        {preview.ok ? `Скидка: ${preview.amount} ₽` : `Правило не выполняется: ${preview.reason}`}
      </output>

      <button type="submit" disabled={!preview.ok}>
        Оформить
      </button>
    </form>
  );
}

Предметные правила как обычный шаг CI

Проверка модели, выполнение примеров, сверка сгенерированного кода и тесты интеграций — четыре шага, которые ловят расхождение текста правила и кода.

Файл
.github/workflows/fts-check.yml
Локально
npm run fts:examples
examples/fts/ci/fts-check.yml
# Предметные правила как обычный шаг CI.
#
# Смысл шага не в «ещё одном линтере»: примеры внутри .fts — это тесты,
# написанные на языке предметной области, а сгенерированный TypeScript
# сверяется с моделью. Правило, изменённое в коде мимо модели, ломает сборку.
#
# Файл кладётся в .github/workflows/fts-check.yml
name: fts

on:
  push:
    branches: [master]
  pull_request:

jobs:
  rules:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - uses: actions/setup-node@v4
        with:
          node-version: 24
          cache: npm

      - run: npm ci

      # Модель разобралась, типы сошлись, ссылки на объекты и поля существуют.
      - name: Проверить модели
        run: npx fts check static/fts/models/order-discount.fts

      # Примеры из .fts выполняются как предметные unit-тесты.
      - name: Выполнить предметные примеры
        run: npx fts test static/fts/models/order-discount.fts --pretty

      # Сгенерированный TypeScript обязан совпадать с закоммиченным.
      - name: Сверить сгенерированный код
        run: node examples/fts/typescript-codegen/generate.mjs --check

      # Интеграции: HTTP-сервис, guard допуска команды, схема формы.
      - name: Тесты интеграций
        run: node --test "examples/fts/**/*.test.mjs"
Что падаетрасхождение модели и коданепройденный пример

Где проходит граница

FTS не заменяет React, Node.js или Python — он отдаёт им решение, посчитанное на снимке данных.

Внешних эффектов у языка нет вовсе: ни HTTP, ни SQL, ни оплаты. Поэтому интеграция у всех стеков одна и та же и состоит из четырёх шагов, из которых язык занимает ровно один.

вся граница целикомNode.js
import { compile, executeUtility } from "@digitable-lol/fts"

const model = compile(source)
const discount = executeUtility(
  model,
  "Рассчитать скидку",
  { сумма: 20_000, "постоянный клиент": true }
)
  1. Приложение читает данныеБаза, HTTP, очередь — всё, что умеет ваш стек. Язык в этом не участвует и знать о нём не должен.
  2. FTS считает решениеПо переданному снимку и без обращений наружу: одни и те же входы всегда дают один и тот же ответ.
  3. Приложение проверяет результатНарушено свойство или разошёлся пример — придёт диагностика с кодом (FTS_UTILITY_PROPERTY) и ненулевой код выхода, а не тихое «безопасное» число.
  4. Приложение выполняет эффектСписать деньги, отгрузить заказ, разрешить команду агенту — это делает ваш код, уже зная ответ и его обоснование.

Тот же вызов с другой стороны разобран в курсе: Node.js и граница HTTP, форма и таблица в React из одной модели, Python, Go и shell через CLI, допуск команды AI-агенту. Граница везде одна: JSON внутрь, JSON наружу, ненулевой код выхода на провале.

Где применяют

232 прикладных кейса в 29 отраслях.

Каждый кейс называет входные факты, роль FTS, выходной артефакт и место интеграции.

Показано 24 из 232
РитейлMiddle

Рассчитать скидку корзины

Retail: deterministic calculation

  1. ВходСумма корзины, сегмент и промокод
  2. FTSСложить применимые проценты и проверить верхний предел
  3. На выходеЧисловая скидка без скрытых веток
Node.jsFTS runtimeTypeScriptnode:test
РитейлSenior

Разрешить возврат товара

Retail: command eligibility

  1. ВходПокупка, срок и состояние товара
  2. FTSВывести право на возврат из проверяемых фактов
  3. На выходеКоманда «Оформить возврат» разрешена или отклонена
DDDcommand guardcertificateJSON
РитейлQA / Middle

Проверить бесплатную доставку

Retail: executable examples

  1. ВходСумма, регион и вес
  2. FTSВыполнить примеры на границах тарифа
  3. На выходеРегрессия тарифа блокирует сборку
CI/CDfts testpropertyCI gate
РитейлJunior

Собрать форму товарной карточки

Retail: generated form

  1. ВходСтруктура товара и обязательность полей
  2. FTSСкомпилировать поля в каноническую модель
  3. На выходеОписание React-формы
Reactcanonical JSONform descriptorReact
РитейлJunior / Middle

Собрать таблицу остатков

Retail: generated table

  1. ВходSKU, склад, остаток и резерв
  2. FTSПревратить типы полей в колонки
  3. На выходеКонфигурация таблицы без ручного дублирования
React / Webcanonical JSONtable columnsfrontend
РитейлSenior / Lead

Доказать готовность заказа к выдаче

Retail: verified transition

  1. ВходОплата и факт комплектации
  2. FTSСкомпозировать состояния в разрешение выдачи
  3. На выходеПроверяемый сертификат перехода
ArchitecturemorphismcertificateMermaid
РитейлAI agent

Дать агенту расчёт цены

Retail: agent tool

  1. ВходЗапрос покупателя и снимок корзины
  2. FTSВызвать детерминированную FTS-утилиту через MCP
  3. На выходеСтруктурированный ответ с диагностикой
Digit / MCPMCPstructured resultdiagnostics
РитейлTeam

Защитить правила промокодов

Retail: regression gate

  1. ВходНабор граничных примеров
  2. FTSЗапустить примеры и свойства в CI
  3. На выходеНенулевой exit code при расхождении
CI/CDgenerated testsexit codebuild gate
МаркетплейсыMiddle

Рассчитать комиссию продавца

Marketplaces: deterministic calculation

  1. ВходКатегория, оборот и тариф
  2. FTSПрименить последовательность комиссионных правил
  3. На выходеСумма комиссии и сгенерированный тест
Node.jsFTS runtimeTypeScriptnode:test
МаркетплейсыSenior

Разрешить публикацию товара

Marketplaces: command eligibility

  1. ВходКарточка, документы и ограничения
  2. FTSПроверить свидетельства допуска
  3. На выходеКоманда публикации с объяснимым guard
DDDcommand guardcertificateJSON
МаркетплейсыQA / Middle

Проверить SLA отгрузки

Marketplaces: executable examples

  1. ВходДедлайн, статус и схема FBO/FBS
  2. FTSЗафиксировать примеры нарушения SLA
  3. На выходеВоспроизводимый тест бизнес-сроков
CI/CDfts testpropertyCI gate
МаркетплейсыJunior

Собрать форму нового SKU

Marketplaces: generated form

  1. ВходАтрибуты категории товара
  2. FTSПолучить поля из одной структуры FTS
  3. На выходеДинамическая форма кабинета
Reactcanonical JSONform descriptorReact
МаркетплейсыJunior / Middle

Собрать таблицу выплат

Marketplaces: generated table

  1. ВходПериод, продажи, удержания, итог
  2. FTSСопоставить типы с форматтерами колонок
  3. На выходеТаблица сверки выплат
React / Webcanonical JSONtable columnsfrontend
МаркетплейсыSenior / Lead

Доказать право на выплату

Marketplaces: verified transition

  1. ВходДоставка, период спора и KYC
  2. FTSСвязать факты морфизмами допуска
  3. На выходеСертификат разрешения выплаты
ArchitecturemorphismcertificateMermaid
МаркетплейсыAI agent

Дать агенту проверку листинга

Marketplaces: agent tool

  1. ВходТекст карточки и факты продавца
  2. FTSПередать исходник в fts_check и fts_execute
  3. На выходеРешение агента, ограниченное валидатором
Digit / MCPMCPstructured resultdiagnostics
МаркетплейсыTeam

Защитить сетку комиссий

Marketplaces: regression gate

  1. ВходПримеры по категориям и порогам
  2. FTSГенерировать node:test из FTS
  3. На выходеСтабильный релиз тарификации
CI/CDgenerated testsexit codebuild gate
БанкингMiddle

Рассчитать кредитный лимит

Banking: deterministic calculation

  1. ВходДоход, нагрузка и риск-класс
  2. FTSВычислить лимит и проверить максимум
  3. На выходеДетерминированный лимит
Node.jsFTS runtimeTypeScriptnode:test
БанкингSenior

Разрешить выдачу кредита

Banking: command eligibility

  1. ВходKYC, скоринг и риск-проверка
  2. FTSСкомпозировать свидетельства допуска
  3. На выходеGuard команды выдачи
DDDcommand guardcertificateJSON
БанкингQA / Middle

Проверить пороги скоринга

Banking: executable examples

  1. ВходГраничные баллы и ожидаемые классы
  2. FTSИсполнить предметные примеры
  3. На выходеТесты скоринговой политики
CI/CDfts testpropertyCI gate
БанкингJunior

Собрать форму заявки

Banking: generated form

  1. ВходПоля клиента и финансов
  2. FTSСкомпилировать структуру заявки
  3. На выходеReact-форма с типами
Reactcanonical JSONform descriptorReact
БанкингJunior / Middle

Собрать таблицу просрочек

Banking: generated table

  1. ВходДоговор, DPD и остаток долга
  2. FTSПолучить колонки из структуры
  3. На выходеОперационная таблица коллекшна
React / Webcanonical JSONtable columnsfrontend
БанкингSenior / Lead

Доказать допустимость операции

Banking: verified transition

  1. ВходЛимит, санкционный контроль и MFA
  2. FTSПровести типизированную цепочку морфизмов
  3. На выходеПроверяемый сертификат операции
ArchitecturemorphismcertificateMermaid
БанкингAI agent

Дать агенту pre-check заявки

Banking: agent tool

  1. ВходАнкета без сетевых секретов
  2. FTSВызвать read-only MCP-инструменты FTS
  3. На выходеСтруктурированный pre-check
Digit / MCPMCPstructured resultdiagnostics
БанкингTeam

Защитить риск-политику

Banking: regression gate

  1. ВходНабор одобренных и отказных заявок
  2. FTSПроверить свойства и примеры в CI
  3. На выходеЗапрет мержа при изменении решения
CI/CDgenerated testsexit codebuild gate

Границы

Чего язык не делает.

  • Внешних эффектов нет. Ни HTTP, ни SQL, ни оплаты: приложение выполняет действие уже после результата FTS.
  • Коллекций и функций высшего порядка в FTS нет. map, filter, groupBy, debounce остаются в JavaScript и переезжать не должны.
  • Доказательство завершения — не всё. Тотальная функция может честно закончиться и вернуть неверное число: за правильность отвечают примеры, за сложность — никто.
  • Часть задач не выражается. Из взятого набора LeetCode 12 задач не пишутся вовсе, а у 6 решений завершение не доказано.
Чего не хватает языку: 16 пунктов и 12 невыразимых задач
разложение строки
Нет встроенной формы «символы строки» и нет образцов для строк: «пусто» и «голова и хвост» работают только со списком. Любой посимвольный проход — обычная функция. Это самая дорогая из недостач: она одна делает нетотальными задачи 13, 14, 20, 125.
убывание по мере
Анализ завершаемости знает только структурное убывание. Рекурсия «n минус 1», Евклид, двоичный поиск по границам — всё это FLANG_NOT_TOTAL, хотя завершается очевидно. Обход есть (список-топливо), но он засоряет сигнатуру.
ассоциативный массив
Нет ни словаря, ни множества. Каждая задача «посчитай, сколько раз встретилось» превращается из O(n) в O(n²): 1, 136, 169, 217, 49.
массив с индексным доступом
Список читается только с головы; «Элемент по номеру» пишется рекурсией и стоит O(n). Кучи, таблицы динамики и двумерные сетки на этом ломаются.
сравнение строк
types.mjs разрешает «больше»/«меньше» для строк, а interpret.mjs на них бросает FLANG_TYPE. Это расхождение слоёв: программа проходит проверку и падает при запуске. Сортировка строк невыразима.
логические операции
Нет «и», «или», «не» для признаков. Конъюнкция пишется вложенными «если», отрицание — сравнением «равен нет». Читается заметно хуже написанного условия.
параметрический полиморфизм
«Обратить» для списка числа и для списка строки — две разные функции с одинаковым телом. Опциональное значение приходится заводить отдельно под каждый тип, а имена вариантов обязаны быть уникальны в модуле.
модульность
Заголовок «модуль … использует …» разбирается, но связывания между файлами нет: каждое решение переписывает нужные ему «Приписать в начало» и «Соединить списки» заново. Стандартной библиотекой нельзя воспользоваться из решения.
значение варианта в примере
parseLiteralValue сворачивает конструктор варианта в запись из его полей и теряет имя варианта. Поэтому функция, принимающая или возвращающая сумму типов, примера иметь не может — приходится обкладывать её скалярными обёртками.
структурное сравнение в примерах
runExamples (compat.mjs) сравнивает результат с ожидаемым через Object.is, поэтому любой пример, возвращающий список или запись, считается провалившимся, даже когда значения совпадают поэлементно. Команда «flang test» на таких файлах не работает; тесты в flang/test сравнивают структурно (valuesEqual) и проходят.
встроенная форма «символ»
Парсер и builtins.mjs передают «символ N в текст» как (число, строка), а types.mjs ждёт (строка, число). Любое использование формы «символ» не проходит check; вместо неё приходится писать «подстрока текст с N по N».
встроенная форма «пусто»
В позиции выражения слово «пусто» всегда читается как литерал пустого списка, поэтому до одноимённой встроенной формы (проверка «список или строка пусты») из исходника не добраться. Пишется «(длина x) равен 0».
списочная форма «соединить»
builtins.mjs умеет «соединить список с разделителем», но поверхностный синтаксис «соединить X с Y» всегда даёт склейку двух строк. Соединение списка строк написано в stdlib заново.
вызов функции без аргументов
Применение записывается только как «Имя» от аргумента, поэтому функцию с пустым списком параметров вызвать нечем. Константы приходится делать функциями от неиспользуемого аргумента или встраивать выражением.
псевдоним типа
«тип «X» это список числа» разбирается в узел alias, но types.mjs раскладывает объявления на суммы и записи, и alias становится записью без полей. Пользоваться псевдонимами нельзя.
обработка ошибок
Отказ встроенной формы («к числу» от «abc», «голова» от пустого списка) прекращает вычисление целиком и не перехватывается. Проверять пригодность аргумента приходится заранее, а выразить эту проверку удаётся не всегда.
  • 3 Longest Substring Without Repeating Characters — Скользящее окно по строке: две границы, двигающиеся по числовым индексам, и множество символов в окне. Ни окна, ни множества, ни убывания по индексам язык не даёт; выразимо лишь квадратичным перебором подстрок в обычном классе, что уже не решение задачи.
  • 4 Median of Two Sorted Arrays — Требуемое O(log(m+n)) — двоичный поиск по разделяющей позиции сразу в двух массивах с произвольным доступом. Индексный доступ в flang линеен, поэтому даже правильный алгоритм даст O(n log n), а тотальность потребует топлива для каждого из двух поисков.
  • 23 Merge k Sorted Lists — Сам результат выразим (свёртка слиянием), но условие говорит о связных списках и требует O(N log k) через кучу. Связный список в flang неотличим от обычного списка, а куча требует индексного доступа. Задача в её настоящей формулировке отсутствует в языке вместе со структурой данных.
  • 76 Minimum Window Substring — Скользящее окно плюс счётчики символов в словаре. Ни того, ни другого; перебор всех подстрок требует обхода строки по двум индексам — нетотально и за пределами разумного лимита шагов.
  • 139 Word Break — Нужны и разрезы строки по всем позициям (обход строки), и запоминание уже посчитанных суффиксов. Первого нет тотально, второго нет никак: мемоизация — это состояние.
  • 146 LRU Cache — Требуется объект с состоянием и набором методов (get/put), сохраняющий его между вызовами. В flang нет ни изменяемых значений, ни объектов с методами, ни способа завести долгоживущее состояние: функция — чистое отображение аргументов в результат.
  • 155 Min Stack — То же: задача формулируется как API из четырёх операций над разделяемым состоянием. Выразить можно только «состояние в аргументе, состояние в результате», и это уже другая задача — соответствия условию не будет.
  • 179 Largest Number — Сортировка строк по правилу «a+b против b+a». Сравнивать строки в flang нельзя вообще: types.mjs считает строки упорядоченными, а интерпретатор на «больше»/«меньше» для строк бросает FLANG_TYPE («сравнения порядка допустимы только для чисел»). Обойти это можно только собственной посимвольной функцией сравнения — то есть нетотально и через несуществующее разложение строки.
  • 200 Number of Islands — Обход в глубину по сетке помечает посещённые клетки. Без изменяемых структур пометки пришлось бы возвращать новой сеткой на каждом шаге, а рекурсия «сетка после пометки» не убывает структурно — доказать конец нельзя. В обычном классе решение раздувается до неузнаваемости и всё равно упирается в отсутствие индексного доступа.
  • 208 Implement Trie — Опять API с состоянием; кроме того, узел бора — это словарь «символ → узел», а ассоциативных массивов нет. Список пар с линейным поиском превращает O(длины слова) в O(длины × алфавит) и перестаёт быть бором по существу.
  • 295 Find Median from Data Stream — Поток и две кучи: и то, и другое — состояние, живущее между вызовами. Куча к тому же требует индексного доступа к массиву, которого в языке нет (только «голова», «хвост» и обход).
  • 322 Coin Change — Динамика по таблице сумм: нужен массив длиной amount с чтением произвольной ячейки и записью в неё. Список flang читается только с головы, а построение таблицы свёрткой требует на каждом шаге линейного поиска — и всё равно рекурсия по сумме нетотальна. Наивный перебор экспоненциален и не укладывается в лимит шагов.

Дальше

Курс: от первого правила до production и проверяемых сертификатов.

23 модулей по FTS и 14 по flang — синтаксис, утилиты, тесты, диагностика, Node.js, React, DDD, AI/MCP, CI, тотальность и кодогенерация. В каждом модуле упражнение, которое открывается прямо в песочнице на шаге 3.

Открыть курс
  1. Язык и модель
  2. Утилиты и тесты
  3. Интеграции
  4. DDD и агенты
  5. Proofs и benchmark