Шелехов Владимир Иванович, к.т.н., зав. лаб. системного программирования, Институт систем информатики имени А. П. Ершова СО РАН; доцент кафедры программирования НГУ
630090, Новосибирск, просп. Ак. Лаврентьева, 6, тел. (383) 330-27-21
Компилятор со средствами дедуктивной верификации подлежит тщательной сертификации для подтверждения высокого уровня доверия к результатам дедуктивной верификации. Разработка компилятора предикатных программ на базе его модели в соответствии с модельно-ориентированной технологией повышает уровень доверия к компилятору. Главной частью модели компилятора является модель внутреннего представления программы, реализуемая в рамках третьего релиза компилятора предикатных программ. В настоящей работе описывается архитектура модели внутреннего представления программы. Важнейшим аспектом модели является анализ типов. В описании модели используется специально разработанный язык спецификации структур данных компилятора. Верификация модели и разработка программы компилятора на базе модели обеспечат высокую надежность компилятора.
A compiler with deductive verification facilities should be thoroughly certified to obtain high level of assurance. The development of the compiler for a predicate program using a compiler model in accordance with a model-based design method makes the compiler to be of a higher level of assurance. The main part of a compiler model is the model of inner program representation for a predicate program. The model is designed in the framework of third release of the compiler. The model architecture for inner representation of predicate program is described. Type checking is specially analyzed as an important aspect in the compiler development. The verification of the model and compiler development on the base of the model should guarantee a high level of compiler reliability.
The authors declare that there are no conflicts of interest present.