Справочник отказов

Компилятор отказывает кодом. Код всегда стоит первым словом строки:

FLANG_TYPE в файле type.flang, строка 6, столбец 3: функция «Удвоить» объявлена как число, а тело даёт строка

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

Коды возврата: 0 — проверено, 1 — есть замечания, 2 — кривой вызов.

Три ловушки, которые стоят дня

Прочитайте их до того, как начнёте искать свой код. Каждая даёт отказ не там, где ошибка.

Постусловие, зовущее функцию своего же модуля, ломает тех, кто ввозит модуль списком

Файл зелёный у себя. Ввозящий падает.

// ядро.flang
модуль «Ядро»

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

тотальная функция «Учтено»
  принимает н: число
  возвращает число
  обеспечивает «не меньше двойки» результат не меньше («Двойка» от н)
  («Двойка» от н) плюс 1

// ввоз.flang
модуль «Ввоз»
использует «Ядро» только «Учтено»

тотальная функция «Проба»
  принимает н: число
  возвращает число
  «Учтено» от н

flang check ядро.flang

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

flang check ввоз.flang

модуль «Ввоз»: функций 2, из них с доказанным завершением 0; типов 0; файлов вместе с импортами 2
без доказанного завершения: «Учтено» «Проба»
FLANG_UNKNOWN_NAME, строка 12, столбец 4: неизвестная функция «Двойка»
FLANG_UNKNOWN_NAME, строка 11, столбец 50: неизвестная функция «Двойка»
FLANG_NOT_TOTAL, строка 12, столбец 4: тотальная функция «Учтено» вызывает неизвестную функцию «Двойка»: завершение доказать нельзя
ввоз.flang: не проверено — замечаний 3

Ввоз только «Учтено» приводит одно имя. Тело и постусловие «Учтено» зовут «Двойку», которой в ввозящем нет. Столбец 50 указывает внутрь постусловия — строка та же, что и в исходном модуле, а файл не назван: проверено два файла.

Что делать — одно из трёх:

Зелёный вывод не значит, что утверждения доказаны

flang check без ключей проверяет разбор, типы, завершаемость и примеры. Постусловие, которое он не сумел ни доказать, ни опровергнуть, он пропускает молча. Постусловие «меньше двойки» из примера выше ложно — файл зелёный.

Спрашивайте прямо:

flang check ядро.flang --proof

  постусловие «меньше двойки» функции «Учтено» — объявлено, не доказано: ни теоремы, ни примеров. Его считает рантайм после каждого возврата — на тех входах, которые придут

Читайте слова буквально: «доказано» — обо всех входах; «сетка N» — посчитано на N значениях, доказательством не является; «объявлено, не доказано» — утверждение высказано, за ним ничего нет.

И второе: пока в проверке стоит FLANG_UNKNOWN_NAME, функция теряет обещание тотальная и её утверждения не доказывает никто. Сначала имена, потом всё остальное.

FLANG_BOUND_ON_NAN: «не число» живёт в типе число и стоит вне порядка

Самый частый ложный испуг. Утверждение выглядит очевидно верным, а ядро отвечает контрпримером.

модуль «Проба»

тотальная функция «Прибавить один»
  принимает н: число
  возвращает число
  обеспечивает «результат больше довода» результат больше н
  н плюс 1

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

Причина: тип число содержит «не число», всякая арифметическая операция его переносит, а сравнение с ним ложно в обе стороны. Утверждение о порядке над сырой арифметикой поэтому неверно.

Разбор

модуль «Проба»

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

FLANG_PARSE в файле parse.flang, строка 7, столбец 1: у 'если' нет ветки 'иначе'

FLANG_LEX в файле lex.flang, строка 5, столбец 3: не закрыта кавычка

Имена и ввоз

модуль «Проба»

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

FLANG_UNKNOWN_NAME в файле unknown.flang, строка 6, столбец 3: неизвестная функция «Утроить»
FLANG_NOT_TOTAL в файле unknown.flang, строка 6, столбец 3: тотальная функция «Удвоить» вызывает неизвестную функцию «Утроить»: завершение доказать нельзя

Незнакомое имя всегда тянет за собой второй отказ про завершаемость. Чините первый — второй уходит сам.

Если имя написано как действие, компилятор скажет об этом прямо:

FLANG_UNKNOWN_NAME в файле pr4.flang, строка 10, столбец 14: имя «м» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»

Типы

FLANG_TYPE в файле type.flang, строка 6, столбец 3: функция «Удвоить» объявлена как число, а тело даёт строка

FLANG_TYPE в файле dup.flang, строка 8, столбец 1: функция «Удвоить» объявлена дважды

FLANG_MATCH_NOT_EXHAUSTIVE в файле match.flang, строка 6, столбец 3: разбор списка не покрывает «пусто»

FLANG_EXAMPLE: пример «Двойка» функции «Удвоить»: значение не совпало с ожидаемым: ожидалось 5, получено 4

Завершаемость и пределы

модуль «Проба»

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

FLANG_NOT_TOTAL в файле total.flang, строка 6, столбец 30: тотальная функция «Считать»: рекурсивный вызов «Считать» не убывает — аргумент 1 («н» add 1) увеличивает параметр «н». Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции

flang run rec.flang --function "Вниз" --args '{"н":100}' --max-steps 5

FLANG_RECURSION_LIMIT: функция «Вниз» исчерпала лимит шагов (5) на глубине вызовов 1

Утверждения и доказательство

Требования, обещания и теоремы.

модуль «Проба»

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

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

FLANG_PROOF_STEP: теорема «удвоенное неотрицательно»: ни одного шага

FLANG_PROOF_NO_GOAL в файле pr1.flang, строка 9, столбец 1: теорема «удвоенное неотрицательно» ничего не закрывает: постусловия «удвоенное неотрицательно» нет ни у одной функции модуля. Теорема доказывает названное утверждение, а не утверждение вообще — назовите её так же, как постусловие, которое она закрывает

FLANG_PROOF_AMBIGUOUS в файле pa.flang, строка 15, столбец 1: теорема «неотрицательно» закрывала бы сразу 2 постусловия («Удвоить», «Утроить»), и выбрать нельзя. Дайте постусловиям разные имена

FLANG_PROOF_CLAIM_MISMATCH в файле pm.flang, строка 11, столбец 3: теорема «неотрицательно» утверждает не то, что обещает функция «Удвоить»: утверждение теоремы и постусловие обязаны совпадать слово в слово. Ядро не решает, что два разных утверждения означают одно и то же

Постусловие, пропущенное проверкой, считает рантайм:

flang run prop.flang --function "Половина" --args '{"н":0}'

FLANG_PROPERTY: нарушено свойство «результат меньше довода» функции «Половина»

Законы объявленных структур

Эти законы компилятор СЧИТАЕТ на конечной сетке значений автора, а не доказывает. Отказ означает найденное нарушение — контрпример есть всегда.

Поручения и ввод-вывод

Отказы команды flang io. План возвращает ОПИСАНИЕ действия, а делает его хозяин; коды семейства FLANG_IO_* говорят, что хозяин делать отказался.

Полномочия сужаются по одному, умолчание — «можно всё»:

flang io план.flang --plan 'Разбор' --no-net --in-dir

Процессы

Командная строка и внутреннее

flang check --неткого

flang check: непонятный ключ «--неткого»

Код возврата — 2.

Дальше: Ядро отказало: чья это ошибка — как читать отказ доказательства и когда виноват не автор.