Формальная семантика C-LIGHT программ и их верификация методом Хоара

• Автор: Промский, Алексей Владимирович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Новосибирск
• Количество страниц: 157 с.

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 Язык С-ИдЫ; и его операционная семантика
2.1 Язык С-^Ы;
2.1.1 Типы
2.1.2 Декларации
2.1.3 Выражения
2.1.4 Операторы
2.1.5 Программы
2.2 Язык утверждений
2.3 Абстрактная машина языка С-%М
2.3.1 Состояния абстрактной машины языка С-^М
2.3.2 Конфигурации абстрактной машины языка СЯщМ
2.3.3 Система типов
2.4 Динамическая операционная семантика
2.4.1 Семантика выражений
2.4.2 Семантика деклараций
ЩЬ, 2.4.3 Семантика операторов
2.4.4 Семантика частичной корректности

3 Язык С-кегпеї и его аксиоматическая семантика
3.1 Обзор языка С-кегпе1
3.2 Связь аксиоматической семантики с операционной
3.2.1 Интерпретация выражений
3.2.2 Значение логических утверждений
3.2.3 Лемма о подстановке
3.3 Система НЭС
3.4 Непротиворечивость системы НЭС
4 Перевод из языка С-^М в язык С-кегпе1
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, исследован вопрос корректности преобразований С-программ и их влияния на верификацию, разработаны логические средства для верификации С-light, программ методом Хоара
Актуальность темы
Тысячекратный рост производительности компьютеров за последние 25 лет привел к росту размеров программ в тех же пропорциях. Область применения огромных программ (от 1 до 40 млн. строк) значительно увеличилась за последнее десятилетие. Для таких больших программ является необходимым требование разработки по разумной цене и дальнейшей модификации и поддержки в течении всего их жизненного цикла (часто более 20 лет). Размеры и эффективность программ и коллективов, занимающихся их проектированием и сопровождением, не могут расти в одинаковых пропорциях. При достаточно устоявшейся (и зачастую оптимистичной) оценке в одну ошибку на тысячу строк кода такие программы быстро могут стать неуправляемыми. Поэтому в ближайшие 10 лет проблема надежности программного обеспечения может стать одним из основных вызовов для современных компьютерно-зависимых обществ.
До сих пор основным средством установления надежности программ в компьютерной индустрии остается тестирование [17,84]. Оно же является и самым требовательным по времени и затратам. В качестве подтверждения можно перечислить следующие факты [91]: половина всех инженеров компании Microsoft занимаются тестированием; половина своего времени разработчики тратят на тестирование; промежуток времени между фазами ‘Code Complete’ и ‘Release to Manufacture’ составляет 6 и более месяцев. В отчете 2002 года по использованию компьютеров в США [157J отмечалось, что потери от неадекватного тестирования программ составили 60 млрд. $, причем две трети этой суммы — это потери пользователей и одна треть — разработчиков.
В связи с этим рынок уже оказывает давление на разработчиков, требуя снижения этих издержек1 и, что особенно важно, возобновления интереса к чисто академическим исследованиям в области надежности программного обеспечения. Среди этих исследований важное место занимают методы формальной верификации программ.
Первым шагом на пути к верификации программ является формализация семантики
1 Здесь показателен пример, когда вся команда разработчиков Microsoft Windows (более 8000 инженеров) весь февраль 2002 г. занималась не своей непосредственной работой, а вопросами безопасности [91]. Такие перерывы в работе дороги, но еще дороже обходится «деятельность» последних сетевых вирусов.
Глава 2. Язык С-ИдЫ и его операционная семантика

Для корректной обработки вызовов функций и присваиваний необходимо ввести отношение, приводимости по умолчанию. В противном случае в правилах для операции присваивания и вызова функции пришлось бы явно записывать требования точного согласования типов аргументов. Это отношение, обозначаемое как 1С, будет отношением эквивалентности [133].
, Д и Т-2 — арифметические типы
Ь Ю^оЫ*. Т*) ЩтЖ)-
Тогда правило для вызова функции выглядит как
е : Тг х ... х Тп -> Т Уг.1 < г < п => ЗТ'.(е{ : Г Л 1С{ТиТ')) е(е1 еп) : Т
Заметим, что определение отношения 1С для арифметических типов неявно включает в
себя понятие приведения аргументов по умолчанию, поэтому правило для вызовов работает независимо от наличия или отсутствия прототипа для данного функционального типа.
Что касается операций языка С-^М, то правила для них могут быть достаточно громоздкими, потому что над аргументами происходят стандартные преобразования типов. Поэтому информация об окончательном типе выражения определяется специальными предикатами вида Р0р, где ор - символ операции. Они определяются в соответствии со стандартом, поэтому их реализация не представляет здесь особого интереса. Для обозначения унарных операций используем символ □, для бинарных операций — символ ©. Заметим, что операции постфиксного инкремента/декремента рассмотрены отдельно.
е : Т бх : Т е2:Т2 Рф(Т, Дц Т)
□ е : Т 61 ©е2 : Т
е0 : Г0 — скалярный е : Т е2 : Т2 Р?(2,Т2,Т) е0?е!:е2 : Т
В операциях присваивания необходимо, чтобы выражение в правой части было модифицируемым 1-значением. Правила для простого и составного присваиваний выглядят как
е : 1и(Т) е2 : Т0 1С(Т0, Т) Т — не массив
бх = е2 : Т
е-.1и(Т) е1©е2:Г0 1С(Т0,Т) Т — не массив
б1©= е2 : Т
Операции постфиксных инкремента и декремента определяются одинаково. Заметим, что префиксный инкремент и декремент можно обрабатывать с помощью правила для составного присваивания, так как выражения ++1 и --1 есть эквивалентные записи для 1+=1 и 1-=1.
е : 1ь'(Т) Т — скалярный тип е++ ; Т
2.4 Динамическая операционная семантика
Как следует из названия, данная часть семантики относится к моделированию реального исполнения С-1іаЬ+, программы в абстрактной машине. Динамическая семантика разбита