⚠️ Устарело (DEPRECATED)
Данный RFC заменён RFC-027: Типы с вычислениями на этапе компиляции и унифицированная статическая верификация.
Причина устаревания: 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-ассертов для постепенного внедрения

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-проверки	Преобразование спецификаций в runtime-ассерты, panic при нарушении	`yaoxiangc --enable-runtime-checks source.yx`

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

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

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

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

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

5. Комбинация с тестированием

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

6. Поддержка редакторами

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

Детальное проектирование

Синтаксические изменения

До	После
Нет синтаксиса аннотаций спецификаций	Разрешены аннотации `//!` и `/! ... !/`

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 Runtime-проверки

В режиме --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-кэша
Режим runtime-проверок: генерация операторов assert, обнаружение нарушений на этапе выполнения

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

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

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

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

Компромиссы

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

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

Недостатки

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

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

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

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

Фазы

Фаза	Содержание
Фаза 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 Runtime-проверки ​

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 Runtime-проверки

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

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

Поведение на этапе выполнения

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

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

Компромиссы

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

Недостатки

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

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

Фазы

Зависимости

Риски

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

Список литературы

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

Пояснение к статусам

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

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