Доказательство руками

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

Как узнать, что ядро не справилось

flang check без ключей не говорит о постусловиях ничего: недоказанное постусловие — не ошибка, оно проверяется при работе после каждого возврата. Спрашивать надо отчёт о доказательствах:

flang check файл.flang --proof

В разделе «что высказано и чем это несётся» у каждого постусловия один из четырёх ответов:

Ответ	Что значит	Что делать
`доказано …`	верно для всех входов	ничего
`сетка N значений`	проверено только на примерах функции	писать теорему
`объявлено, не доказано`	нет ни доказательства, ни примеров	писать теорему
`НАРУШЕНО` / `ЛОЖНО`	найден контрпример	чинить функцию или постусловие, а не доказывать

Ключ --strict переводит ответ в код возврата: 0 — доказано всё, 1 — опровергнуто, 3 — что-то стоит на сетке или не доказано. Его удобно ставить в сборку.

Скелет теоремы

теорема «имя постусловия»
  дано параметр: тип
  утверждаем то же, что после имени в обеспечивает
  обоснование
  следовательно доказано

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

Приём	Когда брать
`индукция по` + `по предположению` / `по примеру`	функция обходит свой тип с вариантами `разбор`ом
`по свойству «имя»`	функция зовёт другую, у которой постусловие уже доказано
шаги `затем … по закону «правило» из …`	нужна цепочка фактов, которую ядро само не строит

Приём первый: индукция

Функция считает высоту стопки, начиная с заданного дна. Дно неотрицательно по предусловию, поэтому и результат неотрицателен.

модуль «Высота стопки»

тип «Стопка»
  вариант «Пусто»
  вариант «Звено» содержит голова: число, хвост: «Стопка»

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

Ядро само не доказывает:

постусловие «высота от дна неотрицательна» функции «Высота от дна» — сетка 1 значение (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

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

модуль «Высота стопки»

тип «Стопка»
  вариант «Пусто»
  вариант «Звено» содержит голова: число, хвост: «Стопка»

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

теорема «высота от дна неотрицательна»
  дано стопка: «Стопка»
  дано дно: число
  утверждаем результат не меньше 0
  индукция по стопка
    случай вариант «Пусто»
      то по предположению
    случай вариант «Звено» с голова как г и хвост как х
      то по предположению
  следовательно доказано

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

Если случай покрывает одно значение (случай вариант «Пусто», случай пусто, случай 0) и у функции есть пример ровно с этим значением, вместо допущения можно сослаться на пример: то по примеру «пустая от нуля». Для случая со связанными именами пример не годится: он одно значение, а случай — бесконечно много.

Индукция работает по типу с вариантами (своему или списку) и по неотрицательное со спуском ровно на единицу. По число и целое индукции нет: ядро ответит FLANG_PROOF_INDUCTION_TYPE.

Приём второй: свойство вызванной функции

Добавим функцию, которая считает высоту от нулевого дна:

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

Её постусловие ядро тоже оставляет сеткой. Довод короткий: тело — вызов «Высоты от дна», а у неё постусловие уже доказано. Так и пишется:

модуль «Высота стопки»

тип «Стопка»
  вариант «Пусто»
  вариант «Звено» содержит голова: число, хвост: «Стопка»

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

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

теорема «высота от дна неотрицательна»
  дано стопка: «Стопка»
  дано дно: число
  утверждаем результат не меньше 0
  индукция по стопка
    случай вариант «Пусто»
      то по предположению
    случай вариант «Звено» с голова как г и хвост как х
      то по предположению
  следовательно доказано

теорема «высота неотрицательна»
  дано стопка: «Стопка»
  утверждаем результат не меньше 0
  по свойству «высота от дна неотрицательна»
  следовательно доказано

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

flang check файл.flang --proof --strict на этом файле отвечает кодом 0; без двух теорем — кодом 3.

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

Приём третий: цепочка шагов с названными правилами

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

модуль «Через середину»

тотальная функция «Меньшее из пары»
  принимает а: число, б: число
  требует «а не больше б» а не больше б
  требует «б не больше десяти» б не больше 10
  возвращает число
  обеспечивает «результат не больше десяти» результат не больше 10
  пример «три и семь»
    дано а равно 3
    дано б равно 7
    ожидается 3
  а

постусловие «результат не больше десяти» функции «Меньшее из пары» — сетка 1 значение (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

Теорема выписывает цепочку по шагу на строку. Каждый шаг — затем факт по закону «правило» из опор; опора — строка исходника (из строки 5) или номер предыдущего шага (из 1 и 2). Последний шаг без затем закрывает цель:

модуль «Через середину»

тотальная функция «Меньшее из пары»
  принимает а: число, б: число
  требует «а не больше б» а не больше б
  требует «б не больше десяти» б не больше 10
  возвращает число
  обеспечивает «результат не больше десяти» результат не больше 10
  пример «три и семь»
    дано а равно 3
    дано б равно 7
    ожидается 3
  а

теорема «результат не больше десяти»
  дано а: число
  дано б: число
  утверждаем результат не больше 10
  затем а не больше б по закону «О1» из строки 5
  затем б не больше 10 по закону «О1» из строки 6
  затем а не больше 10 по закону «О10» из 1 и 2
  по закону «Разв2» из 3 и строки 13
  следовательно доказано

постусловие «результат не больше десяти» функции «Меньшее из пары» — доказано: терм принят ядром, 4 шага — утверждение обо ВСЕХ входах

Строки 5 и 6 — предусловия, строка 13 — тело функции. Правил, которые можно назвать в шаге, шесть:

Правило	Что даёт
`Н1`	литерал не меньше нуля: `0 не меньше 0`
`Н3`	`х не меньше 0` из строки, где это сказано: предусловие или тип `неотрицательное`
`Н5`	сумма двух неотрицательных неотрицательна (из двух шагов)
`О1`	факт порядка `а не больше б` из строки, где он сказан
`О10`	через середину: из `а не больше б` и `б не больше в` — `а не больше в`
`Разв2`	подставляет тело функции вместо `результат` и закрывает цель

Ядро проверяет каждый шаг и говорит, какой не сошёлся. Шаг сослался не на ту строку:

FLANG_PROOF_STEP в файле m3.flang, строка 19, столбец 3: теорема «результат не больше десяти»: шаг 1 (О1, строка 6): О1 — допущение даёт «б не больше 10», а заключено «а не больше б»

Опоры переставлены местами:

FLANG_PROOF_STEP в файле m4.flang, строка 21, столбец 3: теорема «результат не больше десяти»: шаг 3 (О10, шаг 2 и шаг 1): О10 — середина не сходится: шаг 2 кончается «10», шаг 1 начинается «а»

Шаг с названным правилом стоит того ещё и потому, что его перепроверяет независимая программа (flang/proof/checker/checker.c): шаг без имени ей приходится принимать на слово ядра.

Любое другое имя правила отвергается, и сообщение перечисляет те, что есть:

FLANG_PROOF_STEP … правило «чего не бывает» ведомости ядро пока не проверяет; проверяет шесть: Н1, Н3, Н5, О1, О10, Разв2

Когда руками не доказать

Шесть правил не покрывают вычитание. Постусловие ниже верно, но ни ядро, ни теорема из этих правил его не доказывают:

модуль «Дополнение»

тотальная функция «Сколько дополнить»
  принимает ширина: число, длина: число
  требует «ширина конечна» (ширина минус ширина) равно 0
  требует «длина конечна» (длина минус длина) равно 0
  требует «ширина не меньше длины» ширина не меньше длина
  обеспечивает «дополнение неотрицательно» результат не меньше 0
  пример «ровно по ширине»
    дано ширина равно 5
    дано длина равно 5
    ожидается 0
  пример «дописать три»
    дано ширина равно 8
    дано длина равно 5
    ожидается 3
  ширина минус длина

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

Порядок работы

Напишите постусловие и спросите flang check --proof.
доказано — остановитесь, теорема не нужна.
НАРУШЕНО или ЛОЖНО — чините функцию или постусловие.
Сетка или «объявлено, не доказано» — пишите теорему: индукция, если функция идёт разбором; по свойству, если тело зовёт функцию с доказанным постусловием; шаги с правилами, если довод — цепочка фактов.
Отказ ядра — читайте хвост сообщения; что значит каждый код, сказано на странице Ядро отказало: чья это ошибка.

Полный синтаксис теоремы — в Справочнике конструкций.