Язык спецификации ANSI/ISO C

Язык спецификации ANSI/ISO C

Парадигма	декларативный с небольшим количеством императивных функций.
Разработано	Комиссия по атомной энергии и INRIA
Разработчик	Комиссия по атомной энергии и INRIA
Впервые появился	2008
Стабильная версия	v1.16 / 19 ноября 2020 г.
Дисциплина набора текста	статический
Основные реализации
Фрама-С
Под влиянием
Кол-во

Язык спецификации ANSI /ISO C ( ACSL ) — это язык спецификации для программ C , использующий в стиле Хоара предварительные и постусловия и инварианты , который следует парадигме проектирования по контракту . Спецификации записываются в виде аннотаций C к программе C, которые, следовательно, могут быть скомпилированы любым компилятором C.

Текущим инструментом проверки ACSL является Frama-C . Он также реализует родственный язык, язык спецификации ANSI/ISO C++ ( ACSL++ ), определенный для C++ .

Обзор

В 1983 году Американский национальный институт стандартов (ANSI) поручил комитету X3J11 стандартизировать язык C. Первый стандарт C был опубликован ANSI. Хотя этот документ впоследствии был принят Международной организацией по стандартизации (ISO), а последующие версии, опубликованные ISO, были приняты ANSI, название ANSI C продолжает использоваться.

ACSL — это язык спецификации поведенческого интерфейса (BISL). Его цель — указать поведенческие свойства исходного кода C. Основное вдохновение для создания этого языка взято из языка спецификаций инструмента Caduceus для дедуктивной проверки поведенческих свойств программ на языке C. Язык спецификации Caduceus сам по себе вдохновлен JML , который преследует аналогичные цели для исходного кода Java.

Одно из отличий от JML заключается в том, что ACSL предназначен для статической и дедуктивной проверки, тогда как JML предназначен как для проверки утверждений во время выполнения, так и для статической проверки с использованием, например, инструмента ESC/Java .

Синтаксис

Рассмотрим следующий пример прототипа функции с именем incrstar:

/*@ requires \valid(p);
  @ assigns *p;
  @ ensures *p == \old(*p) + 1;
  @*/
void incrstar (int *p);

Контракт задается комментарием, который начинается с /*@. Его смысл следующий:

• первая строка является предварительным условием: она утверждает, что функция incrstar должен вызываться с указателем p это указывает на безопасно выделенную ячейку памяти.
• Вторая строка — это предложение фрейма, в котором говорится, что функция incrstar не изменяет какую-либо ячейку памяти, кроме той, на которую указывает p.
• Наконец, ensures Предложение — это постусловие, которое указывает, что значение *p увеличивается на единицу.

Допустимой реализацией вышеуказанной функции будет:

void incrstar (int *p) {
    (*p)++;
}

Поддержка инструментов

Большинство функций ACSL поддерживаются Frama-C .

Статический анализатор TrustInSoft является коммерческой производной Frama-C. Он проверяет поведение программы и (с помощью встроенных правил, основанных на спецификации языка) выявляет случаи неопределенного поведения .

Ссылки

• Пример использования ACSL. Достаточные предварительные условия для модульной проверки утверждений в VMCAI 2008, страницы 188–202.
• ACSL на примере , хорошо документированный набор спецификаций ACSL простых алгоритмов, был разработан группой VerificationGroup в Fraunhofer FOKUS.
• Учебное пособие по Frama-C с WP и ACSL для начинающих, которое также дает некоторые идеи о теории, лежащей в основе инструментов ( доступно также на французском языке ).
• Отчет об использовании ACSL и Frama - C для формулирования и проверки требований низкого уровня в контексте DO-178C . проекта, соответствующего
• Report mentioning the use of ACSL in teaching [1] , Петренко Ольга Леонидовна and Хорошилов Алексей Владимирович.
• В Technikum Wien ACSL и Frama-C преподаются на курсе проектирования и проверки .

Внешние ссылки

• Полную спецификацию ACSL можно найти на странице загрузки Frama -C .
• TSnippet от TrustInSoft позволяет тестировать фрагменты C в браузере с использованием ACSL.