OPERATIONAL SEMANTICS FOR LYaPAS.pdf Язык программирования ЛЯПАС разработан в 1960-х годах в Томском государственном университете, использовался в СССР и других странах, в настоящее время возрождается на кафедре защиты информации и криптографии ТГУ с целью разработки доверенного программного обеспечения [1]. В данной работе сообщается об операционной семантике ЛЯПАСа, которая может применяться как минимум для двух целей: для доказательства формальных свойств программ на ЛЯПАСе и для создания верифицирующего транслятора. Семантика языка программирования - формализация значений конструкций языка построением их математических моделей. Существует несколько вариантов семан-тик, самые распространённые - операционные и денотационные семантики. Денотационные семантики основаны на абстракции функций и ориентированы на функциональные языки. Операционные семантики основаны на определении состояний абстрактной машины и переходов между ними. Семантические правила представляют собой переход из одного состояния в другое при соблюдении условий. Для ЛЯПАСа и метода абстрактной интерпретации наиболее подходящий вариантом является операционная семантика. Под программой понимается синтаксически правильная последовательность команд, представленная нумерованным списком. Состоянием программы на ЛЯПАСе является шестёрка объектов (c, var, т, EL, Q, S), где c - номер текущей команды; var - массив значений переменных; т - значение внутренней переменной; EL - массив списков элементов комплексов; Q и S - массивы мощностей и ёмкостей комплексов соответственно. Операции в ЛЯПАСе можно разделить на четыре группы: операции присваивания, логические и арифметические операции, операции перехода, операции над комплексами. Формулы (1) представляют примеры правил для операций из каждой группы. Это операции занесения значения в переменную, дизъюнкции, перехода по нулю и добавления элемента в комплекс: p[c] а (c, var, т, EL, Q, S) -> (с + 1, var [а/т], т, EL, Q, S)' p[c] = Vy, ri = т V y (с, var, т, EL, Q, S) -^ (с + 1, var, y, EL, Q, S)' , . _p[c] = 0 ^ 8, т = 0_( ) (c, var, т, EL, Q, S) -> (8, var, т, EL, Q, S)' _p[c] = @>^,qw < s (ф),е ^ q(0)_ (c, var, т, EL, Q, S) -► (c + 1, var, т, EL[0/EL(0):insert(£, т)], Q[0/Q(0) + 1],S). В используемом на данный момент компиляторе имеется недостаток при работе с комплексами: каждый раз при обращении к элементу производится проверка, не выходит ли индекс за границы комплекса. Это значительно замедляет работу программ, но убирать проверку можно только в тех местах, где есть полная уверенность, что выход за границы комплекса не произойдёт. Для того чтобы получить возможность не тратить время на проверку там, где в этом нет необходимости, нужен способ автоматического доказательства корректности обращения к элементам комплекса. Для построения такого способа может быть применён метод абстрактной интерпретации [2]. Суть метода заключается в том, что семантическим правилам в конкретном домене ставятся в соответствие правила некоторого абстрактного домена, который по структуре проще конкретного. Домены и соответствие между ними должны удовлетворять некоторым правилам. Доказательство производится в абстрактном домене, а затем результат интерпретируется в конкретном. Опираясь на семантические правила, можно не только доказать отдельные утверждения о программах, но и создать верифицирующий транслятор, что важно для написания доверенного программного обеспечения. Для языка С существует верифицирующий транслятор CompCert [3], основанный на применении средства доказательства теорем Coq [4]. Аналогичный транслятор может быть создан в будущем для ЛЯПАСа. В дальнейшем для реализации поставленных целей следует представить семантические правила в Coq. Для доказательства корректности обращения к элементам комплекса необходимо задать абстрактный домен и соответствие между семантическими правилами и правилами в абстрактном домене. Для создания верифицирующего транслятора следует задать в Coq семантику машинного языка и построить доказательства корректности переходов, используемых транслятором.

Скачать электронную версию публикации