Формальная семантика C-LIGHT программ и их верификация методом Хоара тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Промский, Алексей Владимирович

• Промский, Алексей Владимирович
• кандидат физико-математических наук
• 2004

Оглавление диссертации кандидат физико-математических наук Промский, Алексей Владимирович

Введение

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-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.

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

Список литературы диссертационного исследования кандидат физико-математических наук Промский, Алексей Владимирович, 2004 год

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.