Оглавление
Язык спецификации ANSI/ISO C
-
Обзор языка спецификаций ANSI/ISO C (ACSL)
- ACSL – это язык спецификаций для C, использующий условия и инварианты Hoare.
- Спецификации записываются в виде комментариев к исходному коду C и могут быть скомпилированы любым компилятором C.
- Текущий инструмент проверки ACSL – Frama-C, который также поддерживает ANSI/ISO C++ Specification Language (ACSL++).
-
История и стандартизация
- ANSI стандартизировала язык Си в 1983 году, и название ANSI C продолжает использоваться, несмотря на принятие ISO.
- ACSL является языком спецификации поведенческого интерфейса, вдохновленным Caduceus и JML.
-
Синтаксис и примеры
- Пример контракта для функции incrstar включает предварительное условие, предложение frame и постусловие.
- Frama-C поддерживает большинство функций ACSL, а TrustInSoft является коммерческим инструментом, основанным на Frama-C.
-
Поддержка и рекомендации
- Frama-C и TrustInSoft используются для статического анализа и верификации поведения программ.
- Существуют учебные пособия и доклады, демонстрирующие использование ACSL в различных контекстах, включая верификацию требований и обучение.
-
Внешние ссылки
- Полная спецификация ACSL доступна на сайте Frama-C.
- TSnippet от TrustInSoft позволяет тестировать код C в браузере с использованием ACSL.