Верификация C-программ на основе смешанной аксиоматической семантики

И. С. Ануреев; И. В. Марьясов; В. А. Непомнящий

doi:undefined

Верификация C-программ на основе смешанной аксиоматической семантики

И. С. Ануреев, И. В. Марьясов, В. А. Непомнящий

Полный текст:

Аннотация

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

Ключ. слова

верификация, операционная семантика, аксиоматическая семантика, язык C, язык C-light, язык C-kernel, частичная корректность,

УДК: 519.681.3

Об авторах

И. С. Ануреев

Институт систем информатики им. А. П. Ершова СО РАН
Россия

И. В. Марьясов

Институт систем информатики им. А. П. Ершова СО РАН
Россия

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

Институт систем информатики им. А. П. Ершова СО РАН
Россия

Список литературы

1. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. Ориенти¬рованный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формаль¬ные методы и модели информатики. С. 51 - 134.

2. Непомнящий В. А., Ануреев И. С., Промский А. В. На пути к верификации C-программ. Язык C-light и его трансформационная семантика // Problems in Programming. Kiev, 2006. № 2 - 3. С. 359 - 368.

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

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

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

6. Марьясов И. В. На пути к автоматической верификации C-light программ. Сме¬шанная аксиоматическая семантика языка C-kernel. Новосибирск, 2008. 32 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 150).

7. Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки. - Новосибирск, 2010. - 33 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 155).

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

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

10. Maryasov I. V. Towards automatic verification of C-light programs. Mixed axiomatic semantics of C-kernel language // Perspectives of Systems Informatics (PSI): A. Ershov 7th Int. Conf.: Int. workshop on Program Understanding. Novosibirsk, 2009. P. 44 - 52.

11. Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.

Дополнительные файлы

Для цитирования: Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики. Моделирование и анализ информационных систем. 2010;17(3):5-28.

For citation: Anureev I.S., Maryasov I.V., Nepomniaschy V.A. C-programs Verification on Basis of Mixed Axiomatic Semantics. Modeling and Analysis of Information Systems. 2010;17(3):5-28. (In Russ.)

Обратные ссылки

Обратные ссылки не определены.

Контент доступен под лицензией Creative Commons Attribution 4.0 License.

ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)

Логин
Пароль