flang — язык с доказуемым завершением Старые модели: что компилятор делает с прежней поверхностью
0%

Старые модели: что компилятор делает с прежней поверхностью

Старые модели: что компилятор делает с прежней поверхностью

Эта глава нужна тому, у кого лежат файлы ранней поверхности языка — со словами категория, объект, утилита, правило, свойство. Если таких файлов у вас нет, главу можно пропустить.

Что происходит, когда такой файл отдают компилятору

Возьмём модель скидки из песочницы курса, order-discount.fts: категория «Продажи», объект «Покупка», утилита «Рассчитать скидку» с тремя правилами, свойством и пятью примерами. На flang 0.7.29:

$ flang check order-discount.fts
модуль «Продажи»: функций 0, из них с доказанным завершением 0; типов 1
order-discount.fts: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ echo $?
0

Ответ «замечаний нет» легко прочитать неверно. Посмотрите на первую строку: функций ноль. Из файла взято вот что:

  • категория «Продажи» стала именем модуля;
  • объект Покупка стал записью с типами полей, и типы проверяются: если написать у поля несуществующий тип, будет FLANG_UNKNOWN_NAME и код 1;
  • утилита, её правила, свойство и примеры легли в дерево разбора отдельными узлами ftsLegacy (их видно в выводе flang ast order-discount.fts, раздел legacy), но не исполняются.

Последнее проверяется одной правкой. Замените в примере «Постоянный клиент на пять тысяч» ожидание 250 на 999 — flang check ответит тем же «замечаний нет» и кодом 0. Примеры старой поверхности не прогоняются: flang test на том же файле, переименованном в .flang, печатает примеров 0.

Вывод: flang check на файле .fts подтверждает только, что текст разбирается и типы полей существуют. О правилах он не говорит ничего.

Почему нет команды «перевести автоматически»

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

Утилита старой поверхности считала на динамических данных: поля приходили объектом, их наличие проверялось во время исполнения, отсутствие поля давало диагностику. Функция flang требует типов при сборке, и то, что раньше было ответом рантайма («во входных данных нет поля «сумма»»), становится ошибкой компиляции или не возникает вовсе. Автоматический перевод был бы вынужден что-то додумать — типы полей, поведение на отсутствующем поле, границы чисел, — и додуманное выглядело бы перенесённым. Поэтому перенос ручной.

Таблица соответствий

Прежняя поверхность Сегодняшний flang Что меняется по существу
категория «Продажи» модуль «Продажи» то же имя, но теперь это модуль
объект «Покупка» с полями тип «Покупка» — запись с типами полей типы полей обязательны и проверяются при сборке
утилита «Рассчитать скидку» тотальная функция «Рассчитать скидку» появляется обязанность доказать завершение
правило внутри утилиты тело функции: если … то … иначе …, разбор … случай … ветвление становится выражением со значением
свойство «…» обеспечивает «…» <утверждение> утверждение проверяет и пытается доказать компилятор
пример … ожидается … пример … дано … ожидается … форма почти та же, но теперь пример исполняется

Так выглядит та же модель скидки после переноса (два примера из пяти):

модуль «Продажи»

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

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «Скидка ограничена» результат не больше 15000
  пример «Постоянный клиент на пять тысяч»
    дано покупка равно «Покупка» с сумма равным 5000 и постоянный равным да
    ожидается 250
  пример «Очень крупная покупка»
    дано покупка равно «Покупка» с сумма равным 200000 и постоянный равным нет
    ожидается 15000
  пусть сумма равно покупка.сумма
  если сумма больше 100000
    то 15000
    иначе
      пусть большая равно если сумма не меньше 10000 то сумма умножить на 0.1 иначе 0
      пусть постоянному равно если покупка.постоянный и притом (сумма больше 0) то сумма умножить на 0.05 иначе 0
      большая плюс постоянному
$ flang test port.flang
port.flang: примеров 2, прошло 2, не прошло 0

Теперь неверное ожидание 999 даёт не прошёл: … ожидалось 999, получено 250 и код 1. Постусловие «Скидка ограничена» при этом не доказано: flang check --proof честно пишет, что оно держится только на двух значениях из примеров.

Примеры — главный инструмент переноса: перенесли утилиту, перенесли её примеры, flang test их прогнал — значит, поведение сохранилось там, где оно описано.

Коды диагностик с приставкой FTS_

У постусловия обычной функции flang код нарушения — FLANG_PROPERTY. Код FTS_UTILITY_PROPERTY закреплён за свойством утилиты старой поверхности; он записан в рантаймах целевых языков (flang/src/emit/*/ в репозитории языка). Встретили FTS_ в выводе — дело в конструкции старой поверхности. Перепишете модель по таблице — коды станут обычными FLANG_*.

Что от ранней поверхности осталось в языке

Три решения пережили переписывание компилятора:

  • Имена в ёлочках. «Рассчитать скидку» вместо calculateDiscount: правило называется так, как его называют в предметной области.
  • Несколько наборов слов. Сегодня их четыре — русский, английский, эсперанто и китайский, — и все дают одно дерево разбора (глава «Своя поверхность»).
  • Примеры внутри функции. Тест лежит рядом с кодом.

Остальное — типы, доказательство завершения, постусловия, перевод в другие языки, ввод-вывод — появилось уже в flang.

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

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

Доска запросов
Дальше