Учебник

Шесть глав: от первой функции до утверждения, которое ядро доказало обо всех входах. Каждая глава — код, прогон и упражнение с ответом.

Нужен установленный flang (как поставить) и пять минут на первую программу — она здесь не повторяется.

Каждая программа ниже показана целиком: скопируйте её в файл, добавьте первой строкой модуль «Учебник» и прогоните flang check и flang test.

Глава 1. Функция, типы, пример

тотальная функция «Удвоить»
  принимает н: число
  возвращает число
  пример «дважды два»
    дано н равно 2
    ожидается 4
  н умножить на 2

Имя функции — в ёлочках: «Удвоить». Вызов пишется «Удвоить» от 21.

пример — не тест сбоку, а часть объявления: его прогоняет и flang test, и flang check. Пример без имени написать нельзя, и это не педантизм — по имени на него ссылается доказательство (глава 6).

Обе команды на файле из этой главы отвечают так:

flang check ch1.flang
flang test ch1.flang
flang run ch1.flang --function Удвоить --args '{"н": 21}'

модуль «Учебник»: функций 2, из них с доказанным завершением 2; типов 0
ch1.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
ch1.flang: примеров 2, прошло 2, не прошло 0
42

Упражнение 1. Напишите «Утроить» с примером «трижды два».

тотальная функция «Утроить»
  принимает н: число
  возвращает число
  пример «трижды два»
    дано н равно 2
    ожидается 6
  н умножить на 3

Теперь вы умеете: объявить функцию с типами и примером, проверить её и вызвать из командной строки.

Глава 2. Циклов нет — есть свёртка

Цикла в языке нет вовсе. Обход списка пишется свёртка:

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

Читается так: начать с 0, идти по списку, на каждом шаге взять накопленное (акк) и очередной элемент (эл) и дать новое накопленное.

Стрелка набирается →, -> или => — это одно и то же. Здесь и дальше стоит →; если её нет на клавиатуре, пишите ->.

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

Условие внутри свёртки писать можно, отдельной формы для «наибольшего» не нужно:

  свёртка элементы начиная с 0 как акк и эл → если эл больше акк то эл иначе акк

Ловушка имён. эл — обычное имя, а элемент — слово языка («элемент списка по номеру»), и занять его нельзя. На такой попытке компилятор отвечает так:

FLANG_PARSE в файле ch2.flang, строка 9, столбец 68: не разобрана конструкция: неожиданное '
'

Причины сообщение не называет, показывает на конец строки. Занятые имена перечислены в словаре — 150 понятий.

Упражнение 2. Сумма квадратов списка [1, 2, 3] — 14.

  свёртка элементы начиная с 0 как акк и эл → акк плюс (эл умножить на эл)

Три свёртки этой главы одним файлом дают:

модуль «Свёртки»: функций 3, из них с доказанным завершением 3; типов 0
ch2.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
ch2.flang: примеров 3, прошло 3, не прошло 0

Теперь вы умеете: обойти список свёрткой — суммой, наибольшим, любым накоплением — без единого цикла.

Глава 3. Четыре формы тела, и выбор не безразличен

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

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

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

Глава 4. тотальная — обещание, которое проверяют

тотальная значит «завершается на любом входе», и компилятор это проверяет. Вот программа, которая обещания не держит:

тотальная функция «Крутить»
  принимает н: число
  возвращает число
  если н равен 0
    то 0
    иначе «Крутить» от (н минус 1)

flang check отказывает и называет, чего не хватило:

FLANG_NOT_TOTAL в файле krutit.flang, строка 8, столбец 11: тотальная функция
«Крутить»: рекурсивный вызов «Крутить» не убывает — аргумент 1 («н» sub 1)
уменьшает параметр «н», но снизу «н» ничем не ограничен: добавьте проверку вида
«если н не больше 0». Передавайте часть аргумента: хвост списка из образца
«голова и хвост», поле варианта из образца, поле записи или элемент коллекции

И он прав: на входе −1 эта функция не завершится никогда — мимо равен 0 отрицательные числа проходят. Правка ровно та, что названа: равен → не больше.

  если н не больше 0

После неё flang check отвечает «замечаний нет», а отчёт flang check --proof называет, на чём обещание держится:

«Сумма до»  доказано постоянным шагом: аргумент 1 («н») убывает на постоянный
шаг и ограничен снизу; на IEEE-754 шаг не всегда меняет число, поэтому сторож,
1 место

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

Упражнение 3. Объявите вход неотрицательное вместо число — проверка проходит и без правки условия, потому что отрицательных входов в этом типе нет. Границу тогда проверяет вызов:

flang run ch4.flang --function 'Сумма до' --args '{"н": -3}'

FLANG_TYPE: вызов функции «Сумма до»: аргумент «н»: -3 вне неотрицательное

Код возврата 1.

Теперь вы умеете: прочитать отказ FLANG_NOT_TOTAL и починить рекурсию ровно так, как он просит.

Глава 5. Сумма типов и разбор

Своё множество значений объявляется так:

тип «Оценка»
  вариант «отлично»
  вариант «хорошо»
  вариант «удовлетворительно»

Разбирается — так:

тотальная функция «Балл оценки»
  принимает оценка: «Оценка»
  возвращает число
  разбор оценка
    случай вариант «отлично»
      то 5
    случай вариант «хорошо»
      то 4
    случай вариант «удовлетворительно»
      то 3

Забытый случай — ошибка проверки, а не сюрприз во время работы:

FLANG_MATCH_NOT_EXHAUSTIVE в файле cveta.flang, строка 10, столбец 3:
разбор «Цвет» не покрывает «зелёный»

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

Упражнение 4. Добавьте вариант «неявка» и допишите разбор так, чтобы неявка стоила 0. Проверка обязана снова стать зелёной:

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

Теперь вы умеете: объявить свой тип из вариантов и разобрать его так, что забытый случай не доживёт до запуска.

Глава 6. От «сетки» к «доказано»

Утверждение о результате пишется словом обеспечивает:

  обеспечивает «сумма до неотрицательна» результат не меньше 0

Само по себе оно доказательством не становится, и отчёт говорит, на чём оно держится на самом деле:

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

Дальше два хода, и оба показаны прогоном.

Ход первый: индукция по объявленной сумме. У типа из трёх вариантов-констант каждый случай закрывается ссылкой на пример:

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

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

Ход второй: предусловие как факт. требует — то, что обязан обеспечить вызывающий; ядру оно даёт факт, из которого выводится результат:

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

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

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

Проверьте, что доказательство не подделывается. Уберите строку требует — утверждение станет ложным (на −1 результат равен −2), и ядро откажет:

FLANG_PROOF_INDUCTION_STEP в файле ch6.flang, строка 15, столбец 3: шаг 1,
теорема «двойная норма неотрицательна»: «по предположению» стоит вне индукции,
а допущений у этой цели нет ни одного: ни посылки индукции (её даёт `индукция
по`), ни предусловия функции (его даёт `требует`). Предполагать не о чем.
к этому месту не известно ничего, кроме гипотез «дано»

Теорема без опоры не принимается. Это и есть разница между «написал» и «доказано».

Упражнение 5. Докажите то же про «Тройная норма» с телом норма умножить на 3. Ответ: та же строка требует и те же четыре строки теоремы; отчёт ответит «доказано: терм принят ядром, 1 шаг».

Теперь вы умеете: довести утверждение от «сетки» до «доказано» — индукцией по объявленному типу или предусловием как фактом.

Что говорит компилятор, когда вы ошиблись

Все сообщения ниже сняты прогоном flang check на маленьких программах. Замечание — это код, файл, строка, столбец и текст; код возврата 1.

Все отказы ядра доказательств — а FLANG_PROOF_INDUCTION_STEP один из них — разобраны поимённо на странице Ядро отказало: чья это ошибка: там у каждого сказано, правится он теоремой или упирается в предел языка. Остальные коды компилятора перечислены на странице руководства (man flang), раздел ДИАГНОСТИКА.

Что дальше

• Операции языка — списки, строки, множества, числа
• Словарь языка — 150 понятий, из них 133 открыты на всех четырёх поверхностях записи