9 / 16
Разработка и исследование синтетического метода верификации программы…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
57
Шаг 1.
Разметка программы и трансляция ее в идентичный помеченный
текст. Каждый оператор помечен меткой
m
. Метки начала и конца программы
считаем заданными. При трансляции любого оператора вводим метку начала,
меткой конца является начало следующего оператора (табл. 2).
Таблица 2
Трансляция программы в помеченный текст
Оператор программы
Помеченный оператор программы
func
:
m func
v E
:
m v E
1 2
;
P P
1 1 2
: ;
:
m P m P
1
2
if bthenP elseP
1 1
2 2
:
:
:
m if bthenm P elsem P
1
whilebdo P
1
:
:
m while bdom P
Шаг 2.
Построение булевой формулы, определяющей множество начальных
состояний программы:
0
0
,
&
,
S V PC Prev V pc m
где
Prev V
— предусловие, определяю-
щее возможные начальные значения переменных (
0
m
метка начального со-
стояния программы,
( )
,
Prev V true
в случае если ограничений на начальные
состояния не наложено).
Шаг 3.
Построение предикатов для переходов:
1
:
;
:
m func m
1
1
,
,
m func m pc m pc m same V
R
—
в этом предикате ниче-
го не изменилось;
1
:
;
:
m v E m
1
1
,
,
{ }
m v E m pc m pc m v E same V v
R
—
измени-
лись
pc
и
;
v
1 1
2 2 3
:
:
:
:
m if b thenm P else m P m
1 1
2 2
1
,
,
,
m if b then m P elsem P b pc m pc m same V
R
—
если
b
истинно, то выполняем
1
;
P
1 1
2 2
2
:
:
if b then m P elsem P b pc m pc m same V
R
—
если
b
ложно, то выполняем
1
;
P
1 1 3
1 1 3
, ,
, ,
m P m m P m
R
R
—
выполняем
1
P
или
2
P
и выходим;
1
2
:
:
:
m while b do m P m
1
2
1
,
: ,
:
m while b do m P m b pc m pc m same V
R
— если
b
истинно, выполняем
;
P
2
b pc m pc m same V
1 1 2
, ,
m P m
R
— если
b
ложно, выходим из цикла.