На пути к верификации С-программ. Язык C-Light 1

Непомнящий В.А.
Институт систем информатики СО РАН, Новосибирск

Ануреев И.С.
Институт систем информатики СО РАН, Новосибирск


Михайлов И.Н.
Институт систем информатики СО РАН, Новосибирск

Промский А.В.
Институт систем информатики СО РАН, Новосибирск

Аннотация:

Описано ориентированное на верификацию представительное подмножество языка C -- язык C-light. Этот язык допускает детерминированные выражения, ограниченное использование операторов $switch$ и $goto$, а вместо библиотечных функций для работы с динамической памятью включает операции $new$ и $delete$ языка C$++$. Для языка C-light представлена структурная операционная семантика в стиле Плоткина. Язык C-light служит входным языком разрабатываемой верификации.

Введение

Формальная верификация программ - актуальное направление современного программирования. Обозримая формальная семантика является необходимой предпосылкой того, что язык программирования удобен для верификации. Поскольку язык С широко используется на практике, проблема верификации для него представляет значительный интерес [5,6,7,10]. Трудности верификации программ на языке С хорошо известны [2,3,4,8]. Основной трудностью является отсутствие формальной семантики для полного языка С, соответствующего стандарту ANSI. Цель настоящей работы - выделение удобного для верификации представительного подмножества языка C, которое расширяется элементами языка С$++$. Этот язык, названный C-light, содержит все множество операторов языка С при некоторых семантических ограничениях и большинство типов и операций. C-light имеет детерминированную семантику выражений, допускает только ограниченное использование операторов switch и goto, а вместо библиотечных функций включает операции new и delete языка С$++$ для работы с динамической памятью. C-light не поддерживает поразрядных операций, типа объединения, структур с битовыми полями, ряда модификаторов и спецификаторов типов, функций с переменным числом аргументов. Предложенная операционная семантика C-light состоит из двух частей: статическая семантика или система типов языка и динамическая, описывающая поведение программы в терминах абстрактной вычислительной машины. Хотя операционная семантика удобна для формального определения языка, для верификации она имеет слишком низкий уровень, что приводит к громоздким доказательствам. Поэтому обычно используют аксиоматическую семантику, которая определяется как система вывода утверждений о свойствах программ. Однако аксиоматическая семантика для языка C-light также была бы громоздкой. В связи с этим была выбрана двухуровневая схема: в языке C-light выделяется ядро -- язык C-light-kernel, для которого разрабатывается аксиоматическая семантика, и в этот язык транслируются исходные программы на языке C-light. По сравнению с языком C-light в нем более простые выражения, более ограниченный набор операторов, сокращенный набор глобальных объектов, а вместо функций используются процедуры. Доказана важная теорема о непротиворечивости аксиоматической семантики языка C-light-kernel относительно операционной. Достоинством двухуровневой схемы является то, что конструкции, которые обычно не поддерживают при создании аксиоматической семантики, здесь не исключаются полностью, а приводятся к эквивалентному виду. Особое внимание уделяется формализации правил перевода языка C-light в язык C-light-kernel. Кроме того, программы на языке Паскаль естественным образом транслируются в C-light-kernel, что позволит проводить верификацию программ на этом языке, используя опыт системы СПЕКТР. Отметим, что указатели языка C-light сохраняются в языке C-light-kernel практически полностью. Для указателей была разработана проблемная область в виде аксиом, определяющих свойства ссылочных классов. Таким образом, предложенный подход к верификации С-программ является весьма перспективным и на его основе разрабатывается атоматизированная система верификации.

Обзор языка C-light

Язык аннотированных программ C-light является подмножеством «чистого» С, расширенным некоторыми лексическими правилами из C$++$ и аннотациями. Любой текст, соответствующий одновременно синтаксису С-light и синтаксису ANSI C, будет иметь одинаковый смысл в обоих этих языках.

Аннотации. В отличие от C в C-light введено понятие аннотации. Аннотация -- это фрагмент текста, обрамленный специальными лексемами-скобками /% и %/. Текст есть правильная аннотация, если он может быть разбит на лексемы и пробельные элементы С-light без лексических ошибок и в нем соблюден «баланс скобок». Используются аннотации для записи спецификаций программ.

Декларации. Текущая версия системы не может строить условия корректности для кода, в котором используются типы, созданные с помощью union. Список членов структуры может содержать спецификаторы доступа (они будут игнорироваться) и битовые поля (текущая версия системы не может создать условия корректности для кода, в котором используются структуры битовыми полями). Модификатор "функция, возвращающая значение типа ..." не только описывает тип, но и может назначить имена некоторым объектам -- аргументам функции. Список аргументов может заканчиваться троеточием, однако в семантике такие функции не поддерживаются. Пустой список аргументов не разрешен -- требуется void.

Выражения. Главным отличием языка С-light от С являются наличие детерминизма вычисления и запрета низкоуровневых операций. В C-light все выражения равноправны. И сложное адресное выражение, и отдельный идентификатор переменной обрабатываются по одним и тем же правилам. Выражение общего вида есть список выражений присваивания, разделенных запятыми. Эти выражения будут вычисляться строго слева направо, результат самого правого из них будет результатом всего выражения. Выражение присваивания может либо содержать операции присваивания, либо быть простым rvalue. Главное, что в нем на верхнем уровне нет операции «запятая», поэтому, в отличие от выражения общего вида, выражение присваивания может встречаться в различных списках выражений. В C-light предусмотрены все операции присваивания C, но условия корректности не могут быть сгенерированы для выражений с побитовыми операциями. Для приведения типов используется синтаксис языка С. Допустимы только безопасные приведения типов (главным образом для скалярных типов). Для указателей введено дополнительное ограничение -- можно делать только приведение от типа void* к Т*, где Т -- любой стандартный тип или тип пользователя. Для выделения и освобождения динамической памяти используются операции языка С$++$.

Операторы. Оператором (инструкцией) языка C-light является любой оператор языка С, в том числе определение переменной или типа данных «на лету». Пустой оператор тоже является оператором вычисления выражения. Типом условных выражений в циклах и условных операторах может быть либо скалярный тип, либо bool. Тип выражения в операторе return должен приводиться по умолчанию к типу, возвращаемому функцией, в которой содержится этот оператор. Мы считаем, что в условном операторе if всегда есть ветвь else, возможно пустая. На метки в операторе switch налагается ограничение: все метки должны находиться на одном уровне вложенности. Не предусмотрено никакого особого места для записи инварианта цикла. По соглашению инвариантом будет считаться первая аннотация в составном операторе -- теле цикла. Запрещено передавать управление по goto внутрь любого блока из охватывающего его блока, или из одного блока в другой, не пересекающийся с ним. Однако можно передать управление из вложенного блока в охватывающий. Как и в С$++$, запрещено передавать управление по goto в обход инициализации.

Операционная семантика языка C-light

Семантика -- это отображение, которое сопоставляет каждому элементу из синтаксической области определения значение или интерпретацию, т. е. элемент семантической области. Сначала определим семантику выражений. Во-первых, для каждого типа T фиксируем множество значений, называемое носителем типа T и обозначаемое $D_T$. Далее, для любой константы типа T фиксируем значение в носителе $D_T$ и говорим, что константа обозначает это значение. Cчитаем, что каждая константа базового типа (а также типов «массив» и «структура») обозначает саму себя. В свою очередь константы типов «функций» обозначают соответствующие функции. В отличие от констант значения переменных не фиксированы и определяются через состояния абстрактной вычислительной машины. Состояние -- это в простейшем случае отображение, которое присваивает любой переменной типа T значение в области $D_T$. Используем слово States для обозначения множества всех состояний. Семантика $\mathcal{I}\Vert s\Vert$ выражения s типа T это отображение

\begin{displaymath}\mathcal{I}\Vert s\Vert : States \rightarrow D_T\end{displaymath}

определяемое индукцией по структуре s (рассмотрим ограниченное подмножество выражений):

Следует отметить, что если все выражения записывать в префиксной форме, то этих четырех случаев достаточно для всего языка C-light, например, бинарную операцию "+" можно считать константой типа $\mathbf{int}\times\mathbf{int}\rightarrow\mathbf{int}$. Как обычно, индукцией по структуре утверждения определяется понятие истинности утверждения p в состоянии $\sigma$, записываемой в виде $\sigma \models p$. Также используем понятие смысла утверждения, определенного как

\begin{displaymath}\Vert p\Vert = \{ \sigma \vert \sigma - \mathrm{состояние\; и\;} \sigma \models p \}.\end{displaymath}

Мы говорим, что утверждение p истинно или выполняется, если $\Vert p\Vert = States$.

Операционную семантику C-light будем представлять в виде множеств пар конфигураций абстрактной вычислительной машины, используя подход Плоткина [1,9]. Конфигурация -- это пара $\langle \mathrm{P}, \sigma\rangle$ -- программа P и состояние $\sigma$. Пустая программа обозначается символом E, и записи E; A и A; E являются эквивалентными обозначениями для программы А. Как уже отмечалось ранее, в простейшем случае состояние -- это отображение из множества идентификаторов переменных во множество их потенциальных значений. Такого представления достаточно для простых модельных языков [1], но для языка C-light необходимо добавить новые компоненты.

Определение. Состояние абстрактной вычислительной машины языка C-light -- это семерка {M, $\Gamma$, $\Sigma$, $\Phi$, TD, $\Pi$, GLF}, где 1) M -- отображение всех переменных программы во множество их потенциальных значений; 2) $\Gamma$ -- отображение из множества имен переменных программы в типы; 3) $\Sigma$ -- отображение, сопоставляющее тегу структуры последовательность пар имен и типов полей структуры; 4) $\Phi$ -- отображение, сопоставляющее идентификатору функции кортеж типов ее аргументов и тип возвращаемого значения; 5) TD -- отображение, сопоставляющее идентификатору имя типа, связанное с ним typedef-декларацией; 6) $\Pi$ -- очередь отложенных побочных эффектов, которые накапливаются при вычислении выражений. Очередь очищается при достижении контрольной точки. Отметим, что если бы мы не ввели детерминизм вычисления выражений, то очередь превратилась бы в мультимножество; 7) GLF -- флаг, определяющий вложенность, необходим для корректной инициализации переменных. В начале работы программы, т. е. на глобальном уровне, флаг равен нулю, при входе в любой блок увеличивается на единицу, при выходе соответственно уменьшается. Изменения состояний записываются в виле обновлений. Далее запись $\sigma(Х(a\leftarrow e))$ означает состояние $\sigma'$ такое, что компонента X состояния $\sigma'$ совпадает с компонентой X состояния $\sigma$ всюду, кроме, может быть, a, и $Х_{\sigma'}(a) = e$, а все остальные компоненты совпадают полностью. Изменение нескольких компонент состояния записывается через запятую: $\sigma(X(a\leftarrow e), Y(b\leftarrow i))$. Такая запись имеет смысл для компонент, являющихся отображениями. Для флага GLF, например, можно использовать просто символ равенства. Семантика программы определяется индукцией по структуре программы в терминах отношений переходов. Для языка С-light необходимо ввести три бинарных отношения перехода, а именно: 1) отношение для вычисления выражений: $\rightarrow _e$, 2) отношение для вычисления объявлений: $\rightarrow _v$, 3) отношение для обработки операторов: $\rightarrow _s$. Рассмотрим примеры правил перехода для этих трех отношений.
\begin{displaymath} \frac{\Gamma_{\sigma}(\mathbf{arr\_id}) = \tau[n]}{\langle... ...tarrow_e \langle (\mathbf{arr\_id}, \tau*), \sigma \rangle}. \end{displaymath} (1)


\begin{displaymath} \frac{\langle(\tau_1)(v_0, \tau_0), \sigma_0\rangle \right... ... \langle v, \sigma_0(\Pi+\{\mathrm{upd(lval}, v)\})\rangle}. \end{displaymath} (2)


\begin{displaymath} \frac{\mathrm{GLF}_{\sigma} = 0\qquad \tau - \mathrm{скаля... ...ftarrow\tau), \mathrm{M}(\mathbf{id}\leftarrow 0)) \rangle}. \end{displaymath} (3)


\begin{displaymath} \langle \mathsf{enum\; id}\{ decls\};, \sigma \rangle \ri... ...rrow_v \langle \mathsf{signed\; int}\;decls, \sigma \rangle. \end{displaymath} (4)


\begin{displaymath} \frac{\langle e, \sigma_0(\Pi\leftarrow\emptyset) \rangle ... ... \rightarrow_s \langle \mathrm{RetVal}(v), \sigma \rangle}. \end{displaymath} (5)


\begin{displaymath} \frac{\langle decls , \sigma_0 \rangle \rightarrow_v \la... ...w_s \langle v, \sigma_0(M \leftarrow M_{\sigma_2})\rangle}. \end{displaymath} (6)

Здесь представлены правила для обработки массивов (1), присваиваний простым переменным (2), объявлений простых переменных (3) и перечислимых типов (4), а также правила для оператора возврата значений (5) и блока (6).

Обзор языка C-light-kernel

Декларации. Принципиальное отличие языка C-light-kernel как от С, так и от C-light, заключается в том, что глобальными объектами могут быть только указатели. Это ограничение снимает ряд существенных трудностей семантики функций и процедур. При переводе глобальные объекты будут собираться в специальную структуру, а функциям будет передаваться указатель на нее. В языке C-light-kernel локальное переопределение переменных отсутствует -- все различные объекты должны иметь уникальные имена. В частности, при трансляции имена автоматических объектов будут уточняться за счет добавления информации о строке и столбце в исходном файле. Одна декларация не может содержать целый список декларируемых объектов. Таким образом любая декларация объявляет ровно один объект. Случай одновременной декларации структуры и typedef не является исключением, поскольку типы являются объектами периода компиляции, но не периода исполнения. После имени объекта могут быть указаны такие модификаторы типа, как "массив из элементов типа ..." и "функция, возвращающая значение типа ...". В отличие от C-light, разрешающего например описание типа многомерного массива непосредственно в декларации (например int a[2][3]), необходимо использовать предварительно созданый именованный тип. Последнее важное отличие от языка C-light относится к спецификации декларации. Она перечисляет свойства объекта, которые нужны в основном для оптимизации кода. В языке C-light большинство спецификаторов и модификаторов игнорировались, так как операционная среда C-light существенно проще реальной операционной среды C. Но в C-light-kernel спецификаторы класса памяти static и auto становятся обязательными, что позволяет просто задать семантику неявной инициализации.

Выражения. В языке С-light допускались все выражения языка С, несодержащие низкоуровневых операций. Синтаксис и семантика выражений языка C-light-kernel гораздо проще. Они получаются из выражений языка C-light максимально возможным разбиением на составные части, и эти части записываются как последовательность операторов вычисления выражения. Выражение присваивания может содержать операции присваивания, а может быть простым rvalue. В отличие от C-light, в C-light-kernel есть ровно одна операция простого присваивания, и отсутствуют операции наподобие +=. Кроме того, не разрешаются цепочки присваиваний вида a=b=c. В C-light-kernel нет операции «запятая», поэтому любое выражение есть либо выражение присваивания, либо вызов процедуры. Таким образом, выражение присваивания обретает тот же статус, что и оператор присваивания в языке Паскаль. Фактическим аргументом функции может быть либо константа, либо переменная, но не выражение с какими-либо операциями. Если указатель ptr есть параметр функции, возвращающей значение, то в теле этой функции выражение вида *ptr не может находиться слева от операции присваивания. На процедуры это ограничение не распространяется. Т. е., если функция возвращает значение, то она не может изменять аргументов, передаваемых через указатели. Такое ограничение обычно является правилом хорошего стиля в программировании, но в нашем случае его необходимо жестко фиксировать, иначе соответствующее правило аксиоматической семантики в общем случае окажется неверным. При трансляции из языка C-light функция, в которой есть такая ситуация, преобразуется в процедуру с тем же именем и дополнительным параметром. При трансляции также контролируется изменение глобальных объектов.

Операторы. При переводе происходят следующие изменения: Операторы передачи управления break, continue и return заменяются на оператор goto; Все операторы циклов заменяются на цикл while; Оператор-переключатель switch приводится к форме оператора case языка Паскаль. Все остальные ограничения языка C-light для операторов остаются без изменений. В семантике языка C-light-kernel понятие состояния проще, а три отношения перехода объединяются в одно. Определяя транзитивное, рефлексивное замыкание ( $\rightarrow ^*$) для отношения перехода, можем определить семантику программы S как отображение из States в $2^{States}$:

\begin{displaymath} \mathcal{M}[\![ S ]\!](\sigma) = \{\tau\, \vert \langle S, \sigma \rangle \rightarrow ^*\langle Final, \tau \rangle\},\end{displaymath}

где Final -- пустая программа или значение некоторого программного типа. Т. е. семантика рассматривает все возможные исполнения программы, начинающиеся из состояния $\sigma$. Отображение $\mathcal{M}$ называется семантикой частичной корректности для языка С-light-kernel. Также по определению

\begin{displaymath}\mathcal{M}[\![ S ]\!](\Vert P\Vert) = \bigcup _{\sigma\in\Vert P\Vert} \mathcal{M}[\![ S ]\!](\sigma),\end{displaymath}

где P -- формула. Как уже упоминалось, операционная семантика, даже с высокой степенью абстрактности, неудобна для реальной верификации программ. Хоаром был предложен другой подход -- работать не с отдельными состояниями, а с множествами состояний. Поскольку множества состояний можно определять формулами, истинными в этих множествах, то вход и выход программы характеризуются специальными формулами языка спецификаций -- предусловием и постусловием. При этом для того, чтобы обрабатывать циклы вне зависимости от числа итераций, для них используют свои формулы -- инварианты циклов. Основной объект в этой семантике -- это тройка Хоара $\langle\, P\,\rangle\, A\, \langle\,Q\,\rangle$, где A -- некоторая программа, а P и Q -- ее предусловие и постусловие соответственно. Фактически эта тройка является формулой, и она считается истинной в смысле частичной корректности, если из того, что утверждение P истинно перед исполнением программы и программа А завершается, следует, что утверждение Q истинно. Формально понятие истинности тройки Хоара [1] дается на основе операционной семантики частичной корректности: Определение. Говорим, что тройка Хоара $\langle\, P\,\rangle\, A\, \langle\,Q\,\rangle$ истинна в смысле частичной корректности и изображаем $\models \langle\,P\,\rangle\,A\, \langle\,Q\,\rangle$, если

\begin{displaymath}\mathcal{M}[\![A]\!](\Vert P\Vert) \subseteq \Vert Q \Vert.\end{displaymath}

Аксиоматическая семантика языка C-light-kernel

Аксиоматическая семантика для любого языка программирования определяется как система вывода, в которой роль формул играют тройки Хоара. При этом программные конструкции являются преобразователями предикатов. При выводе тройки Хоара в этой системе происходит элиминация операторов, и истинность тройки сводится к истинности набора лемм -- условий корректности, которые не содержат программных конструкций. Аксиоматическая семантика HSC для языка C-light-kernel описана в [12]. Рассмотрим примеры правил системы HSC. Пусть символы P и Q обозначают аннотации, символы A, B (c индексами) -- операторы; Expn обозначает оператор-выражение.
\begin{displaymath} \frac{\mathcal{D}om(Expn)}{\langle\,\mathcal{U}pd(Q, Expn)\,\rangle\,Expn\,\langle\,Q\,\rangle}, \end{displaymath} (7)

где Expn -- выражение без вызовов функций.
\begin{displaymath} \frac{P\!\Rightarrow\! P'(\overline{v}\leftarrow \overlin... ...ngle\,lval = \mathrm{f}(\overline{e});\,\langle\,Q\,\rangle}, \end{displaymath} (8)

где B -- тело функции f, $\overline{v}$ и $\overline{e}$ -- списки формальных параметров и фактических аргументов, z -- идентификатор ранее не встречавшийся.
\begin{displaymath} \frac{\langle\,P\wedge(z=k_i)\,\rangle\,A_i\,\langle\,Q\,... ...e}\;k_i:A_i\,...\,\mathbf{default}:B\}\,\langle\,Q\,\rangle}. \end{displaymath} (9)


\begin{displaymath} \frac{P\Rightarrow INV} {\langle\,P\,\rangle\,\mathbf{goto}\;\mathrm{L}\,\langle\,\mathrm{L}:INV\,\rangle}. \end{displaymath} (10)


\begin{displaymath} \frac{\langle\,P'\,\rangle\,B\,\langle\,Q'\,\rangle\qquad... ...,\mathrm{f}(\overline{p},\overline{e})\,\langle\,Q\,\rangle}, \end{displaymath} (11)

при $\mathbf{void}\; \mathrm{f}(\overline{x},\overline{v})B\mathrm{(f)}\mbox{ и } \langle\,P'\,\rangle\,\mathrm{f}(\overline{x},\overline{v})\,\langle\,Q'\,\rangle$.

Правило (7) определяет способ обработки выражений. В отличие от аналогичного правила для простых языков, здесь присутствует посылка $\mathcal{D}om(Expn)$, которая является проверкой на допустимость вычисления выражения в данном контексте. Правило (8) определяет присваивание результата вызова функции некоторой переменной. Правило (9) обрабатывает оператор-переключатель, а правило (10) -- оператор передачи управления. Наконец, правило (11) определяет семантику вызова рекурсивной процедуры. Как и в обычных логических системах вывода, в аксиоматической системе HSC в качестве базиса должны быть заданы некоторые истинные утверждения -- аксиомы. Они используются в качестве посылок в стандартном правиле усиления посылки/ослабления заключения. Набор этих аксиом зависит от класса программ, для которых проводится верификация, т. е. от проблемной области. В качестве наиболее распространенной базы можно задать все истинные утверждения исчисления предикатов первого порядка над массивами.


В работе [12] доказана следующая важная теорема о непротиворечивости аксиоматической семантики относительно операционной. Теорема. Система вывода HSC непротиворечива для свойства частичной корректности для троек языка С-light-kernel. Т. е. $\vdash_\mathrm{HSC}\phi$ влечет $\models\phi$.

Заключение

Описанный здесь язык C-light лежит в основе проекта, цель которого -- разработка системы верификации C-light-программ. Достоинство языка C-light состоит в том, что он составляет представительное подмножество языка C и позволяет работать с динамической памятью. Кроме того, язык C-light существенно расширяет Паскаль, для которого в 1991-1996 гг. была разработана система верификации программ СПЕКТР [14]. В качестве промежуточного языка системы был определен язык C-light-kernel. Являясь ядром языка C-light и, следовательно, подмножеством языка ANSI C, C-light-kernel позволяет существенно упростить аксиоматическую семантику входных программ, сохраняя при этом большую часть выразительной мощи языка С. Кроме того программы на языке Паскаль естественным образом транслируются в него, что позволяет проводить верификацию программ на этом языке, используя опыт системы СПЕКТР [13,14]. Важным достоинством языка C-light-kernel является то, что указатели языка C-light сохраняются в нем практически полностью. Для указателей была разработана проблемная область в виде аксиом, определяющих свойства ссылочных классов. Помимо создания операционной и аксиоматической семантик [11,12], важным результатом является доказательство свойства непротиворечивости аксиоматической семантики HSC относительно операционной. На основе непротиворечивой и небольшой по объему системы HSC был создан прототип генератора условий корректности, позволяющий автоматически порождать утверждения о свойствах программ -- условия корректности. Заметим, что эта выбранная двухуровневая схема предусматривает также формальное обоснование корректности трансляции языка C-light в язык C-light-kernel. Для этого необходимо полностью формально определить правила перевода и индуктивно доказать, что в процессе трансляции семантика программы сохраняется.

Литература

1
Apt K.R., Olderog E.R. Verification of sequential and concurrent programs. -- Berlin a.o.: Springer Verlag, 1991.

2
Black P.E., Windley Ph.J. Inference rules for programming languages with side effects in expressions // Proc. 9th Intern. Conf. on Theorem Proving in HOL. -- Berlin a.o.: Springer Verlag, 1996. -- P. 56-60. -- (Lect. Notes Comput. Sci.; Vol. 1125).

3
Elgaard J., Moller A., Schwartzbach M.I. Compile-time debugging of C programs working on trees // Proc. Europ. Symp. on Programming (ESOP2000). -- Berlin a.o.: Springer Verlag, 2000. -- P. 119-134. -- (Lect. Notes Comput. Sci.; Vol. 1782).

4
Fradet P., Gaugne R., Le Metayer D. Static detection of pointer errors: an axiomatisation and a checking algorithm // Proc. Europ. Symp. on Programming (ESOP96). -- Berlin a.o.: Springer Verlag, 1996. -- P. 125-140. -- (Lect. Notes Comput. Sci.; Vol. 1058).

5
Gurevich Y., Huggins J.K. The semantics of the C programming language // Proc. of the Intern. Conf. on Computer Science Logic. -- Berlin a.o.: Springer Verlag, 1993. -- P. 274-309. -- (Lect. Notes Comput. Sci.; Vol. 702).

6
Huggins J.K., Shen W. The static and dynamic semantics of C (extended abstract) // Local Proc. Int. Workshop on Abstract State Machines. -- Zurich, 2000. -- P. 272-284. -- (ETH TIK-Rep.; N 87).

7
Luckham D., Suzuki N. Verification of array, record and pointer operations in Pascal // ACM Trans. on Programming Languages and Systems, 1979. -- Vol. 1, N 2. -- P. 226-244.

8
Norrish M. C formalised in HOL // PhD thes., Computer Lab., Univ of Cambridge, 1998.

9
Plotkin G.D. A structure approach to operational semantics: Technical Rep. FN-19, Aarhus University, DAIMI, 1981.

10
Wilson R.P., Lam M.S. Efficient Context-Sensitive Pointer Analysis for C Programs // ACM SIGPLAN Notices, 1995. -- Vol. 30. -- N 6. -- P. 1-12.

11
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Часть 1. Язык C-light. -- Новосибирск, 2001. -- (препр. / РАН. Сиб. Отд-ние. ИСИ; N 84).

12
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Часть 2. Язык C-light-kernel и его аксиоматическая семантика. -- Новосибирск, 2001. -- (препр. / РАН. Сиб. Отд-ние. ИСИ; N 87).

13
Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. -- М.: Радио и связь, 1988.

14
Непомнящий В.А., Сулимов А.А. Проблемно-ориентированные базы знаний и их применение в системе верификации программ СПЕКТР // Известия РАН. Сер. "Теория и системы управления". -- 1997. -- N 2. -- C. 169-175.

Примечание

На пути к верификации С-программ ... 1
Работа частично поддержана грантами РФФИ 00-01-00909 и 01-01-06141 и молодежным грантом президиума СО РАН.

Ваши комментарии
[SBRAS]
[Головная страница]
[Конференции]
[СО РАН]

© 2001, Сибирское отделение Российской академии наук, Новосибирск
© 2001, Объединенный институт информатики СО РАН, Новосибирск
© 2001, Институт вычислительных технологий СО РАН, Новосибирск
© 2001, Институт систем информатики СО РАН, Новосибирск
© 2001, Институт математики СО РАН, Новосибирск
© 2001, Институт цитологии и генетики СО РАН, Новосибирск
© 2001, Институт вычислительной математики и математической геофизики СО РАН, Новосибирск
© 2001, Новосибирский государственный университет
Дата последней модификации Wednesday, 12-Sep-2001 11:17:40 NOVST