8 / 16
И.В. Рудаков, Р.Е. Гурин
56
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
4 1
2
3
;
2;
5;
4
s pc m v
v
v
— соотношение принадлежит множе-
ству состояний, которое удовлетворяет предикату
.
P
В свою очередь, состояние
4 1
2
3
;
5;
2;
4
s pc m v
v
v
не принадлежит этому множеству.
Рассмотрим оператор присваивания
1 1 2
v v v
(метка состояния про-
граммы
4
).
m
Новое значение переменной
1
v
, которое мы обозначим как
,
v
будет равно
1 2
v v
при любых начальных значениях. Следовательно, можно за-
писать предикат, который описывает все переходы, определяемые оператором,
1 1 2
v v v
с меткой
4
,
m
если после него идет оператор с меткой
5
,
m
то преди-
кат имеет следующий вид:
4
5
1 1 2
2 3
(
) (
) (
)
({ , }).
pc m pc m v v v same v v
Предикат, приведенный ранее, описывает множество переходов програм-
мы при произвольных начальных значениях переменных
1 2 3
,
. ,
v v v
Формула
( )
same V
определяется следующим образом:
( ) & (
).
v V
same V
v v
Из приведенного ранее следует, что предикатом можно задать не только
множество состояний, но и множество переходов любой программы.
Если множество
i
D
конечно, то каждый предикат может быть представлен
булевой функцией.
Операторы программы изменяют ее состояния [13];
( , )
s s
— упорядочен-
ная пара состояний в структуре Крипке. Нештрихованные переменные задают
состояния, из которых направлен переход, штрихованные переменные задают
состояние, в которые направлен переход. Поэтому программу можно задать
предикатами, каждый из которых соответствует своему оператору.
Лексический транслятор осуществляет преобразование внутреннего пред-
ставления программного кода на языке Си в формулы логики первого порядка
(рис. 5).
Рис. 5.
Алгоритм преобразования программы в формулу логики первого порядка
Для этого лексический транслятор строит следующие формулы:
0
( ,
)
S V PC
—
для множества начальных состояний;
( ,
, ,
)
V PC V PC
R R
— для всех возможных переходов в программе.
Рассмотрим подробнее алгоритм преобразования кода в формулы логики
первого порядка.
Предположим, что программа состоит из операторов, каждый имеет один
вход и один выход:
1 2
1
2
::
;
P func v E P P if bthenP else P whilebdoP