Первая программа

Пять шагов: написать файл, проверить его, прогнать его unit-тесты, запустить функцию, сгенерировать из него C. Нужен установленный flang — как его поставить.

Всё в блоках вывода ниже скопировано из настоящего прогона текущего двоичного. Команды можно копировать одну за другой.

Написать

Положите в файл hello.flang:

модуль «Привет»

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

Что делает каждая часть:

Часть	Привычное название	Что с ней делает компилятор
`тотальная`	функция, которая всегда завершается	доказывает завершение; не смог — файл отвергнут
`принимает` / `возвращает`	типы параметров и результата	проверяет до любого запуска
`обеспечивает`	postcondition	prover пробует доказать его для всех входов. Имя в `«…»` обязательно: по нему постусловие называется в отчёте о доказательствах
`пример`	unit-тест прямо в функции	прогоняет при каждом `check`
последняя строка	тело функции	—

Имена модулей, функций и примеров всегда пишутся в ёлочках «…». " или ' вместо них не работают: по ёлочкам парсер понимает, что это ваше имя, а не ключевое слово.

Параметр объявлен неотрицательное, а не число, и это важно. С принимает н: число проверка не проходит: в тип число входит «не число» (NaN, например результат 0 делить на 0), а оно не больше и не меньше ничего:

FLANG_BOUND_ON_NAN в файле hello.flang, строка 6, столбец 3: постусловие
«удвоенное не меньше исходного» функции «Удвоить» ЛОЖНО, и контрпример назван:
«н» объявлен типом «число», а «не число» живёт в этом типе и стоит ВНЕ ПОРЯДКА
— оно не больше и не меньше ничего, включая самоё себя.
…

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

Проверить

flang check hello.flang

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

Код возврата 0. check выполняет пять шагов по порядку: разбор, типы, завершаемость, prover («ядро» в выводе), unit-тесты. Если какой-то шаг не прошёл, emit тоже не сгенерирует код.

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

Прогнать unit-тесты

flang test hello.flang

hello.flang: примеров 1, прошло 1, не прошло 0

Один пример, прошёл один, упало ноль.

Запустить

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

доказано: утверждений 1
42

Первая строка: единственное постусловие файла доказано. Пока в файле есть недоказанное постусловие, run ничего не вычисляет. Вторая строка — значение.

В командной строке имя функции пишется без ёлочек.

--args принимает JSON-объект, ключи — имена параметров из принимает. Он понимает только плоский объект скаляров: числа, строки, true, false, null. Список отвергается:

flang run summa.flang --function Сумма --args '{"элементы": [1,2,3]}'

flang run: «--args» разобрать не удалось — ждался плоский объект скаляров, вроде '{"н":10}'

Код возврата 2. Как передать список или запись — Операции языка, раздел про --args.

Типы аргументов flang run проверяет. Функция «Факториал» объявлена на неотрицательное; на −3 она отвечает так, код возврата 1:

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

Прочитать отчёт о доказательствах

flang check hello.flang --proof

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

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

Первая часть: «Удвоить» завершается, потому что в ней нет рекурсии и она вызывает только завершающиеся функции. Вторая часть: постусловие доказано из одного типа параметра — н неотрицательное, значит н плюс н не меньше н. Писать доказательство не пришлось. Строка итога отчёта кончается словами код возврата 0.

У постусловия бывает одно из трёх состояний:

В отчёте написано	Что это значит
доказано	верно для всех входов
сетка N	проверено только на N ваших примерах, как unit-тестами; доказательства нет
объявлено, не доказано	prover не смог доказать, и примеров нет; сгенерированный код проверяет условие во время работы

Как довести постусловие до «доказано» — учебник, глава 6.

Сгенерировать C

flang emit hello.flang --target c --out ./вывод

проверок при работе снято 1: постусловие доказано ядром обо всех входах и
проверено примерами функции — в напечатанный код оно не едет.
напечатано файлов 6, байт …, в ./вывод
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>

Как читать:

Первые две строки: постусловие доказано, поэтому проверка для него в код на C не попадает.
Третья: в ./вывод записано шесть файлов.
Последние строки: emit не прогоняет unit-тесты. Для этого есть flang test.

Каталог вывода создаётся сам. Сгенерированный код собирается обычным make:

make -C ./вывод

make: Entering directory '…/вывод'
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o flang_runtime.o flang_runtime.c
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o privet.o privet.c
ar rcs libprivet.a flang_runtime.o privet.o
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o flang_cli.o flang_cli.c
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto -o flang_cli flang_cli.o flang_runtime.o privet.o -lm -lpthread
make: Leaving directory '…/вывод'

Ни одного предупреждения при -Wall -Wextra -Werror -pedantic. Имя модуля «Привет» в файлах на C стало privet.

Одна ловушка: ваши имена становятся идентификаторами целевого языка, и совпадение — ошибка, а не тихое переименование. Назовите функцию «Double» — и генерация C не пройдёт, код возврата 1:

FLANG_CLI: имена «Double» и «зарезервировано в целевом языке: double» дают один идентификатор «double» — переименуйте одно из них в модели
flang emit: печать отменена — программа не проходит проверку, замечаний 1.
Разбор, типы, завершаемость и ядро доказательств смотрит «flang check» этого же
бинарника: он назовёт то же самое и полнее.

Сообщение называет обе стороны совпадения (double — ключевое слово C). Переименуйте функцию и запустите emit снова.

Другие целевые языки

Целевых языков десять: c, cpp, csharp, elixir, go, java, js, python, rust, ts. Команда та же, меняется только --target:

flang emit hello.flang --target rust --out ./вывод-rust

…
напечатано файлов 7, байт …, в ./вывод-rust
…
собрать: cd <каталог> && cargo build, запустить target/debug/flang_cli <модуль>

В каталоге вывода лежат Makefile и Cargo.toml; cargo build собирает target/debug/flang_cli, который вызывает ту же функцию.

Дальше

Учебник — шесть глав от первой функции до постусловия, которое доказывает prover
Какую конструкцию когда брать — что писать под задачу: enum, Optional, Result, map, filter, reduce
Операции языка — функции стандартной библиотеки для списков, строк и чисел