Содержание к диссертации
Введение 4
1 Предварительные понятия 10
Формальная верификация программ 10
Используемые виды семантик 12
Денотационная семантика 12
Структурная операционная семантика 13
Аксиоматическая семантика 15
Пример верификации 16
Вопросы полноты и непротиворечивости 18
1.3 Язык С 21
История языка 22
Особенности языка 22
Проблемы верификации языка С 23
1.4 Обзор известных работ и систем 26
2 Язык C-light и его операционная семантика 30
2.1 Язык C-light 30
Типы 30
Декларации 32
Выражения 33
Операторы 35
Программы 35
Язык утверждений 37
Абстрактная машина языка C-light 39
Состояния абстрактной машины языка C-light 39
Конфигурации абстрактной машины языка C-light 42
Система типов 47
2.4 Динамическая операционная семантика 50
Семантика выражений 51
Семантика деклараций 57
Семантика операторов 60
Семантика частичной корректности 66
3 Язык C-kernel и его аксиоматическая семантика 68
Обзор языка C-kernel 68
Связь аксиоматической семантики с операционной 70
Интерпретация выражений 70
Значение логических утверждений 71
Лемма о подстановке 72
Система HSC 73
Непротиворечивость системы HSC 82
4 Перевод из языка C-light в язык C-kernel 89
4.1 Переписывание деклараций 89
Уточнение класса памяти 89
Разбиение списка деклараторов 90
4.2 Переписывание операторов 90
Нормализация операторов 90
Элиминация операторов 91
4.3 Переписывание выражений 93
Правила элиминации 93
Правила декомпозиции 95
Правила нормализации 95
Некоторые свойства системы правил 96
Корректность перевода: предварительные понятия 97
Теорема о корректности перевода 100
5 Генерация и метагенерация условий корректности 119
5.1 Автоматизация вывода условий корректности 119
Модификация аксиоматической семантики 119
Автоматизированные системы верификации 121
5.2 Генерация УК в системе СПЕКТР 122
Входной язык генератора УК 122
Нормальная форма правил 125
Схема генератора УК 128
5.3 Метагенерация условий корректности 130
Общая форма правил 131
Алгоритм перевода из общей формы в нормальную 133
Заключение 136
Литература 138
А Пример верификации в системе HSC 150
В Эксперименты в системе СПЕКТР
Введение к работе
В диссертации развит аппарат формализации семантик языков 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 программ методом Хоара.
Методы исследования
В работе использовались аппараты и методы математической логики, теории спецификации программ, структурного операционного подхода Плоткина, аксиоматического подхода Хоара и эквивалентных преобразований программ.
Научные результаты, вынесенные на защиту
В диссертационной работе получены новые научные результаты:
Структурная операционная семантика языка C-light поддерживает представительное подмножество С99, обладает свойством детерминированности вычисления выражений и независимости от конкретной архитектуры, что позволяет придавать смысл более широкому классу программ.
Система правил перевода из языка C-light в язык C-kernel обладает свойством корректности. Для доказательства этого свойства вместо обычных понятий функциональной или логико-термальной эквивалентности предложено новое понятие семантического расширения.
Непротиворечивая аксиоматическая семантика языка C-kernel с новой моделью языка утверждений. Расширение языка утверждений новыми типами высоких порядков позволило формально представлять указатели и области определенности идентификаторов. Благодаря двухуровневой схеме эта семантика фактически применяется для верификации C-light программ.
Новый метод метагенерации условий корректности, ориентирован на модифицированную семантику Хоара и позволяет упростить порождаемые условия корректности.
Научная и практическая ценность
Полученные результаты являются основой для разработки методов формализации и верификации программ написанных на современных языках системного программирования.
Предложенные принципы и средства в большой степени независимы от конкретной среды и могут быть адаптированы и расширены для различных реализаций языка С, а также стать базой для исследования языков прямо или косвенно происходящих из языка С: C++, С#, Java.
Введение
Созданный прототип метагенератора условий корректности используется для экспериментов в системе СПЕКТР-2, которая не зависит от входного языка и может служить основой для разработки промышленной версии системы. Метагенерация позволила расширить систему правилами элиминации инвариантов циклов в программах линейной алгебры. Система правил переписывания была использована П. Караваевым в его входном анализаторе для системы СПЕКТР-2. Также эта система стала основой для системы переписываний в языке С#, разработчиком которой является И. В. Дубрановский.
Доклады и печатные публикации
Основные положения работы докладывались на четвертом сибирском конгрессе по прикладной и индустриальной математике «ИНПРИМ-2000» (Новосибирск, 2000 г.), на конференции молодых ученых, посвященной 10-летию ИВТ СО РАН (Новосибирск, 2001 г.), на конференции, посвященной 90-летию со дня рождения А. А. Ляпунова (Новосибирск, 2001 г.), на международной конференции молодых ученых по математическому моделированию и информационным технологиям (Новосибирск, 2002 г.), а также на международной конференции "Perspectives of System Informatics" (Новосибирск, 2003 г.).
Кроме того, полученные результаты обсуждались на совместных семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры программирования НГУ. Материалы диссертации вошли в отчеты по проектам РФФИ 00-01-00909 (1999-2001) и 04-01-00114.
По материалам диссертации опубликовано 11 работ [24-29,35-38,127].
Структура и объем диссертации
Диссертация состоит из введения, пяти глав, заключения и приложений. Объем работы (за исключением приложений и библиографии) составляет 130 страниц в формате машинописного текста. Список литературы содержит 166 наименований.
Краткое содержание работы
В главе 1 приводятся базовые понятия, используемые в работе, и краткий исторический обзор. Разд. 1.1 представляет современный взгляд на формальную верификацию программ. В разд. 1.2 рассмотрены используемые виды семантик: денотационная (п. 1.2.1), операционная (п. 1.2.2), аксиоматическая (п. 1.2.3); рассмотрен пример верификации программы в логике Хоара (п. 1.2.4); напоминаются проблемы непротиворечивости и полноты (п. 1.2.5). Разд. 1.3 истории языка С, его особенностям и проблемам его верификации. В разд. 1.4 дается краткий обзор известных работ по формализации и верификации С, а также некоторых систем.
