ISSN 1818-1015
Министерство образования и науки Российской Федерации
Ярославский государственный университет им. П.Г. Демидова
МОДЕЛИРОВАНИЕ И АНАЛИЗ
ИНФОРМАЦИОННЫХ СИСТЕМ
Том 17 № 3 2010
Основан в 1999 г.
Выходит 4 раза в год
Свидетельство о регистрации №019209 от 16.08.99
Государственного Комитета Российской Федерации по печати
Главный редактор
В.А. Соколов
Редакционная коллегия
С.М. Абрамов, О.Л. Бандман, В.А. Бондаренко, И.Б. Вирбицкайте,
С.Д. Глызин (зам. гл. ред.), М.Г. Дмитриев, В.Л. Дольников, В.Г. Дурнев,
А.В. Зафиевский, Л.С. Казарин, Ю.Г. Карпов, С.А. Кащенко, А.Ю. Колесов,
И.А. Ломазова, В.Э. Малышкин, В.А. Непомнящий, П.Г. Парфенов, Р.Л. Смелянский
Ответственный секретарь Е.А. Тимофеев
Адрес редакции: 150000, Ярославль, ул. Советская, 14
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
Научные статьи в журнал принимаются по электронной почте и на кафедре
теоретической информатики Ярославского государственного университета. Статьи
должны содержать УДК, аннотации на русском и английском языках и сопровождаться
набором текста в редакторе LaTEX. Плата с аспирантов за публикацию
рукописей не взимается.
Ярославский государственный
университет им. П.Г. Демидова, 2010
c
Стр.1
СОДЕРЖАНИЕ
Моделирование и анализ информационных систем. Т. 17, №3. 2010
Верификация C-программ на основе смешанной аксиоматической семантики
Ануреев И. С., Марьясов И. В., Непомнящий В. А.
Составные редукции моделей Крипке и автоморфизмы
Белов Ю.А.
Локальная динамика уравнения с большим запаздыванием
в окрестности автомодельного цикла
Глазков Д.В., Кащенко С.А.
Вариационные неравенства и принцип виртуальных перемещений
Демьянков Н.А.
Рекуррентные последовательности над почтикольцами
Сбоев А.В.
Разрешимость теории Th(ω, 0, 1, <,+, f0, . . . , fn)
Снятков А.С.
Гиперплоскости универсальной экстремали некоторых задач оптимизации
Федотова Н.П.
Математические модели экономических систем
с учетом необратимости протекающих в них процессов
Цирлин А.М.
Фактор запаздывания и десинхронизация колебаний
связанных осцилляторов ФитцХью–Нагумо
Глызин С. Д., Солдатова Е. А.
Язык объектных запросов динамической информационной модели DIM
Рублев В.С.
Правила для авторов
5
29
38
48
58
72
91
107
134
144
162
Редактор, корректор А.А. Аладьева. Редактор перевода Э.И. Соколова.
Подписано в печать 15.10. 2010. Формат 60х841/8. Усл. печ. л. 19,67. Уч.-изд. л. 15,5. Тираж 500 экз.
Отпечатано на ризографе. Ярославский государственный университет им. П. Г. Демидова,
150 000, Ярославль, ул. Советская, 14. Телефон редакции (4852) 79-77-51.
Стр.2
ISSN 1818-1015
Ministry of Education and Science of the Russian Federation
Yaroslavl Demidov State University
MODELING AND ANALYSIS
OF INFORMATION SYSTEMS
Volume 17 No 3 2010
Founded in 1999
4 issues per year
State Registration License No 019209 of 16.08.1999
Editor-in-Chief
V. A. Sokolov
Editorial Board
S.M. Abramov, O.L. Bandman, V.A. Bondarenko, I.B. Virbitskayte,
S.D. Glyzin (Deputy Editor-in-Chief ), M.G. Dmitriev, V.L. Dol’nikov,
V.G. Durnev, A.V. Zafievsky, L.S. Kazarin, Yu.G. Karpov,
S.A. Kashchenko, A.Yu. Kolesov, I.A. Lomazova,
V.E. Malyshkin, V.A. Nepomniaschy, P.G. Parfionov, R.L. Smeliansky
Responsible Secretary E. A. Timofeev
Editorial Office Address: Sovetskaya str., 14, Yaroslavl, 150000, Russia
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
Yaroslavl Demidov State University, 2010
c
Стр.3
Contents
Modeling and Analysis of Information Systems. Vol. 17, No 3. 2010
C-programs Verification on Basis
of Mixed Axiomatic Semantics
Anureev I. S., Maryasov I. V., Nepomniaschy V. A.
Composite reductions for Kripke models
Belov. Y.A.
Local dynamics of DDE with large delay in the vicinity
of the self-similar cycle
Glazkov D.V., Kaschenko S.A.
Variational inequalities and the principle of virtual displacements
Demyankov N.A.
Recurrence sequences over near-rings
Sboev A.V.
On Decidability of the Theory Th(ω, 0, 1, <,+, f0, . . . , fn)
Snyatkov A.S.
Universal extremum of hyperplanes in some optimization problems
Fedotova N.P.
Mathematical models of economic systems with account
of the irreversibility of processes proceeding in them
Tsirlin A.M.
The factor of delay in a system of coupled oscillators FitzHugh – Nagumo
Glyzin S. D., Soldatova E. A.
The Object Query Language of the Dynamic Information Model DIM
Roublev V.S.
5
29
38
48
58
72
91
107
134
144
Стр.4
Модел. и анализ информ. систем. Т.17, №3 (2010) 5–28
УДК 519.681.3
Верификация C-программ на основе
смешанной аксиоматической семантики
Ануреев И. С., Марьясов И. В., Непомнящий В. А.
Институт систем информатики им. А. П. Ершова СО РАН
Новосибирский государственный университет
e-mail: anureev@iis.nsk.su, ivm1999@mail.ru, vnep@iis.nsk.su
получена 25 мая 2010
Ключевые слова: верификация, операционная семантика, аксиоматическая
семантика, язык C, язык C-light, язык C-kernel, частичная корректность
Описывается смешанная аксиоматическая семантика языка C-kernel, являющегося
ядром представительного подмножества языка C, названного C-light.
Такая семантика позволяет во многих случаях упростить условия корректности
верифицируемых программ. Данная семантика является основой разрабатываемого
генератора условий корректности C-kernel-программ. Рассмотрен
пример, иллюстрирующий применение правил вывода описанной семантики.
1. Введение
Формальная верификация программ — актуальное направление современного программирования.
Особый интерес представляет верификация программ, написанных
на распространённых языках системного программирования, таких как C и C++.
Обозримая формальная семантика является необходимой предпосылкой того, что
язык удобен для верификации.
Формальной детерминированной семантики для полного языка C, соответствующего
стандарту ISO C [9], не существует. В лаборатории теоретического программирования
ИСИ СО РАН был разработан язык C-light, являющийся представительным
подмножеством языка C. Формально этот язык был определён с помощью
структурной операционной семантики в стиле Плоткина. Хотя операционная
семантика удобна для формального определения языка, для верификации она имеет
слишком низкий уровень, что приводит к громоздким доказательствам условий
корректности. Поэтому обычно используют аксиоматическую семантику, базирующуюся
на логике Хоара [8], которая определяется как система вывода утверждений
о свойствах программ. Однако аксиоматическая семантика для языка C-light также
была бы громоздкой. В связи с этим был применён двухуровневый подход: в языке
5
Стр.5