|
Моделирование и анализ информационных систем, 2010, том 17, номер 3, страницы 5–28
(Mi mais20)
|
|
|
|
Эта публикация цитируется в 5 научных статьях (всего в 5 статьях)
Верификация C-программ на основе смешанной аксиоматической семантики
И. С. Ануреев, И. В. Марьясов, В. А. Непомнящий Институт систем информатики им. А. П. Ершова
СО РАН
Аннотация:
Описывается смешанная аксиоматическая семантика языка C-kernel, являющегося ядром представительного подмножества языка C, названного C-light. Такая семантика позволяет во многих случаях упростить условия корректности верифицируемых программ. Данная семантика является основой разрабатываемого генератора условий корректности C-kernel-программ. Рассмотрен пример, иллюстрирующий применение правил вывода описанной семантики.
Ключевые слова:
верификация, операционная семантика, аксиоматическая семантика, язык C, язык C-light, язык C-kernel, частичная корректность.
Поступила в редакцию: 25.05.2010
Образец цитирования:
И. С. Ануреев, И. В. Марьясов, В. А. Непомнящий, “Верификация C-программ на основе смешанной аксиоматической семантики”, Модел. и анализ информ. систем, 17:3 (2010), 5–28
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais20 https://www.mathnet.ru/rus/mais/v17/i3/p5
|
Статистика просмотров: |
Страница аннотации: | 475 | PDF полного текста: | 150 | Список литературы: | 54 |
|