Разбор: задачи с leetcode, решения и то, что о них доказано

Каталог examples/leetcode/ — 82 файла, 7 709 строк, 301 функция и 806 исполняемых примеров (замер 29 августа 2026). Это не пример, написанный для сайта, а код в дереве.

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

Пять способов доказать завершение, и они не равноценны

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

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

Отчёт печатается флагом --proof и различает слова, которые легко спутать: доказано — про все входы; сетка N — посчитано на N значениях автора и доказательством не является; объявлено, не доказано — утверждение высказано, доказательства при нём нет.

Задача 704. Двоичный поиск

Условие. Дан отсортированный по возрастанию список различных чисел и цель. Вернуть номер цели (считая с нуля) или −1, если её в списке нет. Требуется O(log n).

Решение целиком (examples/leetcode/704-binary-search.flang; вводный комментарий файла опущен, он пересказан ниже):

модуль «Двоичный поиск»

тотальная функция «Поиск в диапазоне»
  принимает топливо: список числа, элементы: список числа, цель: число, низ: число, верх: число
  возвращает число
  пример «Нашли середину»
    дано топливо равно [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 и (длина элементы)

Что доказано:

flang check examples/leetcode/704-binary-search.flang --proof

чем несётся обещание «тотальная»:
  «Поиск в диапазоне»  доказано структурой: аргумент 1 («топливо») на каждом витке становится частью себя; цепочка частей конечного дерева обрывается сама, сторожа нет
  «Двоичный поиск»     доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт

итог:
  функций 2: тотальных 2, обычных 0
  обещание несёт: композиция 1, структура 1, точный шаг 0, постоянный шаг 0, объявленная мера 0
  сторожей в рантайме: 0 мест

Здесь видна граница анализа. Двоичный поиск сужает пару чисел «низ» и «верх», а убывания по числам компилятор не признаёт: «середина плюс 1» — результат арифметики, а не часть значения. Прямая запись даёт отказ FLANG_NOT_TOTAL.

Приём в решении честный и стоит того, чтобы его запомнить: рядом с настоящими доводами едет «топливо» — список, у которого на каждом витке берётся хвост. Хвост списка — часть значения, значит цикл доказуемо конечен; а поскольку топливом служит сам входной список, шагов заведомо хватает — их нужно log₂n, а есть n. Ноль проверок в собранной программе: доказательство структурой бесплатно.

Задача 148. Сортировка слиянием

Условие. Отсортировать список по возрастанию за O(n log n).

Решение целиком (examples/leetcode/148-sort-list.flang):

модуль «Сортировка слиянием»

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

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

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

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

Что доказано:

flang check examples/leetcode/148-sort-list.flang --proof

чем несётся обещание «тотальная»:
  «Взять первые»         доказано структурой: аргумент 1 («элементы») на каждом витке становится частью себя; цепочка частей конечного дерева обрывается сама, сторожа нет
  «Отбросить первые»     доказано структурой: аргумент 1 («элементы») на каждом витке становится частью себя; цепочка частей конечного дерева обрывается сама, сторожа нет
  «Слить упорядоченные»  доказано объявленной мерой: убывает длина «первый» плюс длина «второй»; мера объявлена автором, сторож считает её на каждом витке — 2 места
  «Сортировка слиянием»  доказано объявленной мерой: убывает длина «элементы»; мера объявлена автором, сторож считает её на каждом витке — 2 места

итог:
  функций 4: тотальных 4, обычных 0
  обещание несёт: композиция 0, структура 2, точный шаг 0, постоянный шаг 0, объявленная мера 2

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

• убывает длина элементы — у сортировки: обе половины строго короче целого, потому что случай «не больше одного элемента» отработан до деления;
• убывает (длина первый) плюс (длина второй) — у слияния: за виток снимается ровно одна голова, а структурного убывания нет ни у одного из двух доводов во всех ветвях сразу.

Цена названа тут же, у каждой из двух функций: по два места в собранной программе, где мера пересчитывается при работе. Два помощника — «Взять первые» и «Отбросить первые» — доказаны структурой и не стоят ничего.

Задача 42. Сбор дождевой воды

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

Решение целиком (examples/leetcode/042-trapping-rain-water.flang):

модуль «Дождевая вода»

тотальная функция «Большее из двух»
  принимает первый: число, второй: число
  возвращает число
  пример «Второй больше»
    дано первый равно 2
    дано второй равно 5
    ожидается 5
  пример «Первый больше»
    дано первый равно 5
    дано второй равно 2
    ожидается 5
  если первый не меньше второй то первый иначе второй

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

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

Что доказано:

flang check examples/leetcode/042-trapping-rain-water.flang --proof

чем несётся обещание «тотальная»:
  «Большее из двух»   доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт
  «Вода в диапазоне»  доказано объявленной мерой: убывает «право» минус «лево» плюс 1; мера объявлена автором, сторож считает её на каждом витке — 2 места
  «Дождевая вода»     доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт

итог:
  функций 3: тотальных 3, обычных 0
  обещание несёт: композиция 2, структура 0, точный шаг 0, постоянный шаг 0, объявленная мера 1

Два указателя навстречу друг другу — приём, у которого нет ни одного убывающего списка: убывает расстояние между границами. Оно и записано мерой: убывает право минус лево плюс 1. Каждый виток двигает ровно одну границу, и компилятор проверяет это сам, а не верит комментарию.

Пять величин, которые в языке с циклами были бы переменными, здесь едут доводами функции. Это цена отсутствия цикла, и она видна прямо в подписи.

Задача 13. Римские цифры в число

Условие. Перевести римскую запись числа в число.

Единственная задача каталога, у которой есть не только доказанное завершение, но и утверждение о результате — два постусловия обеспечивает.

Решение целиком (examples/leetcode/013-roman-to-integer.flang):

модуль «Римские числа»

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

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

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

тотальная функция «Символы»
  принимает текст: строка
  возвращает список строки
  пример «Две цифры»
    дано текст равно "IV"
    ожидается ["I", "V"]
  пример «Пустая запись»
    дано текст равно ""
    ожидается пустой список
  разложить текст на символы

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

Что доказано:

flang check examples/leetcode/013-roman-to-integer.flang --proof

чем несётся обещание «тотальная»:
  «Приписать строку в начало»  доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт
  «Значение цифры»             доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт
  «Символы»                    доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт
  «Римское в число»            доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт

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

итог:
  функций 4: тотальных 4, обычных 0
  обещание несёт: композиция 4, структура 0, точный шаг 0, постоянный шаг 0, объявленная мера 0

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

Обратите внимание, что написано не меньше 0, а не не меньше 1. Знак вне таблицы даёт ноль, и не меньше 1 было бы ложью — которую поймал бы тот же прогон, на примере «Не римская цифра».

Задача 202. Счастливое число

Условие. Заменяем число суммой квадратов его цифр и повторяем. Число счастливое, если рано или поздно получится 1; иначе последовательность зацикливается.

Эта задача здесь потому, что на ней доказательство не проходит, и файл об этом говорит прямо.

Решение целиком (examples/leetcode/202-happy-number.flang):

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

тотальная функция «Сумма квадратов цифр»
  принимает н: число
  возвращает число
  убывает н
  пример «Двузначное»
    дано н равно 19
    ожидается 82
  пример «Единица»
    дано н равно 1
    ожидается 1
  пример «Ноль»
    дано н равно 0
    ожидается 0
  если н не больше 0
    то 0
    иначе
      пусть цифра равно н остаток от 10
      пусть выше равно (н минус цифра) делить на 10
      (цифра умножить на цифра) плюс («Сумма квадратов цифр» от выше)

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

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

функция «Счастливое»
  принимает н: число
  возвращает признак
  пример «Пример 1 из условия»
    дано н равно 19
    ожидается да
  пример «Пример 2 из условия»
    дано н равно 2
    ожидается нет
  пример «Единица»
    дано н равно 1
    ожидается да
  пример «Семь счастливо»
    дано н равно 7
    ожидается да
  пример «Четвёрка — начало известного цикла»
    дано н равно 4
    ожидается нет
  пример «Сто счастливо»
    дано н равно 100
    ожидается да
  «Шаг счастья» от н и пустой список

Что доказано:

flang check examples/leetcode/202-happy-number.flang --proof

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

итог:
  функций 4: тотальных 2, обычных 2
  обещание несёт: композиция 1, структура 0, точный шаг 0, постоянный шаг 0, объявленная мера 1

«Шаг счастья» и «Счастливое» — единственные две функции всего каталога, написанные словом функция, а не тотальная функция. Они завершаются: последовательность сумм квадратов цифр попадает в цикл, а цикл ловится списком виденных. Но довод этот — теорема о числах, а не убывание чего-либо в тексте программы: не убывает ни список, ни разность, ни само число. Мерой это не записать, и файл честно пишет функция.

Так выглядит отказ, который не скрыт. Компилятор не молчит и не верит на слово: раз доказать нечем, обещания просто нет, и в отчёте стоит «о завершении не сказано ничего».

Весь каталог числом

299 функций из 301 объявлены словом тотальная — то есть несут обещание завершения, а обещание это компилятор обязан доказать: не сумев, он отказывается собрать файл. Это не «примеры прошли». Для задач вроде «поиск в повёрнутом отсортированном списке» или «сбор дождевой воды» бесконечный цикл закрыт до запуска программы.

Утверждений о результате на все 82 задачи — 85, и стоят они в 37 файлах. Здесь стояло «два, оба в задаче 13»: это был замер того дня, и с тех пор набор дописали. Разрыв, однако, никуда не делся: 85 постусловий на 301 функцию — это меньше трети файлов, и о завершении доказано у 299 функций, а о правильности счёта — у меньшинства. Остальную правильность несут 806 примеров, а пример — утверждение об одном входе.

Разрыв между «доказано» и «правильно» — это спецификация. Её можно написать: обеспечивает принимает любая функция, и компилятор попробует доказать. Как это делается — Требования, которые доказываются.

Дальше

• Что доказано, а что нет — где проходит граница.
• Зачем и как — как работает ядро доказательств.
• Отказы доказательства — почему проверка отказывает и что с этим делать.