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

Каталог docs/examples/leetcode/ — 82 файла, 6 224 строки, 301 функция и 806 исполняемых примеров (wc -l, grep -c по заголовкам функций и примеров). Это не пример, написанный для сайта, а код в дереве. Листинги и отчёты ниже сняты с этого же дерева; модули примеров названы по-английски.

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

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

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

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

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

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

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

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

модуль «Binary search»

тотальная функция «Поиск в диапазоне»
  принимает топливо: список числа, элементы: список числа, цель: число, низ: число, верх: число
  возвращает число
  пример «Нашли середину»
    дано топливо равно [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 docs/examples/leetcode/704-binary-search.flang --proof

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

законы (сетка конечна, доказательством не является):
  нет объявленных законов

принято на веру:
  ничего

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

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

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

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

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

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

модуль «Sort list»

тотальная функция «Взять первые»
  принимает элементы: список числа, сколько: число
  возвращает список числа
  пример «Первые два»
    дано элементы равно [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 docs/examples/leetcode/148-sort-list.flang --proof

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

законы (сетка конечна, доказательством не является):
  нет объявленных законов

принято на веру:
  ничего

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

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

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

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

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

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

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

модуль «Trapping rain water»

тотальная функция «Большее из двух»
  принимает первый: число, второй: число
  возвращает число
  обеспечивает «большее — первое, когда первое не меньше второго» если первый не меньше второй то (результат равен первый) иначе да
  обеспечивает «иначе большее — второе» если не (первый не меньше второй) то (результат равен второй) иначе да
  пример «Второй больше»
    дано первый равно 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 docs/examples/leetcode/042-trapping-rain-water.flang --proof

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

законы (сетка конечна, доказательством не является):
  нет объявленных законов

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

принято на веру:
  ничего

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

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

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

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

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

Задача, у которой есть не только доказанное завершение, но и утверждения о результате — шесть постусловий обеспечивает у «Значения цифры» (два о границах и четыре о первых буквах таблицы).

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

модуль «Roman to integer»

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

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

тотальная функция «Значение цифры»
  принимает буква: строка
  возвращает число
  обеспечивает «значение цифры неотрицательно» результат не меньше 0
  обеспечивает «значение цифры не больше тысячи» результат не больше 1000
  обеспечивает «I — это один» если буква равен "I" то (результат равен 1) иначе да
  обеспечивает «V — это пять» если не (буква равен "I") то (если буква равен "V" то (результат равен 5) иначе да) иначе да
  обеспечивает «X — это десять» если не (буква равен "I") то (если не (буква равен "V") то (если буква равен "X" то (результат равен 10) иначе да) иначе да) иначе да
  обеспечивает «L — это пятьдесят» если не (буква равен "I") то (если не (буква равен "V") то (если не (буква равен "X") то (если буква равен "L" то (результат равен 50) иначе да) иначе да) иначе да) иначе да
  пример «Единица»
    дано буква равно "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 docs/examples/leetcode/013-roman-to-integer.flang --proof

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

законы (сетка конечна, доказательством не является):
  нет объявленных законов

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

принято на веру:
  ничего

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

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

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

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

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

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

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

модуль «Happy number»

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

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

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

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

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

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

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

Код возврата 0. У двух обычных функций стоит «обещания нет: функция обычная, о завершении не сказано ничего».

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

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

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

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

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

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

Дальше

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