maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1036Research ArticleОригинальные статьиArticlesВерификация C-программ на основе смешанной аксиоматической семантикиC-programs Verification on Basis of Mixed Axiomatic SemanticsАнуреевИ. С.AnureevI. S.anureev@iis.nsk.suМарьясовИ. В.MaryasovI. V.ivm1999@mail.ruНепомнящийВ. А.NepomniaschyV. A.vnep@iis.nsk.suИнститут систем информатики им. А. П. Ершова СО РАНRussian Federation201020092010173528Copyright © Ануреев И.С., Марьясов И.В., Непомнящий В.А., 20102010Ануреев И.С., Марьясов И.В., Непомнящий В.А.Anureev I.S., Maryasov I.V., Nepomniaschy V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1036

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

верификацияоперационная семантикааксиоматическая семантикаязык Cязык C-lightязык C-kernelчастичная корректностьprogram verificationoperational semanticsaxiomatic semanticsC languageC-light languageC-kernel languagepartial correxctnessReferencesНепомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. Ориенти¬рованный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формаль¬ные методы и модели информатики. С. 51 - 134.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. Ориенти¬рованный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формаль¬ные методы и модели информатики. С. 51 - 134.Непомнящий В. А., Ануреев И. С., Промский А. В. На пути к верификации C-программ. Язык C-light и его трансформационная семантика // Problems in Programming. Kiev, 2006. № 2 - 3. С. 359 - 368.Непомнящий В. А., Ануреев И. С., Промский А. В. На пути к верификации C-программ. Язык C-light и его трансформационная семантика // Problems in Programming. Kiev, 2006. № 2 - 3. С. 359 - 368.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пу¬ти к верификации C программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 19 - 30.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пу¬ти к верификации C программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 19 - 30.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации C программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 5 - 15.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации C программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 5 - 15.Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 1. Язык C-light. Новосибирск, 2001. 48 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 84).Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 1. Язык C-light. Новосибирск, 2001. 48 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 84).Марьясов И. В. На пути к автоматической верификации C-light программ. Сме¬шанная аксиоматическая семантика языка C-kernel. Новосибирск, 2008. 32 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 150).Марьясов И. В. На пути к автоматической верификации C-light программ. Сме¬шанная аксиоматическая семантика языка C-kernel. Новосибирск, 2008. 32 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 150).Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки. - Новосибирск, 2010. - 33 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 155).Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки. - Новосибирск, 2010. - 33 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 155).Непомнящий В. А., Рякин, О. М. Прикладные методы верификации программ. М.: Радио и связь, 1988.Непомнящий В. А., Рякин, О. М. Прикладные методы верификации программ. М.: Радио и связь, 1988.Programming languages - C: ISO/IEC 9899:1999. 1999. 566 p.Programming languages - C: ISO/IEC 9899:1999. 1999. 566 p.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.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.Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.

The authors declare that there are no conflicts of interest present.