Операции языка: что чем делается

Словарь отвечает на вопрос «что значит это слово». Здесь другой вопрос: «у меня список, мне нужна сумма без повторов — что писать».

Весь код этой страницы лежит одним файлом docs/examples/operations.flang и прогоняется целиком:

flang test docs/examples/operations.flang

docs/examples/operations.flang: примеров 254, прошло 254, не прошло 0

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

Подключить модуль

использует — это импорт. Модуль подключается по имени, путь писать не нужно:

модуль «Операции»
  использует «Lists»
  использует «Strings»
  использует «String sets»
  использует «String lists»
  использует «Numbers»

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

FLANG_IMPORT_NOT_FOUND в файле imp1.flang, строка 1, столбец 1: не найден модуль «Множества»: ни рядом с файлом, ни выше по каталогам, ни в библиотеке компилятора

Подключили путём, а имя переврали — отказ называет оба имени:

FLANG_IMPORT_NAME, строка 1, столбец 1: модуль в /путь/sets.flang называется «Множество строк», а импортируется как «Множества»

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

  использует «Lists» только «Двоичный поиск»

FLANG_UNKNOWN_NAME, строка 569, столбец 3: неизвестная функция «Поиск в диапазоне»
FLANG_NOT_TOTAL, строка 569, столбец 3: тотальная функция «Двоичный поиск» вызывает неизвестную функцию «Поиск в диапазоне»: завершение доказать нельзя

Допишите недостающее имя через запятую — или подключайте модуль целиком.

Откуда берутся операции

Слов у языка мало, и это намеренно: плюс, минус, умножить на, делить на, остаток от, равно, не меньше, если … то … иначе, свёртка, разбор … случай. Всё остальное — функции библиотеки, написанные на самом flang и лежащие в flang/stdlib/:

Lists

Задача: сумма без повторов.

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

Ответ 6, а не 10: повторы выброшены до сложения. Проверяет это пример внутри самой функции — исполняемый тест, который едет вместе с объявлением.

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

тотальная функция «Третий по порядку»
  принимает элементы: список числа
  возвращает число
  обеспечивает «результат не меньше минимума» результат не меньше («Минимум» от элементы)
  пример «Нумерация с единицы: третий из [1, 4, 5, 9] — это 5»
    дано элементы равно [5, 4, 9, 1]
    ожидается 5
  «Элемент» от («Сортировать» от элементы) и 3

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

Strings

Задача: сколько слов в строке.

тотальная функция «Слов в строке»
  принимает текст: строка
  возвращает число
  пример «Три слова через пробел»
    дано текст равно "раз два три"
    ожидается 3
  «Длина» от («Разбить по символу» от текст и " ")

flang run docs/examples/operations.flang \
  --function "Слов в строке" --args '{"текст": "раз два три"}'

3

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

Задача: взять кусок пути. Строка — не список: у неё свой модуль. «Разбить по символу» даёт список строк, и дальше работают функции модуля «Списки строк», а не «Списки»:

тотальная функция «Код из адреса»
  принимает адрес: строка
  возвращает строка
  пример «Хвост после последней косой»
    дано адрес равно "/с/абв"
    ожидается "абв"
  «Строка по номеру» от («Разбить по символу» от адрес и "/") и 3 и ""

flang run docs/examples/operations.flang \
  --function "Код из адреса" --args '{"адрес": "/с/абв"}'

"абв"

Третий аргумент — запасное значение: что вернуть, если номера нет. Его нельзя не написать, и в этом смысл.

Множества

Множество — это список строк без повторов; отдельного типа нет, есть модуль, который держит инвариант.

Задача: сколько меток общих у двух наборов.

тотальная функция «Общих меток»
  принимает первые: список строки, вторые: список строки
  возвращает число
  обеспечивает «общих не больше, чем в первом наборе» результат не больше («Размер множества» от («Из списка» от первые))
  пример «Две метки общие»
    дано первые равно ["а", "б", "в"]
    дано вторые равно ["б", "в", "г"]
    ожидается 2
  «Размер множества» от («Пересечение» от («Из списка» от первые) и («Из списка» от вторые))

Numbers

Четыре функции модуля «Числа» из шестнадцати объявлены без признака тотальная — «НОД», «НОК», «Цифры», «Сумма цифр». Это не недоделка, а честная подпись: и Евклид, и разбор числа на цифры убывают по ВЕЛИЧИНЕ числа («Целочисленное деление» от число и 10), а не по его структуре, и спуском по части значения такое завершение не доказывается.

Задача: сколько страниц под N записей. Округление вверх пишется через целочисленное деление и проверку на ноль — иначе функция не была бы тотальной:

тотальная функция «Страниц под записи»
  принимает записей: число, размер: число
  возвращает число
  пример «Двадцать три записи по десять»
    дано записей равно 23
    дано размер равно 10
    ожидается 3
  если размер не больше 0
    то 0
    иначе «Целочисленное деление» от (записей плюс размер минус 1) и размер

flang run docs/examples/operations.flang \
  --function "Страниц под записи" --args '{"записей": 23, "размер": 10}'

3

Ветка если размер не больше 0 стоит не ради аккуратности: без неё деление на ноль дало бы бесконечность, а функция обещает число.

Как передать аргументы: --args

Аргументы едут одним ключом, и он берёт JSON-объект: ключ — имя параметра, как оно написано в принимает; значение — само значение.

Список и запись через --args не проезжают, и это граница, а не описка. Ключ берёт ПЛОСКИЙ объект скаляров — число, строку, true, false, null:

flang run docs/examples/operations.flang \
  --function "Сумма без повторов" --args '{"элементы": [3, 1, 3, 2, 1]}'

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

Отказ уходит в поток ошибок, код возврата 2. Сам язык такие значения принимает — просто через --args их сегодня не передать.

Составное значение передают оболочкой: там оно пишется словами языка, а не JSON-ом, и читает его сам компилятор:

echo '«Сумма без повторов» от [3, 1, 3, 2, 1]' | flang repl docs/examples/operations.flang

объявлено: тотальная функция «Сумма без повторов» — завершение доказано
объявлено: тотальная функция «Третий по порядку» — завершение доказано
объявлено: тотальная функция «Слов в строке» — завершение доказано
объявлено: тотальная функция «Код из адреса» — завершение доказано
объявлено: тотальная функция «Общих меток» — завершение доказано
объявлено: тотальная функция «Страниц под записи» — завершение доказано
загружено из docs/examples/operations.flang
6

Что говорит про этот файл отчёт о доказательствах

flang check docs/examples/operations.flang --proof

Итог отчёта; выше него он называет каждую функцию и каждое утверждение поимённо:

итог:
  функций 115: тотальных 111, обычных 4
  обещание несёт: композиция 95, структура 11, точный шаг 3, постоянный шаг 2, объявленная мера 0
  сторожей в рантайме: 2 места
  законов на сетке: 0 (значений в сетках 0); на веру: 0
  утверждений 238: доказано 101 (из них индукцией 7) (из них без теоремы 93), сетка 137, объявлено, не доказано 0 (шагов в термах 2)

Слово «сетка» отчёт объясняет сам, в своей же шапке: «посчитано на N значениях автора, нарушений не найдено; это НЕ доказательство». То есть утверждение проверено на тех входах, что автор написал в примерах, и только на них.

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

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

Все 101 доказанное утверждение пришли из библиотеки, подключённой этим файлом, а не написаны здесь. Написать постусловие легко, а получить под него доказательство — отдельная работа, и компилятор не делает вид, что она сделана. Чем это обходится и когда получается — на странице Зачем и как.

Что дальше

• Словарь языка — 150 понятий, печатается из таблицы поверхностей
• Справочник библиотеки — все модули с подписями функций
• Как писать пакеты — когда операций перестаёт хватать
• Разборы настоящих случаев — те же операции на 82 задачах и службе