flang компилятор доказывает, что программа не зациклится 0.7.22 GitHub English

Rosetta Code на flang

docs/examples/rosetta/ — канонические задачи Rosetta Code, решённые на flang. Это витрина: язык здесь сравнивают с тем же решением на других языках, поэтому важнее не краткость, а то, что видно при чтении — где завершение доказано, а где язык говорит, что доказать не может.

Файлов в наборе 28, по два на задачу: каждая записана на русской поверхности языка и на английской (*-english.flang). Это не перевод документации: у языка четыре равноправные поверхности записи — русская, английская, эсперанто и китайская, — и тотальная функция / total function — одно и то же ключевое слово (таблица слов — flang/self/lexer.flang; страница — Четыре поверхности записи). Здесь взяты две, потому что на странице задачи Rosetta Code второй листинг стоит ради читателя: рядом с русским листингом английский показывает, что русская запись — выбор, а не ограничение. Все четыре поверхности на одной задаче — в docs/examples/surfaces/.

Готовый текст для страниц вики — docs/examples/rosetta/WIKI.en.md. Порядок публикации, лицензионная оговорка и языковая страница описаны вне этого репозитория.

Как прогнать

bootstrap/flang test docs/examples/rosetta/                                # примеры всех файлов набора
bootstrap/flang check docs/examples/rosetta/towers-of-hanoi.flang --proof  # ведомость одного файла

test прогоняет примеры, объявленные внутри функций. check --proof печатает отчёт о доказательствах: чем несётся обещание «тотальная» у каждой функции и чем — каждое высказанное утверждение. Для «Ханойских башен» он кончается так (прогон 11 сентября 2026, двоичный 0.7.17, коммит 2c40752d0):

что высказано и чем это несётся:
  постусловие «ходов не бывает отрицательно» функции «Число ходов» — доказано индукцией по «список»: база 1 случай, шаг при допущении на частях (1 случай), правила сведения: неотрицательность по построению — утверждение обо ВСЕХ входах типа «список», а не о написанных

Слова этого отчёта не взаимозаменяемы: «доказано» — утверждение обо всех входах; «сетка N» — посчитано на N значениях автора, и это не доказательство; «объявлено, не доказано» — утверждение высказано, доказательства при нём нет. На прогоне 11 сентября 2026 (0.7.17, коммит 2c40752d0) у всех файлов набора каждое высказанное утверждение стоит в отчёте словом «доказано»; строк «сетка» и «объявлено, не доказано» нет ни в одном.

Оба файла каждой задачи проверяются прогоном по отдельности. Проверки, что два листинга — одна программа с точностью до переименования, в дереве нет.

Задачи

Функция без слова тотальная — та, о завершении которой компилятору не сказано ничего: он её не проверяет и не обещает. Столбец «не тотальны» перечисляет такие функции русского файла; в английском файле те же функции под английскими именами.

Задача Rosetta CodeФайлНе тотальныЧто видно на flang
Ackermann functionackermann-function.flang«Аккерман», «Записи совпадают»рекурсия по двум аргументам не убывает ни по части значения, ни постоянным шагом; тотальная «Аккерман замкнуто» считает первые три ряда замкнутыми формулами, а вне их отвечает нулём и говорит это примером
Factorialfactorial.flang«Числа от и до», «Факториал произведением»«Факториал» доказан точным шагом: аргумент объявлен натуральным и убывает на 1; «Числа от и до» считает вверх
Fibonacci sequencefibonacci.flang«Числа от и до», «Ряд Фибоначчи»«Фибоначчи шагом» доказана точным шагом, её неотрицательность — индукцией по натуральному аргументу
FizzBuzzfizzbuzz.flang«Числа от и до», «Физз-базз»три утверждения о «Слово для числа» — кратные пятнадцати, трём и пяти — доказаны сведением цели с телом, без теоремы
100 doorshundred-doors.flang«Числа от и до», «Открытые двери», «Квадраты до», «Двери и квадраты сходятся»неотрицательность «Сколько раз тронули» доказана без теоремы; всё, что считает вверх, не доказано
Levenshtein distancelevenshtein-distance.flang—все функции тотальны; ряды матрицы — списки («Нулевой ряд», «Новый ряд»)
Merge sortmerge-sort.flang—все тотальны; слияние и сортировка идут «с топливом» — по списку, который на каждом витке становится частью себя
Palindrome detectionpalindrome.flang—все тотальны: нормализация регистра и знаков, сравнение; утверждения о «Позиция подстроки» доказаны; та же задача отдельно показана на списке
Sequence of primes by trial divisionprimes-by-trial-division.flang«Просеять», «Числа от и до», «Простые до», «Простые до, с топливом»тотальна только «Просеять с топливом»; настоящее решето Эратосфена вычёркивает записью по индексу, а такой записи в языке нет — поэтому файл лежит под задачей о пробном делении
Quicksortquicksort.flang«Быстрая сортировка»рекурсия по отфильтрованным подспискам: подсписок меньше исходного, но не является его частью — доказательства нет; «Сортировка вставками» рядом тотальна
Reverse a stringreverse-string.flang—все тотальны; обращение идёт по кодовым точкам — в примере строка "а🙂"
Roman numeralsroman-numerals.flang—все тотальны; утверждения о «Значение цифры»: не меньше 0, не больше 1000 и по каждому знаку
Run-length encodingrun-length-encoding.flang—все тотальны; «Туда и обратно» — сжатие и разжатие обратны друг другу
Towers of Hanoitowers-of-hanoi.flang—все тотальны; неотрицательность «Число ходов» доказана индукцией по структуре списка

Столбец «не тотальны» снимается с файла командой grep '^функция ' docs/examples/rosetta/<файл>; чем доказана каждая тотальная — bootstrap/flang check docs/examples/rosetta/<файл> --proof.

Почему часть решений не тотальна

Это граница, которую язык проводит осознанно, а не недоделка. Способы доказать завершение разобраны на странице Что даёт признак «тотальная»; здесь названо только то, на чём набор эту границу показывает.

Что у постоянного шага есть опора вне формы программы, отчёт о доказательствах говорит сам: «на IEEE-754 шаг не всегда меняет число, поэтому сторож» — в каждый доказанный шагом вызов компилятор вставляет проверку убывания, и не убывший шаг даёт отказ FLANG_MEASURE, а не вечный цикл.

Чего в наборе нет

Дальше