Верификация C-программ на основе смешанной аксиоматической семантики
Аннотация
Описывается смешанная аксиоматическая семантика языка C-kernel, являющегося ядром представительного подмножества языка C, названного C-light. Такая семантика позволяет во многих случаях упростить условия корректности верифицируемых программ. Данная семантика является основой разрабатываемого генератора условий корректности C-kernel-программ. Рассмотрен пример, иллюстрирующий применение правил вывода описанной семантики.
Ключевые слова
верификация,
операционная семантика,
аксиоматическая семантика,
язык C,
язык C-light,
язык C-kernel,
частичная корректность
MSC2020: 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.)
Просмотров: 320
Послать статью по эл. почте 