⚠️ УСТАРЕЛО (DEPRECATED)
Данный RFC заменён RFC-027: Типы времени компиляции и унифицированная статическая верификация.
Причина устаревания: RFC-022 проектировал спецификации как внешний синтаксис в форме //! комментариев, что противоречит фундаментальному принципу изоморфизма Карри-Ховарда — «Нет комментариев //!. Нет отдельного языка спецификаций. Всё внутри системы типов». Новая разработка делает типы времени компиляции гражданами первого класса и заменяет аннотационные спецификации единым конвейером вычисления Bool на этапе компиляции. Модель разделённой верификации Debug/Release также заменена унифицированной трёхуровневой моделью возвращаемых значений True/False/Unknown.
Данный документ сохраняется только для исторической справки.

RFC 022: Поддержка статической верификации по логике Хоара (спецификационные комментарии и типы спецификаций) [Устарел]

Ссылки:
RFC-010: Унифицированный синтаксис типов
RFC-011: Проект системы обобщённых типов
RFC-009: Модель владения

Резюме

Данный документ предлагает ввести в язык YaoXiang механизм статической верификации по логике Хоара, позволяющий разработчикам записывать предусловия, постусловия и инварианты циклов в форме комментариев //! или /*! ... !*/. В режиме Debug Build выполняется принудительная статическая верификация, и только после её успешного прохождения возможен Release Build; в режиме Release Build спецификационные комментарии игнорируются (нулевые накладные расходы) и кэш верификации очищается. Сами спецификации рассматриваются как часть системы типов, формируя «типы спецификаций» (например, Requires(P), Ensures(P)), которые могут быть расширены пользователем. Данный проект направлен на сохранение простоты языка при обеспечении высокой надёжности критичного кода и идеально согласуется с унифицированной моделью типов YaoXiang.

Мотивация

Зачем нужна эта функциональность/изменение?

YaoXiang уже обеспечивает безопасность памяти и потоков через модель владения (RFC-009) и модель параллелизма (RFC-001), однако логическая корректность по-прежнему зависит от тестирования. Для системного программирования и критически важных областей (таких как аэрокосмическая отрасль, финансы, ядра операционных систем) логические ошибки могут привести к катастрофическим последствиям. Существующие решения (например, проверка заимствований в Rust) не способны выявлять подобные ошибки. Логика Хоара предоставляет математический инструмент доказательства, однако традиционные средства формальной верификации часто требуют отдельного языка спецификаций и имеют крутую кривую обучения.

Текущие проблемы

Логическая корректность может быть проверена только тестированием и не гарантируется на этапе компиляции
В критичном системном коде отсутствуют средства формальной верификации
Существующие средства формальной верификации имеют крутую кривую обучения и изолированы от主流ных языков программирования

Предложение

Основной проект

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

Обязательная верификация в Debug Build: разработчики пишут спецификации в модулях, требующих высокой надёжности; в Debug Build принудительно выполняется верификация, и только после её успешного прохождения возможен Release Build
Элегантный синтаксис: используются комментарии //!, без введения новых ключевых слов, с возможностью подсветки в редакторе
Интеграция с системой типов: спецификации становятся частью типов, участвуют в проверке типов, допускают пользовательские типы спецификаций
Доказуемость и тестируемость: возможно как статическое доказательство, так и понижение до runtime-assertion для постепенного внедрения

1. Синтаксис спецификационных комментариев

В начале тела функции или цикла спецификации записываются с помощью //! (однострочный) или /*! ... !*/ (многострочный).

1.1 Унифицированный синтаксис спецификаций

Спецификации используют унифицированную модель синтаксиса YaoXiang name: Type = expression и полностью интегрированы с системой типов:

yaoxiang

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0
    //! ensures: GreaterOrEqual(result, arr[0..n])
    //! ensures: ExistsMax(result, arr[0..n])
    // реализация...
}

Спецификация по существу является объявлением типа, в правой части которого находится булево выражение
Слева находится экземпляр типа спецификации (возможно с параметрами типа)
Допускается использование специальной переменной result для обозначения возвращаемого значения

1.2 Спецификации циклов

yaoxiang

while i < n {
    /*! invariant: Bounds[i, n] = 0 <= i <= n
                  && SumInvariant[s, arr[0..i]] !*/
    s = s + arr[i]
    i = i + 1
}

1.3 Выражения спецификаций

В правой части спецификации используется синтаксис выражений YaoXiang, поддерживающий:

Арифметические операции, операции сравнения, логические операции
Кванторы: forall i in 0..n: P(i), exists i in 0..n: P(i) — встроенные логические конструкции языка
Вызовы функций (только чистых функций)

2. Система типов спецификаций

Типы спецификаций по существу являются обычными типами YaoXiang и полностью согласуются с унифицированной моделью синтаксиса.

2.1 Встроенные типы спецификаций

Компилятор имеет встроенные следующие часто используемые типы спецификаций (могут использоваться непосредственно в спецификациях):

yaoxiang

// Определения встроенных типов спецификаций
NonEmpty: (T: Type) -> Type = { len: T; len > 0 }
Positive: Type = { x: Int; x > 0 }
GreaterOrEqual: (T: Type) -> Type = { result: T, arr: Array(T); result >= arr[0] && forall i in 1..arr.len: result >= arr[i] }
Bounds: (T: Type) -> Type = { i: T, n: T; 0 <= i && i <= n }
SumInvariant: (T: Type) -> Type = { s: T, arr: Array(T); s == sum(arr[0..i]) }

// Кванторные конструкции (встроены в язык, не являются функциями)
forall: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool
exists: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool

2.2 Пользовательские типы спецификаций

Полностью аналогично обычному определению типов, пользователь может определять собственные типы спецификаций:

yaoxiang

// Определение спецификации положительного целого числа
Positive: Type = { x: Int; x > 0 }

// Определение спецификации отсортированного массива
Sorted: (T: Ord) -> Type = {
    arr: Array(T);
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

// Определение спецификации максимального значения
ExistsMax: (T: Ord) -> Type = {
    result: T, arr: Array(T);
    exists i in 0..arr.len: result == arr[i]
    && forall j in 0..arr.len: result >= arr[j]
}

Использование пользовательских спецификаций:

yaoxiang

sqrt: (x: Positive) -> Float = {
    //! ensures: SquareRootResult(result, x) = result * result <= x && (result+1)*(result+1) > x
    // реализация...
}

binary_search: (T: Ord) -> ((arr: Sorted(Array(T)), key: T) -> Option(Index)) = {
    //! ensures: SearchResult(result, arr, key)
    // реализация...
}

Типы спецификаций, как и другие типы, поддерживают параметры обобщённых типов, ограничения типов и могут участвовать в выводе типов.

3. Режимы компиляции

Режим	Поведение	Опция
Debug Build	Разбор спецификаций, генерация условий верификации, вызов SMT-решателя для доказательства; только после успешной верификации возможен Release Build	`yaoxiangc --debug source.yx`
Release Build	Все комментарии `//!` игнорируются, никакой код не генерируется; очищается весь кэш верификации; применяются агрессивные оптимизации	`yaoxiangc --release source.yx`
Проверка во время выполнения	Спецификации преобразуются в runtime-assertion, при нарушении вызывается panic	`yaoxiangc --enable-runtime-checks source.yx`

В режиме верификации, если доказательство не удаётся, компилятор сообщает об ошибке и предоставляет возможный контрпример (например, значения входных данных).

4. Механизм верификации

Компилятор преобразует спецификации в условия верификации (Verification Conditions, VC) и отправляет их интегрированному SMT-решателю (например, Z3). Процесс верификации в общих чертах:

Собираются requires и ensures функций, invariant циклов
Для каждого цикла генерируются обязательства доказательства инварианта: выполнение до входа в цикл, сохранение после каждой итерации, импликация постусловия после выхода из цикла
Тело функции преобразуется в логическую формулу, которая вместе со спецификациями формирует условие верификации
Вызывается SMT-решатель для проверки выполнимости

Если решатель возвращает unsat (невыполнимо), спецификация выполняется; в противном случае сообщается контрпример.

5. Интеграция с тестированием

В режиме проверки во время выполнения спецификации могут быть преобразованы в assertion для тестирования. В сочетании с инструментами оценки покрытия спецификаций возможна оценка того, насколько тесты покрывают спецификации. В будущем возможны инструменты для выявления спецификаций, автоматически выводящие кандидатные спецификации из тестов.

6. Поддержка редакторов

Комментарии //! и /*! ... !*/ могут распознаваться редакторами как специальные комментарии с выделением другим цветом (например, фиолетовым) для отличия от обычных комментариев. Языковой сервер может предоставлять подсказки при наведении, автодополнение и сообщения об ошибках верификации для спецификаций.

Детальный проект

Изменения синтаксиса

До	После
Отсутствие синтаксиса спецификационных комментариев	Допускаются спецификационные комментарии `//!` и `/! ... !/`

7.1 Расширение синтаксиса

На основе существующего синтаксиса (RFC-010) разрешается использование нуля или более комментариев //! или /*! ... !*/ в начале тела функции или цикла. Синтаксис спецификаций согласуется с унифицированным синтаксисом типов:

spec_comment     ::= ('//!' spec_line) | ('/*!' spec_block '!*/')
spec_line        ::= spec_name ':' type_expr '=' expr
spec_name        ::= 'requires' | 'ensures' | 'invariant'
spec_block       ::= (spec_name ':' type_expr '=' expr ';')*

Спецификация по существу является объявлением типа: имя_спецификации: тип_спецификации = булево_выражение
type_expr — выражение типа спецификации, возможно с параметрами типа
expr использует синтаксис выражений YaoXiang с поддержкой кванторов

7.2 Проверка типов

В режиме верификации компилятор преобразует спецификационные комментарии в соответствующие экземпляры типов спецификаций и записывает их в метаданные функций или циклов.

7.3 Генерация условий верификации

Используется вычисление weakest precondition или strongest postcondition в сочетании с инвариантами циклов для генерации формул логики первого порядка. Сгенерированные VC представляются в формате SMT-LIB и передаются внешнему решателю.

7.4 Сообщения об ошибках

В случае неудачи доказательства решатель может предоставить модель (контрпример). Компилятор должен преобразовать эти контрпримеры в читаемую форму, например, в виде конкретных значений входных данных, для помощи в отладке.

7.5 Проверка во время выполнения

В режиме --enable-runtime-checks компилятор преобразует спецификации в операторы assert:

requires: вставка assert(cond) в начале функции
ensures: вставка assert(cond) перед всеми точками возврата функции, где result заменяется фактическим возвращаемым значением
invariant: вставка assert(cond) в начале тела цикла

7.6 Интеграция с существующим проектом

Модель владения: выражения в спецификациях подчиняются правилам владения, допускают только чтение, но не запись (чистые функции), что исключает побочные эффекты
Система обобщённых типов: типы спецификаций поддерживают параметры обобщённых типов (например, Requires(P)) и могут сочетаться с обобщёнными функциями/типами
Зависимые типы: значения в спецификациях, зависящие от типов (например, длина массива n), естественно доступны

Влияние на систему типов

Типы спецификаций являются обычными типами YaoXiang и согласуются с унифицированной моделью синтаксиса
Компилятор имеет встроенные часто используемые типы спецификаций (Positive, NonEmpty, GreaterOrEqual и т.д.)
Пользователи могут определять собственные типы спецификаций посредством обычных определений типов
Типы спецификаций могут иметь параметры обобщённых типов и поддерживать ограничения типов

Поведение во время выполнения

Debug Build: вызов SMT-решателя для статической верификации, увеличение времени компиляции; после успешной верификации результат кэшируется
Release Build: спецификационные комментарии игнорируются, нулевые накладные расходы во время выполнения; очищается весь кэш верификации; применяются агрессивные оптимизации, такие как очистка Span-кэша
Режим проверки во время выполнения: генерация операторов assert, обнаружение нарушений во время выполнения

Изменения в компиляторе

Парсер: распознавание синтаксиса спецификационных комментариев
Семантический анализ: сбор спецификаций и их преобразование в типы спецификаций
Бэкенд верификации: генерация условий верификации, вызов SMT-решателя
Генерация кода: поддержка режима проверки во время выполнения

Обратная совместимость

✅ Полностью обратно совместимо
Спецификационные комментарии игнорируются при обычной компиляции и не влияют на существующий код
В Release Build спецификации игнорируются без дополнительных накладных расходов

Компромиссы

Преимущества

Верификация в Debug Build: принудительная верификация в Debug Build обеспечивает логическую корректность
Элегантный синтаксис: чистые комментарии, без новых ключевых слов, удобство для редакторов
Интеграция с системой типов: спецификации как типы, возможность расширения
Постепенное внедрение: возможен постепенный переход от проверки во время выполнения к статической верификации
Повышение надёжности: способность обнаруживать логические ошибки, которые сложно выявить тестированием

Недостатки

Время компиляции: режим верификации может существенно увеличить время компиляции
Кривая обучения: необходимость изучения методов написания эффективных спецификаций и кванторов
Ограничения SMT-решателей: некоторые сложные свойства не могут быть автоматически доказаны

Альтернативы

Подход	Преимущества	Недостатки
Новые ключевые слова (например, `requires`)	Интуитивный синтаксис	Вводит новые ключевые слова, нарушает простоту
Отдельные файлы спецификаций (например, CVL)	Разделение спецификаций и кода	Увеличивает количество файлов, сложно синхронизировать
Только runtime-assertion	Простота реализации	Не обеспечивает статических гарантий
Данный подход (комментарии + типы спецификаций)	Баланс простоты и функциональности	Требует поддержки редакторов

Стратегия реализации

Этапы

Этап	Содержание
Этап 1: Базовая поддержка	Расширение парсера для распознавания комментариев `//!` и `/! ... !/`, присоединение их к узлам AST; в режиме верификации — сбор спецификаций, генерация простых условий верификации (только арифметические сравнения); интеграция решателя Z3
Этап 2: Поддержка кванторов	Поддержка кванторных выражений, трансляция в `forall`/`exists` SMT-LIB; подсветка спецификаций в IDE и подсказки при наведении
Этап 3: Оптимизация и инструменты	Инкрементальная верификация, кэширование проверенных модулей; отчёты о покрытии спецификаций; инструменты для выявления спецификаций (генерация кандидатных спецификаций из тестов)

Зависимости

RFC-009: Модель владения — выражения спецификаций требуют семантики чистых функций
RFC-010: Унифицированный синтаксис типов — система типов спецификаций основана на системе типов
RFC-011: Проект системы обобщённых типов — типы спецификаций поддерживают параметры обобщённых типов

Риски

Сложность интеграции SMT-решателя: интеграция решателей вроде Z3 может столкнуться с техническими трудностями
- Митигация: использование зрелых Rust-биндингов Z3, постепенное расширение поддерживаемых типов выражений
Сложность отладки при неудаче верификации: когда SMT-решатель не может доказать спецификацию, пользователю может быть сложно понять причину
- Митигация: предоставление понятных сообщений об ошибках и объяснений контрпримеров
Затраты производительности: режим верификации может существенно увеличить время компиляции
- Митигация: реализация инкрементальной верификации и механизмов кэширования

Открытые вопросы

[ ] Область поддержки кванторов: поддерживать ли вложенные кванторы? Поддерживать ли кванторы высшего порядка?
[ ] Вывод инвариантов циклов: предоставлять ли функцию автоматического вывода простых инвариантов?
[ ] Формат контрпримеров при неудаче доказательства: как наиболее эффективно представлять контрпримеры?
[ ] Интеграция с другими инструментами верификации: рассматривать ли интеграцию с доказателями вроде Coq, Lean?

Ссылки

Жизненный цикл и судьба

┌─────────────┐
│   Черновик  │  ← Создаётся автором
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  На рассмотрении │  ← Обсуждение сообществом
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│  Принят     │    │  Отклонён   │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/  │    │    rfc/     │
│ (официальный проект) │    │ (остаётся на месте)  │
└─────────────┘    └─────────────┘

Описание статусов

Статус	Расположение	Описание
Черновик	`docs/design/rfc/`	Черновик автора, ожидает отправки на рассмотрение
На рассмотрении	`docs/design/rfc/`	Открыто для обсуждения и обратной связи сообщества
Принят	`docs/design/accepted/`	Становится официальным проектным документом, переходит в фазу реализации
Отклонён	`docs/design/rfc/`	Сохраняется в каталоге RFC, статус обновляется

Действия после принятия

Переместить RFC в каталог docs/design/accepted/
Обновить имя файла на описательное (например, hoare-logic-static-verification.md)
Обновить статус на «Официальный»
Обновить статус на «Принят», добавить дату принятия

Действия после отклонения

Сохранить в каталоге docs/design/rfc/
Добавить причину отклонения и дату в начало файла
Обновить статус на «Отклонён»

RFC 022: Поддержка статической верификации по логике Хоара (спецификационные комментарии и типы спецификаций) [Устарел] ​

Резюме ​

Мотивация ​

Зачем нужна эта функциональность/изменение? ​

Текущие проблемы ​

Предложение ​

Основной проект ​

1. Синтаксис спецификационных комментариев ​

1.1 Унифицированный синтаксис спецификаций ​

1.2 Спецификации циклов ​

1.3 Выражения спецификаций ​

2. Система типов спецификаций ​

2.1 Встроенные типы спецификаций ​

2.2 Пользовательские типы спецификаций ​

3. Режимы компиляции ​

4. Механизм верификации ​

5. Интеграция с тестированием ​

6. Поддержка редакторов ​

Детальный проект ​

Изменения синтаксиса ​

7.1 Расширение синтаксиса ​

7.2 Проверка типов ​

7.3 Генерация условий верификации ​

7.4 Сообщения об ошибках ​

7.5 Проверка во время выполнения ​

7.6 Интеграция с существующим проектом ​

Влияние на систему типов ​

Поведение во время выполнения ​

Изменения в компиляторе ​

Обратная совместимость ​

Компромиссы ​

Преимущества ​

Недостатки ​

Альтернативы ​

Стратегия реализации ​

Этапы ​

Зависимости ​

Риски ​

Открытые вопросы ​

Ссылки ​

Жизненный цикл и судьба ​

Описание статусов ​

Действия после принятия ​

Действия после отклонения ​

RFC 022: Поддержка статической верификации по логике Хоара (спецификационные комментарии и типы спецификаций) [Устарел]

Резюме

Мотивация

Зачем нужна эта функциональность/изменение?

Текущие проблемы

Предложение

Основной проект

1. Синтаксис спецификационных комментариев

1.1 Унифицированный синтаксис спецификаций

1.2 Спецификации циклов

1.3 Выражения спецификаций

2. Система типов спецификаций

2.1 Встроенные типы спецификаций

2.2 Пользовательские типы спецификаций

3. Режимы компиляции

4. Механизм верификации

5. Интеграция с тестированием

6. Поддержка редакторов

Детальный проект

Изменения синтаксиса

7.1 Расширение синтаксиса

7.2 Проверка типов

7.3 Генерация условий верификации

7.4 Сообщения об ошибках

7.5 Проверка во время выполнения

7.6 Интеграция с существующим проектом

Влияние на систему типов

Поведение во время выполнения

Изменения в компиляторе

Обратная совместимость

Компромиссы

Преимущества

Недостатки

Альтернативы

Стратегия реализации

Этапы

Зависимости

Риски

Открытые вопросы

Ссылки

Жизненный цикл и судьба

Описание статусов

Действия после принятия

Действия после отклонения