Разделы сайта находятся в разработке.
Материалы могут быть неполными или содержать ошибки. Содержимое сайта будет синхронизировано с реализацией при выходе следующей версии, тогда как текущая (0.6.0) предназначена для прототипирования синтаксиса и создания песочницы.
Гарантии и безопасность
Свод фич TrustLang, отвечающих за безопасность и качество кода
Раздел объединяет возможности TrustLang, которые отвечают за безопасность и качество программ: безопасное управление памятью, защиту от гонок данных, контроль корректности на этапе компиляции и формальную верификацию.
Каждая возможность описана подробно ровно в одном месте (страница-источник) и лишь
упоминается здесь с выжимкой и ссылкой. Подробные перечни опций/диагностик не дублируются —
их источник в справке инструмента (trust --help, trust -Whelp, LSP-ховеры).
Возможности раздела
| Возможность | Кратко | Подробно (источник) |
|---|---|---|
| Безопасное управление памятью без GC | RAII, сильные/слабые ссылки, запрет сильных циклических ссылок, защита стека от переполнения | Память |
| Защита от гонок и синхронизация доступа | Автоматическая межпотоковая синхронизация при обращении к разделяемым данным | Память |
| Контрактное программирование | Пред-/пост-условия и утверждения (trust_pre/trust_post/trust_assert) |
Верификация |
| Формальная верификация (SMT) | Авто-выполнение Z3 по контрактам, инварианты циклов, кванторы | Верификация |
| Статическая типизация и контроль приведения | Номинальная проверка типов на этапе компиляции; сужение с контролем диапазона | Система типов |
| Диапазонные проверки чисел | Ошибка при выходе за диапазон типа, а не молчаливое переполнение | Числа |
| Контроль целочисленного переполнения | Встроен и включён по умолчанию: переполнение знаковой арифметики (UB в C++) → перехватываемое IntMinus |
Числа |
| Защита стека от переполнения (stack check) | Переполнение стека → перехватываемое исключение stack_overflow, а не segfault |
stack_check |
| Контроль инвалидации ссылок (borrowed) | Запрет использования зависимых ссылок после мутации источника (висячие ссылки) | invalidation |
Модель безопасной памяти портирована на C++ в отдельный проект memsafe.
Смежные темы
- Многопоточность и асинхронность (корутины,
:AsyncTask/:AsyncPool) — это функциональная возможность языка, а не фича безопасности; описана в Выражениях и потоке управления. К безопасности относится лишь защита от гонок, которую обеспечивает модель ссылок из Памяти. - Статус реализации — границы реализации фич этого раздела.
Защита стека от переполнения (stack check)
Превращение переполнения стека в перехватываемое исключение вместо аварийного завершения