(2)
Предположим обратное:
9
n
2
N
:
σ
0
(
n
)
=
φ
∧
σ
(
n
)
6
=
φ
.
Но это
противоречит определению
σ
0
,
ведь если
σ
(
n
)
6
=
φ
,
то в
σ
0
по крайней
мере попадет
n
.
Из справедливости (1) и (2) согласно определнию частичного по-
рядка следует, что
σ
≤
σ
0
,
ч.т.д
.
Отметим, что если два алгоритма
G
1
и
G
2
эквивалентны на уров-
не абстракции
σ
0
,
то они эквивалентны на любом уровне абстракции
σ
≤
σ
0
.
Действительно, уменьшение уровня абстракции (при прямом
исключении рассматриваемых операторов либо косвенным путем за
счет уменьшения числа рассматриваемых переменных) приводит к
дальнейшему транзитивному расширению в дереве поведения. А раз
на текущем уровне они совпадают, то и любые транзитивные операции
на одинаковых множествах приведут к одинаковому результату.
Обозначим алгоритм, полученный из алгоритма
G
на уровне аб-
стракции
σ
,
как
G
σ
,
построение которого аналогично построению на-
блюдаемого поведения: необходимо лишь провести операцию тран-
зитивного расширения достижимости операторов до множества всех
наблюдаемых операторов:
G
σ
= (
V
σ
,
E
σ
,
n
0
σ
);
8
n
2
N
:
n
2
N
σ
,
σ
(
n
)
6
=
φ
;
8
(
n
1
,
n
2
)
2
E
: (
n
1
,
n
2
)
2
E
σ
,
,
n
1
2
N
σ
∧
n
2
2
N
σ
∧
(
¬9
n
3
:
n
1
→
n
3
∧
n
3
→
n
2
);
n
0
σ
:
¬9
n
2
N
σ
:
n
→
n
0
σ.
Алгоритмы
G
и
G
0
σ
эквивалетны на уровне абстракции
σ
.
Необходимо отметить, что достаточный уровень абстракции явля-
ется единственным и максимальным:
8
σ
9
!
σ
0
:
G
,
σ
G
0
σ
∧ ¬9
σ
1
:
σ
0
≤
≤
σ
1
∧
σ
0
6
=
σ
1
.
Понятие уровня абстракции можно расширить следующим обра-
зом:
σ
:
N
→
2
P
V
D
,
где
P
V
D
—
множество предикатов над переменными алгоритма и их
доменами, задающих условия корректности алгоритма.
Достаточный уровень абстракции определяется аналогично: если
в наблюдаемый предикат входит переменная
v
2
V
,
то во множество
попадают все операторы, от которых
n
зависит по переменной
v
,
и все
операторы, от которых
n
зависит по управлению.
Основная идея метода заключается в когерентности работы алго-
ритма [8–11] его поведение изменяется лишь в операторах ветвления,
поэтому логично проверять корректность работы алгоритма на таких
наборах данных, при которых его поведение изменяется, а также в
70
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
