Справочник конструкций flang
Конструкции flang 0.7.32 с примерами. Каждый пример проверен этой версией компилятора при сборке страницы. Документация языка.
Программа и функции
Модуль и импорт модуль, экспортирует, использует
Файл начинается с имени модуля. «экспортирует» открывает функции другим модулям, «использует» подключает модуль стандартной библиотеки.
модуль «Report»
экспортирует «Итог»
использует «Lists»
тотальная функция «Итог»
принимает элементы: список числа
возвращает число
пример «повторы не считаются дважды»
дано элементы равно [3, 1, 3, 2, 1]
ожидается 6
«Сумма» от («Уникальные» от элементы)Тотальная функция и мера тотальная функция, убывает
«тотальная» значит: компилятор доказал, что функция завершается на любом входе. Для рекурсии он ищет аргумент, который убывает; «убывает б» называет его явно.
модуль «Measure»
тотальная функция «НОД»
принимает а: число, б: число
возвращает число
убывает б
пример «двенадцать и восемнадцать»
дано а равно 12
дано б равно 18
ожидается 6
если б равен 0
то а
иначе «НОД» от б и (а остаток от б)«если» и примеры если … то … иначе, пример
«если» — выражение, у него всегда есть «иначе». Блок «пример» — тест внутри функции: «flang check» вычисляет его и падает с ошибкой, если ответ не совпал.
модуль «Branching»
тотальная функция «Сумма до»
принимает н: неотрицательное
возвращает число
пример «до нуля — ноль»
дано н равно 0
ожидается 0
пример «до трёх — шесть»
дано н равно 3
ожидается 6
если н не больше 0
то 0
иначе н плюс («Сумма до» от (н минус 1))«пусть», объект и запись пусть, объект, запись
«объект» объявляет запись с полями, «запись … с … равным …» её создаёт. «пусть» даёт имя промежуточному значению; переприсваивания нет.
модуль «Binding»
объект «Позиция»
цена является числом
количество является числом
тотальная функция «Стоимость позиции»
принимает позиция: «Позиция»
возвращает число
пример «две штуки по триста»
дано позиция равно запись «Позиция» с цена равным 300 и количество равным 2
ожидается 660
пусть чистое равно позиция.цена умножить на позиция.количество
пусть налог равно 10 процентов от чистое
чистое плюс налогФункция как значение функция из … в …
Функцию можно передать аргументом. «функция «Прибавить» с а равным 10» фиксирует первый аргумент — частичное применение.
модуль «Function as a value»
тотальная функция «Удвоить»
принимает х: число
возвращает число
х умножить на 2
тотальная функция «Прибавить»
принимает а: число, б: число
возвращает число
а плюс б
тотальная функция «Применить дважды»
принимает ф: функция из числа в число, х: число
возвращает число
ф от (ф от х)
тотальная функция «Проба»
возвращает число
пример «пятёрка удвоена дважды»
ожидается 20
«Применить дважды» от функция «Удвоить» и 5
тотальная функция «Проба с захватом»
возвращает число
пример «десятка прибавлена дважды»
ожидается 25
«Применить дважды» от (функция «Прибавить» с а равным 10) и 5Данные
Типы с вариантами тип, вариант, иногда является
«тип» с «вариант» — сумма типов, как enum с данными. «иногда является» делает поле необязательным.
модуль «Types»
объект «Позиция»
название является строкой
цена является числом
скидка иногда является числом
тип «Счёт» это список «Позиция»
тип «Ответ»
вариант Успех содержит значение: число
вариант Отказ содержит причина: строка
тотальная функция «Проверить цену»
принимает позиция: «Позиция»
возвращает «Ответ»
пример «цена есть»
дано позиция равно запись «Позиция» с название равным "болт" и цена равным 30
ожидается вариант Успех с значение равным 30
пример «ноль — не цена»
дано позиция равно запись «Позиция» с название равным "гайка" и цена равным 0
ожидается вариант Отказ с причина равным "цена не положительна"
если позиция.цена больше 0
то вариант Успех с значение равным позиция.цена
иначе вариант Отказ с причина равным "цена не положительна"Разбор по вариантам разбор, случай
«разбор» перебирает варианты типа. Компилятор требует, чтобы были разобраны все, и доказывает завершение рекурсии по структуре.
модуль «Tree»
тип «Дерево»
вариант Лист
вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»
тотальная функция «Узлов»
принимает дерево: «Дерево»
возвращает число
пример «в листе узлов нет»
дано дерево равно вариант Лист
ожидается 0
разбор дерева
случай Лист
то 0
случай вариант Узел с левое как л и правое как п
то 1 плюс («Узлов» от л) плюс («Узлов» от п)Числовые типы сотых, неотрицательное, требует
«число» — обычный double. «неотрицательное», «целое», «сотых» (деньги в копейках) сужают значения, и компилятор опирается на это в доказательствах.
модуль «Exact types»
тотальная функция «Копейки заказа»
принимает цена: сотых, штук: неотрицательное
возвращает число
пример «три по 19.99»
дано цена равно 1999
дано штук равно 3
ожидается 5997
цена умножить на штук
тотальная функция «Доля»
принимает часть: неотрицательное, всего: неотрицательное
возвращает число
требует «делитель положителен» всего больше 0
пример «половина»
дано часть равно 1
дано всего равно 2
ожидается 0.5
часть делить на всегоСтроки строка
Строка в двойных или одинарных кавычках; перевод строки можно писать прямо в литерале.
модуль «Two spellings»
тотальная функция «Через перевод строки»
возвращает строка
пример «то же, что с \n»
ожидается "первая\nвторая"
"первая
вторая"
тотальная функция «Одинарными кавычками»
возвращает строка
пример «те же кавычки, только другие»
ожидается "текст"
'текст'Списки: фильтр и отображение отфильтровать, отобразить, разделить
Встроенные формы над списками: «отфильтровать … где», «отобразить … как», «разделить … по». Циклов в языке нет.
модуль «Built-in forms»
тотальная функция «Длинные слова»
принимает текст: строка
возвращает список строки
пример «короткое слово выброшено»
дано текст равно "раз дважды трижды"
ожидается ["дважды", "трижды"]
отфильтровать (разделить текст по " ") где слово → (длина слово) больше 3
тотальная функция «Длины слов»
принимает слова: список строки
возвращает список числа
пример «три слова»
дано слова равно ["раз", "дважды", "трижды"]
ожидается [3, 6, 6]
отобразить слова как слово → длина словоСвёртка свёртка … начиная с … как
«свёртка» — reduce: один проход по списку с накопителем.
модуль «Fold»
тотальная функция «Произведение»
принимает элементы: список числа
возвращает число
пример «три множителя»
дано элементы равно [2, 3, 4]
ожидается 24
свёртка элементы начиная с 1 как акк и эл → акк умножить на элДоказательства
Предусловие требует
«требует» — условие на входы. Вызывающий код обязан его выполнить, а тело функции может на него опираться.
модуль «Precondition»
тотальная функция «Доля»
принимает часть: неотрицательное, всего: неотрицательное
возвращает число
требует «делитель положителен» всего больше 0
пример «половина»
дано часть равно 1
дано всего равно 2
ожидается 0.5
часть делить на всегоПостусловие обеспечивает
«обеспечивает» — обещание о результате для всех входов. «flang check --proof» говорит, доказано оно или нет.
модуль «Postcondition»
тотальная функция «Удвоить все»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «длина сохраняется» (длина результат) равен (длина элементы)
пример «три элемента»
дано элементы равно [1, 2, 3]
ожидается [2, 4, 6]
отобразить элементы как э → э умножить на 2Свойство каждого элемента для всех … из …:
«для всех п из результат: …» — обещание о каждом элементе списка.
модуль «For all after a filter»
тотальная функция «Только положительные»
принимает элементы: список числа
возвращает список числа
обеспечивает «все положительны» для всех п из результат: п больше 0
пример «Смесь»
дано элементы равно [3, 0, 5]
ожидается [3, 5]
отфильтровать элементы где э → э больше 0Утверждение утверждение
«утверждение» — свойство вне функции: о конкретных значениях или «для всех» значений типа.
модуль «Free statements»
утверждение «длина пустого списка нулевая»
утверждаем (длина пустой список) равен 0
утверждение «ноль нейтрален при сложении»
для всех н: неотрицательное таких что н больше 0
утверждаем (н плюс 0) равен нТеорема теорема, индукция по, по предположению
Когда компилятор не выводит обещание сам, доказательство пишут теоремой: индукция, случаи и обоснование каждого шага.
модуль «Theorem»
тотальная функция «Сумма до»
принимает н: неотрицательное
возвращает число
для всех н обеспечивает «сумма до неотрицательна» результат не меньше 0
пример «шагов не осталось»
дано н равно 0
ожидается 0
если н не больше 0
то 0
иначе н плюс («Сумма до» от (н минус 1))
теорема «сумма до неотрицательна»
дано н: неотрицательное
утверждаем результат не меньше 0
индукция по н убывает н
случай 0
то по примеру «шагов не осталось»
случай любое
то по предположению
следовательно доказаноОпора на доказанное по свойству
«по свойству» ссылается на уже доказанное обещание другой функции.
модуль «Property»
тотальная функция «Удвоить все»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «удвоение длины не меняет» (длина результат) равен (длина элементы)
отобразить элементы как э → э умножить на 2
тотальная функция «Через удвоение»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «через удвоение длина та же» (длина результат) равен (длина элементы)
«Удвоить все» от элементы
теорема «через удвоение длина та же»
дано элементы: список числа
утверждаем (длина результат) равен (длина элементы)
по свойству «удвоение длины не меняет»
следовательно доказаноИндукция по своему типу индукция по своему типу
Индукция работает по любому объявленному типу с вариантами, а не только по числам.
модуль «Own natural»
тип «Нат»
вариант «Ноль»
вариант «Следующий» содержит пред: «Нат»
тотальная функция «К числу»
принимает н: «Нат»
возвращает число
разбор н
случай вариант «Ноль»
то 0
случай вариант «Следующий» с пред как п
то («К числу» от п) плюс 1
утверждение «шаг растит счёт на один»
для всех н: «Нат»
утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
теорема «шаг растит счёт на один»
дано н: «Нат»
утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
индукция по н
случай вариант «Следующий» с пред как п
то по предположению
следовательно доказаноПроцессы
Процесс и надзор процесс, надзор, прогон
«процесс» хранит состояние и обрабатывает сообщения чистой функцией, «надзор» перезапускает его при сбоях, «прогон» — тест последовательности сообщений.
модуль «Counter»
объект «Счёт»
«всего»: число
объект «Отклик»
«состояние»: «Счёт»
«действия»: список «Действие»
тип «Команда»
вариант «прибавить» содержит «сколько»: число
процесс «Счётчик»
состояние «Счёт»
начинает с «пустой счёт»
принимает «Команда»
обрабатывает «шаг счёта»
надзор «Учёт»
процесс «Счётчик» стратегия «перезапустить»
порог отказов 3 за 5000 миллисекунд иначе «передать выше»
тотальная функция «пустой счёт»
возвращает «Счёт»
запись «Счёт» с «всего» равным 0
тотальная функция «шаг счёта»
принимает текущее: «Счёт», сообщение: «Команда»
возвращает «Отклик»
пример «прибавление меняет состояние и ничего не шлёт»
дано текущее равно (запись «Счёт» с «всего» равным 1)
дано сообщение равно (вариант «прибавить» с «сколько» равным 2)
ожидается (запись «Отклик» с «состояние» равным (запись «Счёт» с «всего» равным 3) и «действия» равным [])
разбор сообщение
случай вариант «прибавить» с «сколько» как сколько
пусть новое равно (запись «Счёт» с «всего» равным (текущее.«всего» плюс сколько))
запись «Отклик» с «состояние» равным новое и «действия» равным []
прогон «два прибавления»
семя 1
дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)