автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Формальная семантика C-LIGHT программ и их верификация методом Хоара

Российская академия наук Сибирское отделение Институт систем информатики им. А.П. Ершова

На правах рукописи

Промский Алексей Владимирович

ФОРМАЛЬНАЯ СЕМАНТИКА C-LIGHT ПРОГРАММ И ИХ ВЕРИФИКАЦИЯ МЕТОДОМ ХОАРА

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Новосибирск, 2004

Работа выполнена в Новосибирском государственном университете и в Институте систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук

Научный руководитель: кандидат физико-математических наук

Непомнящий В.А

Официальные оппоненты: доктор физико-математических наук

Серебряков В.А.

кандидат физико-математических наук Скопин И.Н.

Ведущая организация: Ярославский государственный университет

(г. Ярославль)

Защита состоится 28 декабря в 14 час. на заседании диссертационного совета К003.032.01 в Институте систем информатики им. А. П. Ершова Сибирского отделения РАН по адресу:

630090, г. Новосибирск, пр. ак. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале библиотеки ИСИ СО РАН (пр. ак. Лаврентьева, 6).

Автореферат разослан ноября 2004 г.

Ученый секретарь диссертационного совета К003.032.01 к.ф.-м.н.

Мурзин Ф.А

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность. Рост производительности компьютеров привел к росту размеров программ. Размеры и эффективность программ и коллективов, занимающихся их проектированием и сопровождением, не могут расти с одинаковой скоростью. При устоявшейся (и часто оптимистичной) оценке в одну ошибку на тысячу строк кода программы быстро могут стать неуправляемыми. Поэтому в ближайшие годы проблема надежности программного обеспечения может стать одним из основных вызовов для современных компьютерно-зависимых обществ.

До сих пор основным средством установления надежности программ в компьютерной индустрии остается тестирование. Оно же является и самым требовательным по времени и затратам. Поэтому рынок уже оказывает давление на разработчиков, требуя снижения издержек и развития академических исследований в области надежности программного обеспечения. Среди этих исследований важное место занимают методы формальной верификации программ.

Первым шагом на пути к верификации программ является формализация семантики языков программирования. Существенный вклад в эту область внесли исследования Д. Гриса, Э. Дейкстры, Р. Флойда, Ч. Э. Р. Хоара, Г. Плоткина. Среди отечественных авторов можно отметить А.П. Ершова, А.В. Замулина, С.С. Лаврова, А.А. Летичевского, В.А. Серебрякова и др. Из языков, для которых известны успешные результаты по формализации семантики, можно назвать языки Pascal, SML, Euclid, Eiffel. Однако для широко распространенных языков системного программирования успехи более скромные.

Среди таких языков большой интерес представляет язык С. Несмотря на появление и развитие более современных языков таких, как C + + и Java, язык С остается одним из самых распространенных в силу своих несомненных достоинств: низкоуровневые операции, быстрый код, компактное и легко переносимое ядро. К тому же система верификации для С могла бы стать базой для систем, ориентированных на язык C + + .

Проблема верификации С-программ заключается в принципиальной трудности адекватной формализации этого языка. Сказывается его низкий уровень — возможность работать со значениями в памяти на уровне отдельных байтов и даже битов. Многие аспекты поведения С-программ в международном стандарте ISO/IEC не специфицированы и зависят от реализации. Поэтому актуальна проблема выделения выразительного подмножества языка С, для которого возможна строгая формализация.

Выбор семантики становится решающим фактором для сложности верификации. Наиболее популярны операционный и аксиоматический подходы. Первый хорошо подходит для формального описания исполнения программ абстрактным интерпретатором, что удобно для низкоуровневых аспектов. Но верификация в операционной семантике является громоздкой. Аксиоматический подход более абстрактный, он позволяет порождать условия, гарантирующие корректность программ. Однако аксиоматизация низкоуровневых конструкций затруднительна или сталкивается с теоретическими ограничениями. Поэтому в известных работах либо рассматриваются ограниченные подмножества языка С, либо предлагается формальное определение практически всего С, но не ориентированное на верификацию. В качестве примеров можно назвать работы Л. Андерсена, П. Блэка, М. Бофингера, И. Гуревича и Д. Хаггинса, М. Норриша, Н. Параспиру и др. К тому же большинство авторов не рассматривали последний стандарт языка С (С99).

Таким образом, актуальна проблема разработки и обоснования метода верификации С-программ, разумно сочетающего достоинства операционной и аксиоматической семантик. Для этого в исходном языке выделяется ограниченное ядро, для которого возможно создание аксиоматической семантики. Исходные программы транслируются в это ядро с их последующей верификацией. Методы трансляции, сохраняющие эквивалентность программ, также актуальны, особенно с появлением таких платформ, как "Microsoft .Net", в которых может возникнуть задача трансляции между входными языками. Эквивалентные преобразования в С предлагались в работах М. Бокхолда, М. Хармана и др., однако корректность перевода не обосновывалась.

Наконец, актуально практическое воплощению теоретических методов упомянутой двухуровневой схемы верификации. Верификация программ на базе аксиоматической семантики использует генерацию условий корректности (УК). Из известных работ по генераторам можно назвать работы Р. Фраэра, Е. Грибомона, П. Хомейера, Д. Мартина, С. Игараши, Д. Лакхэма, Р. Лондона и Н. Сузуки. Также перспективным является дальнейшее развитие этих методов на основе концепции метагенерации, предложенной М. Морикони и Р. Шварцем. Метагене-рация может упростить процесс создания и расширения генераторов.

Цель и задачи диссертации. Целью диссертационной работы является исследование и разработка средств и методов формализации семантики C-light программ и их верификации методом Хоара.

Для достижения цели поставлены следующие задачи:

• Выделение представительного подмножества С-1%Ы: языка С99, расширенного операциями над динамической памятью и не содержащего конструкций, семантика которых существенно зависит от конкретной платформы. Создание формального определения языка С-%М в виде структурной операционной семантики, обладающей свойством детерминированности.

• Выделение в языке С-%М ядра С-кете1 и создание компактной и непротиворечивой аксиоматической семантики этого ядра.

• Разработка корректной системы правил перевода из языка С-

в язык С-кете1.

• Разработка (мета)генератора условий корректности для языка С-кете1 в двухуровневой системе верификации С-%Ы: программ.

Методы исследования. В работе использовались аппарат и методы математической логики, теории спецификации программ, структурного операционного подхода Плоткина, аксиоматического подхода Хоара и эквивалентных преобразований программ.

Научная новизна. В диссертационной работе получены новые научные результаты:

1. Структурная операционная семантика языка С-%М поддерживает представительное подмножество С99 и обладает свойством детерминированности вычисления выражений, что позволяет придавать смысл широкому классу программ.

2. Система правил перевода из языка С-%М в язык С-кете1 обладает свойством корректности. Для доказательства корректности вместо обычного понятия функциональной эквивалентности предложено новое понятие семантического расширения.

3. Разработанная аксиоматическая семантика языка С-кете1 является непротиворечивой и охватывает конструкции языка для работы с памятью. Благодаря двухуровневой схеме эта семантика применяется для верификации С-1%Ы: программ.

4. Новый метод метагенерации условий корректности ориентирован на модифицированную семантику Хоара и позволяет упростить порождаемые условия корректности.

Практическая ценность. Полученные результаты могут стать основой для разработки методов формализации и верификации программ на современных языках системного программирования. Предложенные

методы в большой степени независимы от конкретной среды и могут быть адаптированы и расширены для различных реализаций языка С или таких языков, как C + + , С#, Java.

Созданный прототип метагенератора УК используется для экспериментов в системе СПЕКТР-2, которая ориентирована на языки Pascal и C-light. Метагенерация позволила расширить систему правил вывода условий корректности правилами элиминации инвариантов циклов в программах линейной алгебры.

Аппробация работы. Основные положения работы докладывались на следующих научных конференциях:

1. Четвертый Сибирский Конгресс по Прикладной и Индустриальной математике (ИНПРИМ-2000), Новосибирск, Россия, 2000.

2. Конференция молодых ученых, посвященная 10-летию ИВТ СО РАН, Новосибирск, Россия, 2001.

3. Конференция, посвященная 90-летию со дня рождения А. А. Ляпунова, Новосибирск, Россия, 2001.

4. Международная конференция молодых ученых по математическому моделированию и информационным технологиям, Новосибирск, Россия, 2002.

5. International Conference "Perspectives of System Informatics", Novosibirsk, Russia, 2003.

Кроме того, полученные результаты обсуждались на совместных семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры программирования НГУ. Материалы диссертации вошли в отчеты по проектам РФФИ 00-01-00909 и 04-01-00114.

Публикации. По материалам диссертации опубликовано 11 работ.

Структура диссертации. Диссертация состоит из введения, пяти глав, заключения и приложений. Объем работы (за исключением приложений и библиографии) составляет 137 страниц в формате машинописного текста. Список литературы содержит 161 наименование.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновывается актуальность диссертации и формулируются ее цели, характеризуются научная новизна и практическая ценность работы.

В главе 1 приводятся базовые понятия, используемые в работе, и краткий исторический обзор.

Разд. 1.1 представляет современный взгляд на формальную верификацию программ. Упомянуты основные подходы: дедуктивные, методы проверки моделей, анализ типов и статический анализ.

В разд. 1.2 рассмотрены используемые в работе виды семантик: операционная и аксиоматическая. Структурная операционная семантика (СОС) в стиле Г. Плоткина (п. 1.2.2) позволяет задать абстрактный интерпретатор для языка программирования. Базовое понятие СОС — состояние, в классических работах оно определяется как отображение программных переменных во множество их значений. Для привязки состояния к конкретной точке программы используется понятие конфигурации. Это пара (S, а) — программный фрагмент S и состояние а. Абстрактная машина определяет аксиомы и правила вывода, описывающие бинарное отношение перехода на множестве конфигураций. Такое описание, позволяющее выдавать следующее состояние, называется семантикой мелкого шага (small-step style). Исполнение программы соответствует цепочкам конфигураций, связанных переходами. Вводя транзитивное рефлексивное замыкание отношения перехода, можно по программе и начальному состоянию выдавать сразу заключительное состояние. Это так называемая семантика крупного шага (big-step style).

Аксиоматическая семантика (п. 1.2.3) предлагает более высокий уровень абстракции. Она представляет собой формальную систему вывода утверждений о свойствах программ. Основными формулами в ней являются конструкции вида {Р} S {Q}, называемые тройками Хоара. Здесь S — это программа, а Р и Q — логические утверждения, называемые пред- и постусловием, соответственно. Интуитивно истинность тройки в смысле частичной корректности означает следующее: если перед исполнением программы истинно предусловие Р и программа S останавливается, то истинно постусловие Q. Свойства полноты и непротиворечивости логики Хоара обычно доказываются относительно исходной семантики СОС. В п. 1.2.5 сформулирована известная теорема Кларка о неполноте, которая описывает класс императивных языков, для которых недостижимо свойство полноты логики Хоара.

В разд. 1.3 рассмотрен основной объект изучения в диссертации — язык С. Приводятся краткий исторический обзор (п. 1.3.1) и особенности языка (п. 1.3.2), влияющие на практику его использования. Более подробно изложены проблемы его верификации (п. 1.3.3), в частности, рассмотрены особенности, перед которыми пасует классическая логика Хоара: недетерминизм вычислений, указатели, передача управления.

Разд. 1.4 содержит обзор некоторых теоретических работ по формализации семантики языка С и наиболее известных систем для анализа и верификации С-программ.

Глава 2 посвящена языку C-light и его структурной операционной семантике (СОС). Абстрактная машина языка C-light и СОС, задаваемая этой машиной, представляют основной материал данной главы.

В разд. 2.1 дается обзор языка C-light, который в основном является сравнением с языком С99. При этом для ряда элементов языка С99, не включенных в C-light, рассмотрены проблемы, возникающие при попытке их формализации. Для описания C-light в нем выделены типы, декларации, выражения, операторы и программы.

Допустимыми базовыми типами языка C-light являются все базовые типы языка С99 за исключением расширенных целых и комплексных. Допустимые составные типы включают указатели, массивы, структуры и функции. При этом на типы налагаются ограничения: 1) перечисления вводят не новые типы, а наборы констант типа signed int; 2) значения указателей — неинтерпретируемые символьные литералы. Допустимо приведение целого числа к типу указатель, но не наоборот; 3) запрещены указатели на функции; 4) неполные типы массивов разрешены только как типы аргументов функций; 5) в структурах запрещены битовые поля; 6) запрещены функции с переменным числом аргументов.

С декларациями связаны следующие ограничения: 1) множественные неокончательные определения для одного имени запрещены; 2) запрещены абстрактные декларации аргументов и спецификатор static в размере массива, являющегося параметром функции; 3) функция main не имеет параметров; 4) устаревший синтаксис определений функций (в стиле K&R) не поддерживается, требуются прототипы; 5) выделенные инициализаторы не поддерживаются; 6) запрещены все спецификаторы и модификаторы типов, кроме спецификаторов класса памяти, спецификаторов наличия знака и спецификаторов размера; 7) имена всех статических объектов в программе уникальны.

С выражениями связаны такие ограничения: 1) строго фиксирован порядок вычисления выражений; 2) побочные эффекты не откладываются до контрольных точек, а срабатывают на месте; 3) запрещены битовые операции, в том числе в составных присваиваниях; 4) составные литералы разрешены только в качестве инициализаторов; 5) приведение типов указателей ограничено приведением от void* к произвольному Т*; 6) для выделения/освобождения памяти используются операции

new и delete, позаимствованные из языка C + + .

Для операторов вводятся два ограничения: 1) все case-метки в операторе switch должны находиться на одном уровне вложенности; 2) запрещено передавать управление по goto внутрь блоков. Как и в C + + , запрещено передавать управление по goto в обход инициализации.

Программа на языке C-light — это последовательность внешних деклараций. На внешнем уровне можно объявить тип, функцию, структуру и данные. Кроме обычных конструкций С на верхнем уровне могут присутствовать и аннотации. В языке C-light препроцессор отсутствует, поскольку исходная программа препроцессируется до начала ее верификации. Не предусмотрена никакая предварительная компиляция. Модульность не поддерживается. Поэтому любая исходная C-light программа состоит из одного файла и пользовательские библиотеки верифицируются отдельно от программы, которая использует их.

В разд. 2.2 рассмотрен язык утверждений, используемый для выражения свойств программ и состояний языка C-light. В дополнение к типам языка C-light он вводит идентификаторы, абстрактные адреса, абстрактные имена типов, функции над дополнительными типами, декартовы произведения и типы локаторов объектов. Алфавит языка утверждений состоит из алфавита языка логики первого порядка, расширенного знаками пунктуации и символами операций языка C-light. Все базовые типы расширены неопределенным значением Выражения языка утверждений строятся стандартным образом и имеют префиксный синтаксис. Далее выражения типа _Воо1 называем просто утверждениями. Также индукцией по структуре выражений определяется понятие подстановки терма t вместо переменной и в выражении s, которая записывается в виде

В разд. 2.3 рассмотрена статическая часть абстрактной машины. Во-первых, в п. 2.3.1 модифицируется классическое понятие состояния. В абстрактной машине C-light состояние — это отображение, означивающее следующие метапеременные: 1) МеМ — переменная типа Names х Nat —у Locations, т.е. адресация объектов с учетом уровня их вложенности; 2) MD — переменная типа Locations CTypes. Она определяет значения, хранимые в памяти; 3) Г — переменная типа Names x Nat —> TypeSpecs. Она определяет типы значений объектов; 4) STD — переменная типа Names —» TypeSpecs, т.е. информация о тегах и синонимах типов; 5) Val — переменная типа CTypes x TypeSpecs, в которой хранится значение вычисленного выражения вместе с его типом.

При работе машины используются специальные функции. Они не являются функциями языка C-light и применяются только к состояниям. Перечислим основные: 1) Labels — функция, определяющая множество символических меток в блоке; 2) Cases — функция, определяющая множество меток-констант для оператора switch; 3) UnOpSem — функция, реализующая семантику унарных операций языка C-light; 4) BinOpSem — реализация семантики бинарных операций; 5) InstParms — реализация подстановки фактических аргументов вместо формальных параметров при вызове функции; 6) FindL(id) — определение уровня вложенности для имени id (разрешение области определенности); 7) 1р — реализация особого вида приведений — целочисленных протяжек.

Далее в п. 2.3.2 определяется система типов, сопоставляющая выражению его тип. Аксиомами этой системы являются утверждения о типах констант, которые включают числа, символы, строковые литералы, нулевой указатель. Правила вывода определяют типы более сложных выражений, содержащих идентификаторы, операции, вызовы функций.

В п. 2.3.3 расширяется классическое понятие конфигурации абстрактной машины. Теперь конфигурация — это тройка (S, a, If) — программа (фрагмент), текущее состояние и натуральное число If,, соотвествую-щее текущему уровню вложенности. Вводятся два бинарных отношения перехода между конфигурациями: 1) отношение для вычисления выражений: 2) отношение для исполнения операторов:

Произвольная аксиома СОС для любого отношения выглядит как

Она означает, что один шаг исполнения фрагмента А, начинающийся в состоянии а на уровне п, приводит в состояние т на уровне га и В — тот фрагмент исходной программы, который остается для исполнения. Произвольное правило семантики имеет вид

Это означает, что при выполнении условий Pi,...,Pn можно перейти от первой конфигурации ко второй.

Вводится ряд специальных значений, которые могут храниться в компоненте Val наряду с обычными значениями. Однако эти значения не имеют типов и сигнализируют о том или ином событии в ходе работы программы: 1) OkVal — нормальное завершение работы операто-ра/програмы; 2) GoVal(L) — был встречен оператор goto L; 3) BreakVal

— был встречен оператор break; 4) ContVal — был встречен оператор continue; 5) RetVal(u) — был встречен оператор return и v — возвращаемое значение; 6) CaseVal(c) — управление передано на метку case с: в операторе switch; 7) DefVal — управление передано на метку default: в операторе switch; 8) Fail — ошибка в программе.

В разд. 2.4 представлена динамическая часть абстрактной машины, задающая отношения перехода. Аксиомы и правила разбиты на три группы: вычисление выражений (п. 2.4.1), обработка деклараций (п. 2.4.2), исполнение операторов (п. 2.4.3). В качестве примера типичного правила СОС выбрано правило для присваивания:

где аI = a-a(MD <- upd(MD,с,7r2,nM))(Val ^(Ъ2,пЫ,п)). Т.е.

вычисление присваивания разбито на следующие шаги: 1) с помощью системы типов проверяем, что е1 — это модифицируемое /-значение; 2) вычисляем правую часть присваивания и запоминаем результат с его типом в Val; 3) вычисляем левую часть, одновременно определяя адрес объекта, обозначаемого выражением е1 4) определяем, связаны ли типы левого и правого подвыражений отношением приводимости; 5) значение е2 приводим к типу левой части с помощью отображения 6) это окончательное значение помещаем по адресу модифицируемого объекта и объявляем его значением всего выражения присваивания.

Наконец в п. 2.4.4 определяется семантика частичной корректности М. и рассматриваются некоторые ее свойства. Отображение М строится на базе транзитивного рефлексивного замыкания отношения —>s. По программе (фрагменту) и входному состоянию оно выдает множество заключительных состояний. При этом также происходит расширение класического метода. Входом отображения может быть как допустимая программа, так и произвольный фрагмент. В случае фрагмента семантика определяется с точностью до уровня вложенности. Чтобы обрабатывать передачу управления во фрагменте, к нему добавляется специальная конструкция, связанная с обработкой блоков. Главными свойствами СОС являются детерминизм и отсутствие блокировки.

В главе 3 представлен язык C-kernel, определена интерпретация языка утверждений в виде денотационной семантики и описана аксио-

матическая система HSC для языка C-kemel.

Разд. 3.1 содержит описание языка C-kemel. Являясь ядром языка C-light, он отбрасывает конструкции, не поддающиеся формализации в логике Хоара. Любая декларация объявляет ровно один идентификатор, а спецификаторы static и auto обязательны.

При вычислении любого выражения в C-kemel допускается не более одного изменения содержимого памяти, т.е. побочные эффекты в выражениях единичны. Допустимыми операциями являются только следующие: первичные (О, [], ".", ->), унарные (*, -), бинарные (*, /,'/., +, простое присваивание, выделение/освобождение памяти, приведение типа.

Запрещены цепочки присваиваний вида а=Ь=с. В C-kemel нет операции «запятая», поэтому любой оператор вычисления выражения есть либо выражение присваивания, либо вызов процедуры. Фактическим аргументом функции может быть константа либо переменная.

В языке C-kemel разрешены следующие операторы: 1) оператор-выражение; 2) условный оператор if с обязательной ветвью else (возможно, пустой); 3) оператор цикла while, условием которого может быть только выражение без побочных эффектов; 4) оператор передачи управления goto; 5) оператор возврата значения return, причем выражением в нем может быть только константа или переменная; 6) блок.

В разд. 3.2 обосновывается связь операционной семантики языка C-light и аксиоматической семантики языка C-kernel. Эта связь задается посредством интерпретации языка утверждений с помощью состояний абстрактной машины, тем самым логические утверждения (пред-, постусловия и инварианты) задают множества состояний, в которых они истинны. При этом доказывается стандартная лемма о подстановке, связывающая обновления состояний и подстановки в утверждениях.

В разд. 3.3 представлена аксиоматическая система HSC для языка C-kemel. В системе HSC происходит вывод троек Хоара в окружении. Окружение £nv — это тройка: имя текущей функции, текущий уровень вложенности и множество гипотез, связанных с вызовами функций и передачей управления. В качестве примера приведено правило для присваивания переменной результата вызова функции.

{Р'} {(х) {Q1} е £nv £nv hP=> (Р'а A (Q'7(Val <- г)) => Q-y(36)

Подстановки осуществляют такие действия, как отбрасывание

локальных объектов в точке вызова, замену формальных параметров фактическими аргументами и переименование метапеременных.

Выводимость тройки ф в системе ШС в окружении £пу обозначаем как £пу Ьнэс Ф- Также в ШС вводится новое понятие частичной корректности. ТройкаХоара {Р} Б {ф} истинна в смысле частичной корректности в окружении £пу (обозначение «V [= {Р} 5 {<Э}), если

1. V а, если а |= Р и (5, а, 1/(£пь)) -»* (£, а', Ц(£пу)), то а' |=

2. V Ь € ЬаЬеЦБ) V а такого, что а |= 1пь(Ь), если

Наконец в разд. 3.4 проводится доказательство основной теоремы о непротиворечивости системы НЕС.

Теорема 1. Система вывода ШС непротиворечива для свойства частичной корректности, т.е. £ш Ьнэс Ф влечет £ш ф.

Глава 4 содержит описание системы правил перевода из языка С-%М в язык С-кете1. Правила сгруппированы в соответствии с их предназначением: перевод деклараций (разд. 4.1), перевод операторов (разд. 4.2) и перевод выражений (разд. 4.3). В некоторых группах правила, в свою очередь, разбиты на правила элиминации, правила декомпозиции и правила нормализации. В качестве примера рассмотрим правило для перевода постфиксного инкремента: Мпс. Фрагмент вида е++

заменяется на фрагмент

где д, у — новые переменные, объявленные с типами выражений &е и е, соответственно.

Ряд свойств предложенной системы правил перевода рассмотрен в разд. 4.4. К этим свойствам относятся завершимость алгоритма перевода и нормализованность его выхода, т.е. принадлежность результирую-ще программы языку С-кегпе1.

Необходимые для обоснования корректности сведения рассмотрены в разд. 4.5. Они включают следующие определения. Программа на языке С-И^ — это либо обычный набор внешних деклараций, либо определение одной функции. Множеством семантических объектов программы Е называется множество ОЬ^) идентификаторов функций и всех

статических переменных программы. Множеством семантических объектов функции f называется множество Obj(f) идентификаторов автоматических и статических переменных функции f. Атрибут идентификатора id, принадлежащего множеству семантических объектов, — это либо пара (т, storage), если id — переменная типа г с классом памяти storage, либо сигнатура функции, если id — имя функции.

Правила перевода вводят новые переменные, что позволяет ввести понятие объектного расширения. Программа (функция) Т называется объектным расширением программы (функции) S относительно взаимно-однозначного всюду определенного отображения ф из Obj (S) в Obj(T), если для любого id € Obj(S) атрибут имени (id) совпадает с атрибутом для <^(id), т.е. множество объектов программы (функции) Т получено переименованием объектов программы (функции) S и расширено новыми объектами. Обозначаем объектное расширение как S <ф Т.

Существование такого отображения еще не означает, что программы реализуют одну и ту же вычислимую функцию. Для этого требуется проверить совпадение значение объектов, связанных отображением ф. Программа Т называется семантическим расширением программы S, если существует всюду определенное взаимно-однозначное отображение такое, что

2) для любого начального состояния <т, для любого семантического объекта id его значение в заключительном состоянии совпадает со значением объекта в состоянии

3) для любой пары функций fi 6 S и f2 6 Т таких, что ф(Ь ) — существует всюду определенное взаимно-однозначное отображение Ф(f,,f2): Obj(fi) U Obj(S) -> Obj(f2) U Obj(T) такое, что свойства (1) и (2) рекурсивно выполнены для этих функций и расширенных множеств объектов.

Семантическое расширение обозначается как S =<!ор Т. Это отношение рефлексивно и транзитивно (т.е. является предпорядком). Однако на статических объектах можно ввести эквивалентность. Обозначим множество статических объектов произвольной функции f как Sobj(f). Если в определении семантического расширения заменить множестваiObj(fi) HaSobj(fi), то полученное отношение станет эквивалентностью. Обозначается семантическая эквивалентность как S Т.

Обоснование корректности системы правил перевода содержится в разд. 4.6. Основной результат формулируется в виде теоремы.

Теорема 2. Для любого правила перевода R и любой программы S на языке C-light S =^0р R(S).

Правила перевода не расширяют множество статических объектов программы, что позволяет доказать важное следствие. Следствие. Для любой программы S на языке C-light и для любого правила перевода R из языка C-light в C-kernel

Глава 5 посвящена реализации системы HSC в виде прототипа генератора условий корректности. В разд. 5.1 рассмотрено понятие модифицированной семантики и приводится обобщенная схема автоматизированной системы верификации программ.

В разд. 5.2 рассмотрена формальная база для использования логической системы HSC для вывода условий корректности. Как и в обычной логике Хоара вывод в этой системе имеет недетерминированный характер, поскольку на каждом шаге применимо не единственное правило вывода. Решением является стратегия обратного просмотра, когда на правила вывода применяются для последней конструкции в программе, а вся предыдущая часть программы становится контекстом. В п. 5.2.1 рассмотрен входной язык генератора УК. Его независимая нотация позволяет задавать широкий класс императивных языков, в частности C-kemel и Pascal. В п. 5.2.2 вводится определение нормальной формы правил вывода. В п. 5.2.3 приводится схеме генератора УК в системе СПЕКТР-2.

Разд. 5.3 посвящен перспективному расширению метода генерации УК — метагенерации. Этот подход, в сочетании с независимым представлением, позволяет создать инструментарий для автоматизированного порождения генераторов УК по аксиоматической системе. Для этого вводятся понятия общей и нормальной формы правил вывода и описывается алгоритм перевода их общей формы в нормальную.

Приложение А содержит пример вывода условий корректности для рекурсивной процедуры обращения массива. Указаны 4 условия корректности для самой процедуры и условие корректности всей программы. Истинность условий была доказана вручную.

Приложение В описан эксперимент для прототипа метагенера-тора. Продемонстрирован фрагмент генератора условий корректности для части языка C-kemel, расширенной правилами элиминации инвариантов циклов для программ линейной алгебры. Генератор в виде рекурсивной ML-функции построен метагенератором.

Основные выводы и результаты. В рамках диссертации получены

следующие результаты.

• Выделено представительное подмножество языка С, расширенное операциями для работы с динамической памятью и названное языком С-Щ^! Для этого языка была создана структурная операционная семантика и семантика частичной корректности.

• Выделено ядро языка С-%Ы: — язык С-кегпе1 и создана аксиоматическая семантика НЕС для этого ядра. Введено новое понятие частичной корректности для троек Хоара в окружении. Доказана непротиворечивость системы НЕС.

• Разработана система правил перевода из языка С-%М в язык С-кегпе1. Предложено новое понятие семантического расширения. Доказана корректность системы правил перевода.

• Реализован прототип генератора условий корректности для языка С-кете1. Также предложен новый алгоритм метагенерации, способный порождать генераторы УК по исходной аксиоматической системе. Проведены успешные эксперименты с генератором УК.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Пром-ский А.В. На пути к верификации С-программ. Язык С-1%Ы: // Конференция посвященная 90-летию со дня рождения А.А. Ляпунова (пленарные доклады). — Новосибирск, 2001. — С. 423-432.

2. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Пром-ский А. В. На пути к верификации С-программ. Часть 1. Язык С-%И1

- Новосибирск, 2001. - 48 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 84).

3. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Пром-ский А. В. На пути к верификации С-программ. Часть 2. Язык С-К^-кегпе1 и его аксиоматическая семантика. — Новосибирск, 2001. — 58 с.

- (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 87).

4. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Пром-ский А.В. На пути к верификации С программ. Часть 3. Перевод из языка С-%М в язык С-%Ы:-ке1пе1 и его формальное обоснование. — Новосибирск, 2002. - 82 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 97).

5. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Пром-ский А.В. На пути к верификации С программ. Язык С-1%Ы: и его

формальная семантика. // Программирование. — 2002. — N 6. — С. 1-13.

6. Непомнящий В.А., Ануреев И.С, Михайлов И.Н., Пром-ский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. — 2003. — N 6. — С. 1-16.

7. Промский А.В. Операционная и аксиоматическая семантики языка Си // Четвертый сибирский конгресс по прикладной и индустриальной математике (ИНПРИМ-2000). Тезисы докладов, часть П. — Новосибирск: Изд-во Института математики СО РАН, 2000. — С. 125.

8. Промский А.В. Формальная семантика указателей языка C-light // Материалы конференции молодых ученых, посвященной 10-летию Института вычислительных технологий СО РАН, T.I. — Новосибирск, 2001. - С. 62-65.

9. Промский А.В. Автоматическая генерация условий корректности в системе верификации программ // Международная конференция молодых ученых по математическому моделированию и информатике. Тезисы докладов. — Новосибирск: Изд-во Института математики СО РАН, 2002. - С. 67.

10. Промский А.В. Генерация и метагенерация условий корректности в системе СПЕКТР-2. — Новосибирск, 2003. — 50 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 103).

11. Nepomniaschy V. A., Anureev I. S., Promsky A. V. Verification-oriented language C-light and its structural operational semantics (extended abstract) // 5th International A. Ershov conference "Perspectives of System Informatics" (PSI 2003). - Springer, Berlin, 2003. - P. 103-111. — (Lect. Notes Comput. Sci.; 2890).

Личный вклад автора. Все включенные в диссертацию результаты, касающиеся формализации семантик языков C-light и C-kernel, и доказательства двух основных теорем получены автором самостоятельно. Система правил перевода разработана автором в сотрудничестве с И.Н. Михайловым. Свойства завершимости алгоритма перевода и нормализации его выхода были доказаны И.С. Ануреевым. Автором самостоятельно проведены и описаны эксперименты с прототипом (ме-та)генератора в системе СПЕКТР-2.

Отпечатано в ЗАО РИЦ «Прайс-курьер», тел 307-202, зак. № 55У .тираж 400

-¿636 5

Введение

1 Предварительные понятия

1.1 Формальная верификация программ.

1.2 Используемые виды семантик.

1.2.1 Денотационная семантика.

1.2.2 Структурная операционная семантика.

1.2.3 Аксиоматическая семантика.

1.2.4 Пример верификации.

1.2.5 Вопросы полноты и непротиворечивости.

1.3 Язык С.

1.3.1 История языка.

1.3.2 Особенности языка

1.3.3 Проблемы верификации языка С.

1.4 Обзор известных работ и систем.

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

2.1 Язык C-light.

2.1.1 Типы

2.1.2 Декларации.

2.1.3 Выражения.

2.1.4 Операторы.

2.1.5 Программы.

2.2 Язык утверждений

2.3 Абстрактная машина языка C-light.

2.3.1 Состояния абстрактной машины языка C-light

2.3.2 Конфигурации абстрактной машины языка C-light.

2.3.3 Система типов.

2.4 Динамическая операционная семантика

2.4.1 Семантика выражений.

2.4.2 Семантика деклараций.

2.4.3 Семантика операторов

2.4.4 Семантика частичной корректности.

3 Язык C-kernel и его аксиоматическая семантика

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

3.2 Связь аксиоматической семантики с операционной.

3.2.1 Интерпретация выражений.

3.2.2 Значение логических утверждений

3.2.3 Лемма о подстановке.

3.3 Система HSC.

3.4 Непротиворечивость системы HSC

4 Перевод из языка C-light в язык C-kernel

4.1 Переписывание деклараций.

4.1.1 Уточнение класса памяти.

4.1.2 Разбиение списка деклараторов.

4.2 Переписывание операторов.

4.2.1 Нормализация операторов.

4.2.2 Элиминация операторов

4.3 Переписывание выражений.

4.3.1 Правила элиминации.

4.3.2 Правила декомпозиции.

4.3.3 Правила нормализации.

4.4 Некоторые свойства системы правил.

4.5 Корректность перевода: предварительные понятия.

4.6 Теорема о корректности перевода.

5 Генерация и метагенерация условий корректности

5.1 Автоматизация вывода условий корректности.

5.1.1 Модификация аксиоматической семантики.

5.1.2 Автоматизированные системы верификации.

5.2 Генерация УК в системе СПЕКТР

5.2.1 Входной язык генератора УК.

5.2.2 Нормальная форма правил.

5.2.3 Схема генератора УК.

5.3 Метагенерация условий корректности.

5.3.1 Общая форма правил.

5.3.2 Алгоритм перевода из общей формы в нормальную.

В диссертации развит аппарат формализации семантик языков C-light и C-kernel, исследован вопрос корректности преобразований С-программ и их влияния на верификацию, разработаны логические средства для верификации C-light программ методом Хоара.

Актуальность темы

Тысячекратный рост производительности компьютеров за последние 25 лет привел к росту размеров программ в тех же пропорциях. Область применения огромных программ (от 1 до 40 млн. строк) значительно увеличилась за последнее десятилетие. Для таких больших программ является необходимым требование разработки по разумной цене и дальнейшей модификации и поддержки в течении всего их жизненного цикла (часто более 20 лет). Размеры и эффективность программ и коллективов, занимающихся их проектированием и сопровождением, не могут расти в одинаковых пропорциях. При достаточно устоявшейся (и зачастую оптимистичной) оценке в одну ошибку на тысячу строк кода такие программы быстро могут стать неуправляемыми. Поэтому в ближайшие 10 лет проблема надежности программного обеспечения может стать одним из основных вызовов для современных компьютерно-зависимых обществ.

До сих пор основным средством установления надежности программ в компьютерной индустрии остается тестирование [17,84]. Оно же является и самым требовательным по времени и затратам. В качестве подтверждения можно перечислить следующие факты [91]: половина всех инженеров компании Microsoft занимаются тестированием; половина своего времени разработчики тратят на тестирование; промежуток времени между фазами 'Code Complete' и 'Release to Manufacture' составляет б и более месяцев. В отчете 2002 года по использованию компьютеров в США [157] отмечалось, что потери от неадекватного тестирования программ составили 60 млрд. $, причем две трети этой суммы — это потери пользователей и одна треть — разработчиков.

В связи с этим рынок уже оказывает давление на разработчиков, требуя снижения этих издержек1 и, что особенно важно, возобновления интереса к чисто академическим исследованиям в области надежности программного обеспечения. Среди этих исследований важное место занимают методы формальной верификации программ.

Первым шагом на пути к верификации программ является формализация семантики

1 Здесь показателен пример, когда вся команда разработчиков Microsoft Windows (более 8000 инженеров) весь февраль 2002 г. занималась не своей непосредственной работой, а вопросами безопасности [91]. Такие перерывы в работе дороги, но еще дороже обходится «деятельность» последних сетевых вирусов. языков программирования. Наибольшее влияние на формирование этой области оказали исследования Д. Гриса, Э. Дейкстры, Р. Флойда, Ч. Хоара, Г. Плоткина [5,6,75,90,143]. Среди отечественных авторов можно отметить А.П. Ершова, А.В. Замулина, С.С. Лаврова, А.А. Летичевского, В.А. Серебрякова [7,8,10,11,14,15,30]. Из языков, для которых были получены успешные результаты по формализации семантики, можно назвать языки Pascal, SML, Euclid, Eiffel [93,113,117,119]. Однако по сравнению с теорией синтаксического анализа успехи в области автоматизированной формализации семантик более скромные [120,130,133,137,145,154]. А для распространенных языков системного программирования часто нет даже просто полной формальной семантики (без программной поддержки).

Среди таких языков большой интерес представляет язык С [147]. Область применения С огромна: от авионики и операционных систем до программного обеспечения для бытовой техники. Несмотря на появление и развитие более современных языков таких, как С++ и Java, язык С остается одним из самых распространенных в силу своих несомненных достоинств: поддержка низкоуровневых средств, быстрый код, компактное и легко переносимое ядро. К тому же система верификации для С могла бы стать базой для систем, ориентированных на язык С++.

Основная проблема верификации С-программ заключается в принципиальной трудности адекватной формализации его семантики. Во-первых, сказывается его низкий уро-. вень — возможность работать со значениями в памяти на уровне отдельных байтов и даже битов. Во-вторых, этот язык получил широкое распространение задолго до его стандартизации и тем более формального определения. Поэтому многие аспекты поведения С-программ в международном стандарте ISO/IEC просто не специфицированы. Сам же стандарт, будучи большей частью написан на обычном английском языке, содержит двусмысленности и неясности, присущие любому человеческому языку. Рабочая группой WG14 комитета ISO регулярно анализирует возникающие ошибки [101] и вносит исправления, однако даже последний стандарт [147] не снял всех вопросов. Поэтому актуальна проблема выделения выразительного подмножества языка С, для которого возможно создание строгой формальной семантики.

Как известно, выбор семантики для конструкций языка становится решающим фактором для сложности верификации [41]. В настоящее время наиболее популярны операционный [143,144] и аксиоматический [90,93] подходы. Первый хорошо подходит для формального описания исполнения программ некоторым абстрактным интерпретатором, что позволяет моделировать реальное поведение в конкретных системах. Однако попытки верификации в операционной семантике приводят к громоздким доказательствам [133]. Аксиоматический подход более абстрактный, его правила позволяют порождать условия, гарантирующие корректность программ. Однако аксиоматическая семантика низкоуровневых конструкций затруднительна или сталкивается с теоретическими ограничениями, связанными с вопросами полноты и непротиворечивости [47,62,63,69].

Все это приводит к тому, что в известных работах либо формализуются и верифицируются ограниченные подмножества языка С, либо предлагается формальное определение для практически всего С, но не ориентированное на верификацию. В качестве примеров можно назвать работы Андерсена, Блэка, Бофингера, Гуревича и Хаггинса, Норриша, Параспиру, Субраманиана и др. [40,49,54,83,98,133,140,154]. К тому же в большинстве указанных работ не рассматривался последний стандарт языка С (здесь и далее С99).

Таким образом, актуальна проблема разработки и обоснования метода верификации С-программ, разумно сочетающего достоинства операционной и аксиоматической семан-тик. Исследователи все чаще обращают внимание на двухуровневую схему. В соответствии с ней в исходном языке выделяется ограниченное ядро, допускающее создание аксиоматической семантики. Исходные программы транслируются в это ядро с их последующей верификацией. Другим вариантом схемы может быть определение двух различных языков с трансляцией из одного в другой. Однако пример схемы с формально обоснованной схемы до сих пор неизвестен. Методы трансляции программ, сохраняющие эквивалентность, также являются актуальной темой исследований, особенно с развитием машинно-независимых платформ, как например Microsoft .Net, в которых может возникнуть задача трансляции между языками, ориентированными на них. В нашей стране и за рубежом проводились исследования по этой теме [4,7,8,13,16,33,44,61,87,118,122], однако в основном они были связаны со слишком общими схемами программ, что может привнести излишнюю сложность, либо проводились в контексте задачи оптимизации. Из работ непосредственно связанных с эквивалентными преобразованиями в С известны работы [50,51,85], однако корректность преобразований в них не обосновывалась.

И наконец, актуальными являются исследования по практическому воплощению теоретических методов данной двухуровневой схемы верификации. Верификация программ в аксиоматической семантике базируется на генерации условий корректности (УК). Из известных работ по генераторам УК можно назвать [46,77,79,96,97,100,114]. И наибольший интерес в данной области представляет метод автоматизированного создания генераторов УК — метагенерация [121]. Благодаря этому методу можно будет не только легко расширять системы верификации новыми конструкциями конкретного языка программирования, но и включать в системы новые языки, делая системы многоязыковыми, и следовательно более привлекательными для пользователей.

Цель и задачи диссертации

Целью диссертационной работы является исследование и разработка средств формализации семантики C-light программ и их верификации методом Хоара.

Для достижения цели поставлены и решены следующие задачи:

• Определение языка C-light, базирующегося на представительном подмножестве языка С99, позволяющего работать с динамической памятью и не содержащего конструкций, семантика которых существенно зависит от конкретной платформы.

• Создание формального определения языка C-light в виде структурной операционной семантики, обладающей свойствами независимости от платформы и детерминированности.

• Выделение в языке C-light ядра C-kernel и создание компактной и непротиворечивой аксиоматической семантики этого ядра.

• Разработка корректной системы правил перевода из языка C-light в язык C-kernel.

• Разработка прототипа (мета)генератора условий корректности для языка C-kernel в двухуровневой системе верификации C-light программ методом Хоара.

Методы исследования

В работе использовались аппараты и методы математической логики, теории спецификации программ, структурного операционного подхода Плоткина, аксиоматического подхода Хоара и эквивалентных преобразований программ.

Научные результаты, вынесенные на защиту

В диссертационной работе получены новые научные результаты:

1. Структурная операционная семантика языка C-light поддерживает представительное подмножество С99, обладает свойством детерминированности вычисления выражений и независимости от конкретной архитектуры, что позволяет придавать смысл более широкому классу программ.

2. Система правил перевода из языка C-light в язык C-kernel обладает свойством корректности. Для доказательства этого свойства вместо обычных понятий функциональной или логико-термальной эквивалентности предложено новое понятие семантического расширения.

3. Непротиворечивая аксиоматическая семантика языка C-kernel с новой моделью языка утверждений. Расширение языка утверждений новыми типами высоких порядков позволило формально представлять указатели и области определенности идентификаторов. Благодаря двухуровневой схеме эта семантика фактически применяется для верификации C-light программ.

4. Новый метод метагенерации условий корректности, ориентирован на модифицированную семантику Хоара и позволяет упростить порождаемые условия корректности.

Научная и практическая ценность

Полученные результаты являются основой для разработки методов формализации и верификации программ написанных на современных языках системного программирования.

Предложенные принципы и средства в большой степени независимы от конкретной среды и могут быть адаптированы и расширены для различных реализаций языка С, а также стать базой для исследования языков прямо или косвенно происходящих из языка С: С++, С#, Java.

Созданный прототип метагенератора условий корректности используется для экспериментов в системе СПЕКТР-2, которая не зависит от входного языка и может служить основой для разработки промышленной версии системы. Метагенерация позволила расширить систему правилами элиминации инвариантов циклов в программах линейной алгебры. Система правил переписывания была использована П. Караваевым в его входном анализаторе для системы СПЕКТР-2. Также эта система стала основой для системы переписываний в языке С#, разработчиком которой является И. В. Дубрановский.

Доклады и печатные публикации

Основные положения работы докладывались на четвертом сибирском конгрессе по прикладной и индустриальной математике «ИНПРИМ-2000» (Новосибирск, 2000 г.), на конференции молодых ученых, посвященной 10-летию ИВТ СО РАН (Новосибирск, 2001 г.), на конференции, посвященной 90-летию со дня рождения А. А. Ляпунова (Новосибирск, 2001 г.), на международной конференции молодых ученых по математическому моделированию и информационным технологиям (Новосибирск, 2002 г.), а также на международной конференции "Perspectives of System Informatics" (Новосибирск, 2003 г.).

Кроме того, полученные результаты обсуждались на совместных семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры программирования НГУ. Материалы диссертации вошли в отчеты по проектам РФФИ 00-01-00909 (1999-2001) и 0401-00114.

По материалам диссертации опубликовано 11 работ [24-29,35-38,127]. Структура и объем диссертации

Диссертация состоит из введения, пяти глав, заключения и приложений. Объем работы (за исключением приложений и библиографии) составляет 130 страниц в формате машинописного текста. Список литературы содержит 166 наименований.

Заключение

В рамках диссертации были получены следующие результаты.

• Выделено представительное подмножество языка С99, расширенное операциями для работы с динамической памятью, названное языком C-light. Для этого языка была создана структурная операционная семантика (семантика мелкого шага) и базирующаяся на ней семантика частичной корректности (семантика крупного шага).

• Выделено ядро языка C-light — язык C-kernel и создана аксиоматическая семантика HSC для этого ядра. Введено новое понятие частичной корректности для троек Хоара в окружении, учитывающее произвольные передачи управления в программе. Язык утверждений, используемый для записи спецификаций, способен формализовать работу с указателями и понятие времени жизни объектов. Доказана непротиворечивость системы HSC.

• Разработана система правил перевода из языка C-light в язык C-kernel. Предложено новое понятие семантического расширения и новый способ определения семантической эквивалентности. Доказана корректность системы правил перевода.

• Реализован прототип генератора условий корректности для языка C-kernel. Также предложен новый алгоритм метагенерации, способный автоматически порождать подобные генераторы по исходной аксиоматической системе. Проведены эксперименты с генератором.

Остановимся на достоинствах подхода, представленного в настоящей работе. Двухуровневая схема позволяет охватить значительное подмножество языка С, оставаясь при этом на позициях, близких к классическим подходам Хоара, Апта, Дейкстры и др. Широкий охват языка позволяет сделать систему СПЕКТР-2 интересной для многих исследователей. Близость к классическим подходам позволяет применять стандартные способы исследования свойств семантики и обоснования корректности.

Фиксация порядка вычисления выражений в операционной семантике языка C-light не является основополагающей и жестко заданной. Фактически она определяется порядком посылок в некоторых правилах. Поэтому смена порядка вычисления выражений — это простой процесс. Более того, практически все аспекты поведения С-программ, для которых стандарт оставляет свободу выбора, задаются с помощью абстрактных функций машины. Эти функции фактически являются параметрами абстрактной машины. Смена порядка и этих «параметров» позволит ориентировать СОС для языка C-light на различные реализации и архитектуры.

Практическую ценность подтвердили эксперименты, проведенные с метагенератором

УК в системе СПЕКТР-2. Весьма удобным оказалось независимое представление входного языка генератора УК. Оно позволило не только работать с языками C-light и C-kernel, но и с языком Pascal при его фактической трансляции в язык C-kernel. Благодаря этому, опыт верификации для различных проблемных областей, накопленный в предыдущей системе СПЕКТР, достаточно просто переносится в систему СПЕКТР-2.

Стройная система правил перевода и метод обоснования ее корректности нашли свое применение в проекте верификации программ на языке С#, также развиваемом в лаборатории теоретического программирования ИСИ СО РАН.

1. Агафонов В.Н. Спецификация программ: понятийные средства и их организация. — Новосибирск: Наука, 1987. — 240 с.

2. Бочков С.О., Субботин Д.М. Язык программирования Си для персонального компьютера. — М.: Радио и связь, 1990. — 384 с.

3. Вирт Н. Алгоримы и структуры данных. — М.: Мир, 1989. — 360 с.

4. Глушков В.М. Теория автоматов и формальные преобразования микропрограмм // Кибернетика. 1965. — N 5. — С. 1-9.

5. Грис Д. Наука программирования. — М.: Мир, 1984. — 416 с.

6. Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978. — 275 с.

7. Ершов А.П. Избранные труды / Отв. ред. И.В. Поттосин. — Новосибирск: Наука, 1994. 416 с.

8. Ершов А.П., Ляпунов А.А. О формализации понятия программы // Кибернетика. 1967. — N 5. — С. 40-57.

9. Замулин А.В. Формальные методы спецификации программ (Учебное пособие). — Новисибирск: НГУ, 1999. —81 с.

10. Замулин А.В. Формальная семантика выражений и операторов языка Java // Программирование. — 2003. — N 5. — С. 31-45.

11. Замулин А.В. Алгераическая семантика императивного языка программирования // Программирование. — 2003. — N 6. — С. 51-64.

12. Керниган В., Ритчи Д. Язык программирования Си. — М.: Финансы и статистика, 1985.

13. Котов В.Е., Сабельфельд В.К. Теория схем программ. — М.: Наука. Гл. ред. физ.-мат. лит., 1991. — 248 с.

14. Лавров С.С. Программирование. Математические основы, средства, теория. — СПб.: БХВ-Петербург, 2001. 320 с.

15. Летичевский А.А. Синтаксис и семантика формальных языков // Кибернетика.- 1968. N 4. - С. 1-9.

16. Летичевский А.А. Эквивалентность и оптимизация программ // Теория программирования. — Новосибирск, 1972. — Ч. 1. — С. 166-180.

17. Майерс Г. Искусство тестирования программ. — М.: Финансы и статистика, 1982.- 176 с.

18. Массер Д. Спецификация абстрактных типов данных в системе AFFIRM // Требования и спецификации в разработке программ. — М.: Мир, 1984. — С. 199—222.

19. Непейвода Н. Н., Скопин И. Н. Основания программирования. — Ижевск-Москва: РХД, 2003. 926 с.

20. Непомнящий В.А. Об одном методе распознавания эквивалентности схем программ и дискретных преобразователей // Труды Всесоюз. конф. по программированию (ВКП-2). Новосибирск, 1970. - Вып. К. - С. 49-63.

21. Непомнящий В.А. О проблемно-ориентированной верификации программ // Программирование. — 1986. — N 1. — С. 3-12.

22. Непомнящий В.А. Верификация программ над массивами // Системная информатика. — Новосибирск, 1993. — Вып. 3. — С. 68—98.

23. Непомнящий В.А. Верификация финитной итерации над наборами структур данных // Программирование. — 2002. — N 1. — С. 3-12.

24. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С-программ. Язык C-light // Конф., посвященная 90-летию со дня рождения А.А. Ляпунова (пленарные доклады). — Новосибирск, 2001. — С. 423-432.

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

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

27. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Часть 3. Перевод из языка C-light в язык C-light-kernel и его формальное обоснование. — Новосибирск, 2002. — 82 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 97).

28. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика. // Программирование. — 2002. — N 6. — С. 1-13.

29. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. — 2003. — N 6. — С. 1-16.

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

31. Непомнящий В.А., Сулимов А.А. Верификация программ линейной алгебры в системе СПЕКТР // Кибернетика и системный анализ. — 1992. — N 5. — С. 136-144.

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

33. Подловченко Р.И. Функциональная и другие эквивалентности схем программ //. Проблемы кибернетики. — М.: Наука, 1979. — Вып. 35. — С. 185-198.

34. Пратт Т., Зелковиц М. Языки программирования: разработка и реализация (4-е изд.) / Под общей ред. А. Матросова. — СПб.: Питер, 2002. — 688 с.

35. Промский А.В. Операционная и аксиоматическая семантики языка Си // (ИНПРИМ-2000): Тез. докл. / Четвертый сибирский конгресс по прикладной и индустриальной математике. — Новосибирск, 2000. — Ч. 2. — С. 125.

36. Промский А.В. Формальная семантика указателей языка C-light // Материалы конф. молодых ученых, посвященной 10-летию Института вычислительных технологий СО РАН. Новосибирск, 2001. - Т. 1. - С. 62-65.

37. Промский А.В. Автоматическая генерация условий корректности в системе верификации программ // Тез. докл. междунар. конф. молодых ученых по математическому моделированию и информатике. — Новосибирск, 2002. — С. 67.

38. Промский А.В. Генерация и метагенерация условий корректности в системе СПЕКТР-2. Новосибирск, 2003. - 50 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; N 103).

39. Хэзфилд Р., Кирби JL, и др. Искуство программирования на С. Фундаментальные алгоритмы, структуры данных и примеры приложений. — К.: ДиаСофт, 2001. 736 с.

40. Andersen L.O. Program analysis and specialization for the С programming language. Thes. doct. phylosophy (computer sci.). — DIKU, Universisty of Copenhagen, 1994. — (DIKU report 94/19).

41. Apt K.R. Ten years of Hoare's logic: A survey — Part I // ACM Trans. Progr. Lang, and Systems. 1981. - Vol. 3, N. 4. - P. 431-483.

42. Apt K.R., Olderog E.R. Verification of sequential and concurrent programs. — Berlin etc.: Springer, 1991. — 450 p.

43. Arbib M.A., Alagic S. Proof rules for Gotos // Acta Informatica. 1979. - N 11, -P. 139-148.

44. Archer M., Lo A., Olsson R.A. Towards a transformational approach to program verification. // Software Testing, Verification & Reliability. — 1999. — Vol. 9, N 2, — P. 85-106.

45. Ball Т., Rajamani S.K.The SLAM project: debugging a system via static analysis // POPL 2002. URL: http://research.microsoft.com/slam.

46. Bensalem S., Lakhnech Y., Saidi H. Powerful techniques for the automatic generation of invariants. // Lect. Notes Comput. Sci. — Berlin etc., 1996. — Vol. 1102. — P. 323-335.

47. Bergstra J.A., Tucker J.V. Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. — Amsterdam, 1980. — (Rep. / Mathematisch Centrum; IW 136/80).

48. Bergstra J.A., Tucker J.V. Expressiveness and the completeness of Hoare's logic. — Amsterdam, 1980. — (Rep. / Mathematisch Centrum; IW 149/80).

49. Black P.E. Axiomatic semantics verification of a secure Web server: Thes. doct. phylosophy (computer sci.). — Brigham Young Universisty, 1998. — 255 p.

50. Black P.E., Windley Ph.J. Inference rules for programming languages with side effects in expressions // Lect. Notes Comput. Sci. — Berlin etc., 1996. — Vol. 1125. — P. 56-60.

51. Black P.E., Windley Ph.J. Formal verification of programs in the presence of side effects // Proc. 31st Annual Hawai'i Intern. Conf. on System Science. — IEEE Computer Science Press. 1998. - Vol. 3. - P. 327-334.

52. Blass A., Gurevich Y. Inadequacy of computable loop invariants. // ACM Trans. Computational Logic. — 2001. — Vol. 2, Issue 1. — P. 1-11.

53. Boekhold M., Karkowski I., Corporaal H., Cilio A. A programmable ANSI С code transformation engine. — Delft, 1998. — (Tech. Rep. / Delft University of Technology; N l-68340-44(1998)-08).

54. Bofinger M. Reasoning about С programs: Thes. doct. phylosophy (computer sci.). — University of Queensland, 1998.

55. Bornat R. Proving pointer programs in Hoare logic // Lect. Notes Comput. Sci. — Berlin etc, 2000. Vol. 1873. - P. 102-126.56. de Bruin A. Goto statements: semantics and deduction systems // Acta Informatica.- 1981. — N 15. — 385-424.

56. Calcagno C., Ishtiaq S., O'Hearn P.W. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic // Proc. ACM-SIGPLAN 2nd Intern. Conf. Principles and Practice of Declarative Programming. — ACM Press, 2000. — 32 p.

57. Cannon L.W., Elliott R.A., Kirchhoff L.W., Miller J.H., Milner J.M., Mitze R.W., Schan E.P., Whittington N.O., Spencer H., Keppel D., Brader M.

58. Recommended С style and coding standards. — 2000. URL: http: //sunland. gsf с.nasa. gov/inf o/cstyle. html.

59. Cattel T. Modelling and verificarion of sC++ applications // Lect. Notes Comput. Sci.- Berlin etc, 1998. Vol. 1384. - P. 232-248.

60. Chaki S., Clarke E., Groce A., Jha S., Veith H. Modular verification of software components in С // Proc. 25th Intern. Conf. Software Eng. — IEEE Computer Society, 2003. P. 385-395.

61. Chandra A.K., Manna Z. Program schemes with equality // Proc. 4th Ann. ACM Symp. on Theory Сотр. — Denver, 1972. — P. 52-64.

62. Clarke E. Completeness and incompleteness theorems for Hoare-like axiom systems: Thes. doct. phylosophy (computer sci.). — Cornell Univ., Computer Science Dep., 1976.

63. Clarke E. Programming language constructs for which it is impossible to obtain good Hoare axiom systems //J. Assoc. Computing Machinery. — 1979. — Vol. 26, N 1. — P. 129-147.

64. Clarke E., Kroening D. Hardware verification using ANSI-C programs as a reference // Proc. ASP-DAC 2003. IEEE Computer Society Press, 2003. - P. 308-311.

65. Clarke E., Kroening D., Yorav K. Behavioral consistency of С and Verilog programs using Bounded Model Checking. — Pittsburgh, 2003. — (Technical Rep. / Carnegie Mellon Univ., School of Computer Science; CMU-CS-03-126).

66. Clarke E., Kroening D., Sharygina N., Yorav K. Predicate Abstraction of ANSI-C Programs using SAT // Proc. Model Checking for Dependable Software-Intensive Systems Workshop, San-Francisco, USA, 2003.

67. URL: http: //www-2. cs. emu.edu/~svc/papers/.

68. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs // Lect. Notes Comput. Sci. Berlin etc, 2004. - Vol. 2988. - P. 158-176.

69. Clint M., Hoare C.A.R. Program proving: jumps and functions // Acta Informatica.- 1972. — N 1. P. 214-224.

70. Cook S.A. Soundness and completeness of an axiom system for program verification // SIAM J. Computing. 1978. - Vol. 7, N 1. - P. 70-90.

71. Cousot P. Methods and logics for proving programs // Handbook of Theoretical Computer Science, vol. В (Formal Models and Semantics), Ch. 15. — Elsevier, 1990.- P. 843-993.

72. Cousot P. Abstract interpretation based formal methods and future challenges // Lect. Notes Comput. Sci. Berlin etc, 2001. - Vol. 2000. — P. 138-156.

73. Dolado J.J., Harman M., Otero M.C. An empirical investigation of the influence of a type of side effects on program comprehension // IEEE Trans. Software Eng. — 2004.- Vol. 29, N. 7. P. 665-670.

74. DuVarney D.C., Purushothaman Iyer S. С Wolf — a toolset for extracting models from С programs // Proc. / IFIP WG 6.1 22nd Intern. Conf. Formal Techniques for Networked and Distributed Systems. — London, 2002. P. 260-275.

75. Elgaard J., Moller A., Schwartzbach M.I. Compile-time debugging of С programs working on trees // Lect. Notes Comput. Sci. Berlin etc., 2000. — Vol. 1782. — P. 119-134.

76. Floyd R. W. Assigning meanings to programs // Proc. AMS Symp. Applied Mathematics. — American Mathematical Society, Providence, R.I., 1967. — Vol. 19. — P. 19-31.

77. Fradet P., Gaugne R., Le Metayer D. Static detection of pointer errors: an axiomatisation and a checking algorithm // Lect. Notes Comput. Sci. — Berlin etc., 1996. Vol. 1058. - P. 125-140.

78. Fraer R. Tracing the origins of verification conditions. — Rocquencourt, 1996. — 17 p.- (Rapp. / INRIA; N 2840).

79. Gerhart S.L. An overview of AFFFIRM: a specification and verification system // Proc. IFIP Congress (Tokyo, Melbourne, 1980). Amsterdam, 1980. - P. 343-347.

80. Gribomont E.P. Simplification of Boolean verification conditions. — Liege, 1999. — 25 p. — (Prepr. / Institut Montefiore, Universite de Liege).

81. Gries D. The multiple assignment statement // IEEE Trans. Software Eng. — 1978. — Vol. SE-4, N 6. — P. 89-93.

82. Gries D., Levin G. Assignment and procedure call proof rules // ACM Trans. Progr. Lang, and Systems. 1980. - Vol. 2, N 4. - P. 564-579.

83. Guidelines for the Use of the С Language in Vehicle Based Software. The Motor Industry Software Reliability Association, 1998. URL: http://www.misra.org.uk.

84. Gurevich Y., Huggins J.К. The semantics of the С programming language // Lect. Notes Comput. Sci. Berlin etc., 1993. - Vol. 702. — P. 274-309.

85. Hailpern В., Santhanam P. Software debugging, testing, and verification // IBM Systems J. 2002. - Vol. 41, N 1. — P. 4-12.

86. Harman M., Hu L., Munro M., Zhang X. Side-effect removal transformation // Proc. IEEE Int'l Workshop Program Comprehension. — IEEE Computer Society Press, 2001. P. 310-319.

87. Harman M., Hu L., Munro M., Zhang X. Weakest precondition for general recursive programs formalized in Coq // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2410. P. 332-348.

88. Harman M., Hu L., Hierons R., Wegener J., Sthamer H., Baresel A., Roper

89. M. Testability transformation // IEEE Trans Software Eng. 2004. - N 30(1). — P. 3-16.

90. Haugh E.D. Testing С programs for buffer overflow vulnerabilities: Thes. master of science. — Univ. of California, Davis. 1999. — 82 p.

91. Heintze N., Tardieu O. Ultra-fast aliasing analysis using CLA: a million lines of С code in a second // Proc. ACM SIGPLAN 2001 conf. Programming language design and implementation. ACM Press, 2001. — P. 254-263.

92. Hoare C.A.R. An axiomatic basis for computer programming // Communs ACM. — 1969. Vol. 12, N 1. - P. 576-580.

93. Hoare C.A.R. Assertions / Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 August 11, 2002. - Amsterdam, 2003. - P. 291-316.

94. Hoare C.A.R., Jifeng H. A trace model for pointers and objects // Lect. Notes Comput. Sci. Berlin etc., 1999. - Vol. 1628. - P. 1-18.

95. Hoare C.A.R., Wirth N. An axiomatic definition of the programming language Pascal // Acta Informatica. 1973. - Vol. 2, N 4. - P. 335-355.

96. Hohmuth M., Tews H. The semantics of С++ data types: towards verifying low-level system components // Emerging Trends: Proc. / TPHOLs 2003. — P. 127-144.

97. URL: http: //wwwtcs. inf. tu-dresden. de/~tews/science.html. en.

98. Holzmann G.J. Logic verification of ANSI С code with SPIN // Lect. Notes Comput. Sci. Berlin etc., 2000. - Vol. 1885. - P. 131-147.

99. Homeier P.V., Martin D.F. Trustworthy tools for trustworthy programs: A verified verification condition generator // Lect. Notes Comput. Sci. — Berlin etc., 1994. — Vol. 859. P. 269-284.

100. Homeier P.V., Martin D.F. Mechanical verification of mutually recursive procedures // Lect. Notes Comput. Sci. Berlin etc., 1996. — Vol. 1104. — P. 201-215.

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

102. Huisman M., Jacobs B. Java program verification via Hoare logic with abrupt termination // Lect. Notes Comput. Sci. — Berlin etc, 2000. — Vol. 1783. — P. 284303.

103. Igarashi S., London R.L., Luckham D.C. Automatic program verification I: A logical basis and its implementation // Acta Informatica. — 1975. — Vol. 4. — P. 145-182.

104. ISO commitee JTC/SC22/WG14. Record of responses. URL: ftp: //ftp. dmk. com/DMK/sc22wgl4/RR/.

105. Jim Т., Morrisett G., Grossman D., Hicks M., Cheney J., Wang Y. Cyclone: a safe dialect of С //In USENIX Annual Technical conf., Monterey, CA, June 2002. URL: http://www.cs.cornell.edu/projects/cyclone.

106. Johnson S.C. Lint, а С program checker. 1977. - (Tech. Rep. AT&T Bell Laboratories; N CSTR-65). - updated version TM 78-1273-3.

107. Jones R.W.M., Kelly P.H.J. Backwards-compatible bounds checking for arrays and pointers in С programs // Automated and Algorithmic Debugging. — 1997. — P. 13-26. URL: http: //www-dse. doc. ic . ac. uk/~r j 3/.

108. Kleymann T. Hoare logic and VDM: machine-checked soundness and completeness proofs: Thes. doct. phylosophy (computer sci.). — Univ. of Edinburgh, 1998. — 260 p.

109. Kleymann T. Hoare logic and auxiliary variables // Formal Aspects of Computing. — 1999. Vol. 11. - P. 541-566.

110. Kowaltowski T. Axiomatic approach to side effects and general jumps // Acta Informatica. 1977. — N 7. — P. 357-360.

111. Kozen D., Tiuryn J. On the completeness of propositional Hoare logic // Information Sciences. — 2001. Vol. 139, N 3-4. - P. 187-195.

112. Kroening D.Application specific higher order logic theorem proving // Proc. Verification Workshop (VERIFY'02). 2002. - P. 5-15.

113. Lamport L., Paulson L.C. Should your Specification language be typed? // ACM Trans. Progr. Lang., and Systems. — 1999. — Vol. 8, N. 1. — P. 1-25.

114. Lifschitz V. On verification of programs with goto statements // Inform. Processing Letters. 1984. - N 18. - P. 221-225.

115. Lipton R.J. A necessary and sufficient condition for the existence of Hoare Logics //In Proc. 18th IEEE Symp. Foundations of Computer Sci. — 1977. P. 1-6.

116. London R.I. et al. Proof rules for the programming language EUCLID // Acta Informatica. 1978. - Vol. 10. - P. 1-26.

117. Luckham D.C., Suzuki N. Verification of array, record and pointer operations in Pascal // ACM Trans. Progr. Lang., and Systems. 1979. - Vol. 1, N 2. - P. 226-244.

118. Manna Z., Waldinger R. Problematic features of programming languages: A situational-calculus approach // Acta Informatica. — 1981. — Vol. 16, N 4. — P. 371-426.

119. McCarthy J. Towards a mathematical science of computation // Proc. IFIP Congress 62. Amsterdam, 1962. — P. 21-28.

120. Meyer B. Object-oriented software construction (2nd ed.). — Prentice Hall PTR, 1997.

121. Milner R. Equivalences on program schemes //J. Computer and System Sci. — 1970. Vol. 4, N. 3. - P. 205-219.

122. Milner R., Tofte M., Harper R.W. The definition of Standard ML. MIT Press, 1990.

123. Moore J. S. Proving theorems about Java and the JVM with ACL2 / Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 August 11, 2002. — Amsterdam, 2003. - P. 227-290.

124. Moriconi M., Schwartz R.L. Automatic construction of cerification condition generators from Hoare logics // Lect. Notes Comput. Sci. — Berlin etc., 1981. — Vol. 115. P. 363-377.

125. Muller-Olm M., Wolf A. On Excusable and inexcusable failures: Towards an adequate notion of translation correctness // Lect. Notes Comput. Sci. — Berlin etc, 1999. — Vol. 1709. P. 1107-1126.

126. Muller-Olm M., Seidl H. Computing polynomial program invariants// Inform. Processing Letters. 2004. - N 91(5). - P. 233-244.

127. Nepomniaschy V.A. On a symbolic method of verification for definite iteration over data structures / / Joint Bulletin of the Institute of Informatics Systems and Computer Center. 1998. - N 5. - P. 1-22.

128. Nepomniaschy V.A. Verification of pointer programs using symbolic method for definite iterations // Joint Bulletin of the Institute of Informatics Systems and Computer Center. 2000. - N 13. - P. 56-66.

129. Nepomniaschy V.A. Symbolic verification method for definite iterations over tuples of. data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. 2001. - N 15. - P. 103-123.

130. Nepomniaschy V.A., Sulimov A.A. Problem-Oriented Means of Program Specification and Verification in Project SPECTRUM // Lect. Notes Comput. Sci. — 1993. Vol. 722. - P. 374-378.

131. Nepomniaschy V.A., Sulimov A.A. Towards Automatic Program Verification: Problem-Oriented Knowledge Bases // Specification, verification and net models of concurrent systems. — Novosibirsk, 1994. — P. 138—150.

132. Nimmer J.W., Ernst M.D. Automatic generation of program specifications. Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications // Proc. international symposium on Software testing and analysis. — ACM Press, 2002. — P. 229-240.

133. Nipkow T. Hoare logics for recursive procedures and unbounded nondeterminism.2001. — (Draft / Fakultat fur Informatik, Technische Universitat Munchen). URL: http://www.in.turn.de/~nipkow/.

134. Norrish M. Derivation of verification rules for С from operational definitions // Supplementary Proc. 9th International Conf. Theorem Proving in Higher Order Logics.- TUCS General Publication N 1, Turku Centre for Computer Science, 1996. — P. 69-75.

135. Norrish M. С formalised in HOL: Thes. doct. phylosophy (computer sci.). — Cambridge,1998. 150 p.

136. Norrish M. Deterministic expressions in С // Lect. Notes Comput. Sci. — Berlin etc,1999. — Vol. 1576. P. 147-161.

137. O'Donnell M.J. A critique of the foundations of Hoare style programming logics // Communs ACM. 1982. - Vol. 25, N 12. - P. 927-935.

138. Oheimb D. von. Hoare logic for mutual recursion and local variables // Lect. Notes Comput. Sci. Berlin etc., 1999. - Vol. 1738. - P. 168-180.

139. Oheimb D. von. Hoare logic for Java in Isabelle/HOL // Concurrency and Computation: Practice and Experience, 13(13), 2001.

140. URL: http: //isabelle. in. turn. de/Bali/papers/CPEOl.html.

141. Oheimb D. von, Nipkow T. Hoare logic for NanoJava: auxiliary variables, side effects, and virtual methods revisited // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2391. P. 89-105.

142. Owre S., Rushby J., Shankar N. PVS: A prototype verification system // Lect. Notes Art. Intell. 1992. - Vol. 607. - P. 748-752.

143. Paraspyrou N.S. A formal semantics for the С programming language: Thes. doct. phylosophy (computer sci.). — National Technical University of Athens, 1998. — 269 p.

144. Paraspyrou N.S., Maco§ D. A study of evaluation order semantics in expressions with side effects // J. Functional Programming. — 2000. — N 10(3), — P. 227-244.

145. Paraspyrou N.S., Vescoukis V.C. Facilitating the definition of programming languages by using parametric context-free grammars // Advances in Informatics. — 2000. P. 260-272.

146. Plotkin G.D. A structure approach to operational semantics. — 1981. — (Tech. Rep./ DAIMI/Aarhus University; FN-19).

147. Plotkin G.D. The origins of structural operational semantics // Inform. Processing Letters. — 2003. Vol. 88, Issue 1-2. - P. 27-32.

148. Poetzsch-Heffer A., Mtiller P. A programming logic for sequential Java // Lect. Notes Comput. Sci. Berlin etc., 1999. - Vol. 1576. - P. 162-176.

149. Programming languages C: ISO/IEC 9899:1990. — 1990.

150. Programming languages C: ISO/IEC 9899:1999. - 1999. - 566 p.

151. Reynolds J.C. Theories of Programming Languages. — Cambridge University Press, 1998. 500 p.

152. Ritchie D.M. The developement of the С language //In 2nd History of Programming Languages conf., Cambridge, Mass., — ACM, 1993.

153. Scott D.S., Strachey C. Towards a mathematical semantics for programming languages. — Oxford, 1971. — (Tech. Rep. / Programmnig Research Group, University of Oxford; N PRG-6).

154. Sharma В., Dhodapkar S.D., Ramesh S. Assertion checking environment (ACE) for formal verification of С programs // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2434. P. 284-295.

155. Simon A., King A. Analysing string buffers in C. — Kent, 2002. — (Tech. Rep. / Computing Laboratory, Univ. of Kent; N 2-02).

156. Stoy J.E. Denotational semantics: the Scott-Strachey approach to programmnig language theory. — MIT Press, Cambridge, Mass., 1977.

157. Subramanian S., Cook J.V. Machanichal verification of С programs // In 1st workshop on Formal Methods in Software Practice (FMSP1996). — J. Assoc. Computing Machinery, 1996.

158. Suzuki N. Automatic verification of programs with complex data structure: Thes. doct. phylosophy (computer sci.). — Stanford Univ., 1976.

159. Suzuki N. Analysis of pointer Rotation // Communs ACM. — 1982. — Vol. 25, Issue 5. P. 330-335.

160. US National Institute of Standards and Technology. The Economic Impacts of Inadequate Infrastructure for Software Testing, May 2002.

161. Wand M. A new incompleteness result for Hoare's system //J. Assoc. Computing Machinery. 1978. - Vol. 25, N 1. - P. 168-175.

162. Wang C., Musser D.R. Dynamic verification of С++ generic algorithms // IEEE Trans. Software Eng. 1997. — Vol. 23, N 5. - P. 314-322.

163. Wilson R.P., Lam M.S. Efficient context-sensitive pointer analysis for С programs // ACM SIGPLAN Notices. 1995. - Vol. 30, N 6. - P. 1-12.

164. Zamulin A.V. Algebraic modelling of imperative languages with pointers // Lect. Notes Comput. Sci. Berlin etc., 1993. - Vol. 735. - P. 81-97.