10 / 16
И.В. Рудаков, Р.Е. Гурин
58
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
Предикат, который определяет все возможные переходы для всей програм-
мы, строится как дизъюнкция предикатов переходов для всех операторов про-
граммы [14]:
1
2
.
n
Programm
R
R R R
Стоит отметить, что проводится анализ путей выполнения программы.
Это наиболее предпочтительно, так как анализ условий программы ведет к ком-
бинаторному взрыву.
Пример.
Рассмотрим простую программу и построим для нее сумму преди-
катов переходов программы.
i
nt main()
{
int k = 3;
int n = 1024;
for(inti = 1; i< n; i++)
{
if(i> 4) k = k + 1;
else
k = k*2;
printf("k > i: %i>%i\n", k,i);
}
return 0;
}
Осуществим разметку программы и трансляцию ее в идентичный
текст (табл. 3).
Таблица 3
Разметка и трансляция программы
Оператор программы
Помеченный оператор программы
3
k
:
3
m k
1024
n
: 1024
m n
( 1;
;
)
for int i
i n i
1
: ( 1;
; :
)
m for int i
i n m i
4
1
2
if i
then k k elsek k
1
2
: 4
:
1
:
2
m if i
then m k k else m k k
Далее построим предикат для переходов программы:
1
:
3 :
m k m
1
1
,
3,
3
;
m k m pc m pc m k
same V k
R
1
: 1024 :
m n
m
1
1
,
1024,
1024
;
m n
m pc m pc m n
same V n
R
1
2
:
1;
; :
) :
n
m for int i
i
m i
m
1
2
1
2
:
1;
; :
:
'
1
\
;
;
m for int i
i n m i
m i n pc m pc m
i i
same V i
i n pc m pc m same V
R
1
2
3
:
4
:
1
:
2 :
then
m if i
m k k else m k k* m