ANSI / ISO C Specification Language ( ACSL ) является языком спецификаций для программ C , используя Хоару стиль до и постусловия и инварианты, что следует за дизайн по контракту парадигмы. Спецификации записываются в виде комментариев аннотации C к программе C, которая, следовательно, может быть скомпилирована любым компилятором C.
Парадигма | декларативный с несколькими императивными функциями. |
---|---|
Разработано | Commissariat à l'Énergie Atomique и INRIA |
Разработчик | Commissariat à l'Énergie Atomique и INRIA |
Впервые появился | 2008 г. |
Стабильный выпуск | 2008 / декабрь 2008 |
Печатная дисциплина | статический |
Основные реализации | |
реализация находится на платформе Frama-C . | |
Под влиянием | |
JML |
Текущий инструмент проверки ACSL - Frama-C .
Обзор
В 1983 году Американский национальный институт стандартов (ANSI) поручил комитету X3J11 стандартизировать язык C. Первый стандарт для C был опубликован ANSI. Хотя этот документ впоследствии был принят Международной организацией по стандартизации (ISO), а последующие версии, опубликованные ISO, были приняты ANSI, название ANSI C по-прежнему используется.
ACSL - это язык спецификации поведенческого интерфейса (BISL). Он направлен на определение поведенческих свойств исходного кода C. Главным источником вдохновения для этого языка происходит от языка спецификации инструмента Кадуцей для дедуктивной верификации поведенческих свойств программ C . Язык спецификаций Caduceus сам по себе вдохновлен JML, который преследует аналогичные цели для исходного кода Java.
Одно из отличий от JML заключается в том, что ACSL нацелен на статическую проверку и дедуктивную проверку, тогда как JML нацелен как на проверку утверждений во время выполнения, так и на статическую проверку с использованием, например, инструмента ESC / Java .
Синтаксис
Рассмотрим следующий пример прототипа функции с именем incrstar
:
/ * @ требует \ valid (p); @ присваивает * p; @ гарантирует * p == \ old (* p) + 1; @ * / void incrstar ( int * p );
Контракт дается комментарием, который начинается с /*@
. Его значение таково:
- первая строка является предварительным условием: в ней говорится, что функция
incrstar
должна вызываться с указателемp
, указывающим на безопасно выделенную ячейку памяти. - Вторая строка - это предложение кадра, в котором говорится, что функция
incrstar
не изменяет никакую ячейку памяти, кроме той, на которую указываетp
. - Наконец,
ensures
предложение является постусловием, которое указывает, что значение*p
увеличивается на единицу.
Поддержка инструмента
Большинство функций ACSL поддерживаются Frama-C .
Рекомендации
- Пример использования ACSL Достаточные предварительные условия для модульной проверки утверждений в VMCAI 2008, страницы 188-202.
- ACSL by Example , хорошо документированный набор спецификаций ACSL простых алгоритмов, разрабатывается и поддерживается VerificationGroup в Fraunhofer FOKUS.
- Учебник о Фрама-C с WP и ACSL для начинающих , который также предоставляет некоторые идеи о теории позади инструментов ( доступные также на французском языке ).
- Отчет об использовании ACSL и FRAMA-C для разработки и проверки требований низкого уровня в контексте DO-178C совместимого проекта
- Сообщите об использовании ACSL в обучении [1] , Петренко Ольга Леонидовна и Хорошилов Алексей Владимирович.
- В Technikum Wien ACSL и Frama-C преподаются в рамках курса по проектированию и проверке .
Внешние ссылки
Полная спецификация ACSL доступна на странице загрузки из Фрама-C .