Дерево поведения процесса может быть бесконечным, но из каж-
дой его вершины исходит конечное число дуг.
Состояние
s
= (
n, val
(
V
))
будет наблюдаемым на заданном уровне
абстракции
σ
,
если:
а)
σ
(
n
)
6
=
φ
;
б)
9
v
2
V
:
v
2
σ
(
n
)
∧
func
(
n, v
)
6
=
;
.
Тогда наблюдаемое поведение алгоритма на уровне абстракции
σ
есть ни что иное, как транзитивное расширение отношения достижи-
мости
R
до множества наблюдаемых состояний.
Назовем два алгоритма эквивалентными на уровне абстракции
σ
,
если их наблюдаемое поведение совпадает при одинаковых начальных
состояниях.
Достаточный уровень абстракции
σ
0
определяет ту часть алгорит-
ма, которую необходимо выполнить для наблюдения операторов, за-
данных уровнем абстракции
σ
.
Для выделения необходимых операто-
ров используется механизм зависимостей.
Существуют два основных типа зависимостей в последователь-
ной программе: зависимости по управлению, которые определяются
управляющими конструкциями программы, и зависимости по данным,
которые определяются переменными, используемыми в алгоритме.
Оператор
n
2
N
зависит по управлению от предиката
c
,
который
содержится в операторе условного ветвления
n
c
2
N
,
если в структуре
потока управления алгоритма от выбора пути выполнения, на который
потенциально влияет
c
,
зависит, будет ли выполнен оператор
n
.
Оператор
n
2
N
зависит по данным от оператора
n
0
,
если данные,
определяемые в
n
0
2
N
,
используются в
n
и потенциально могут
достичь
n
через последовательность присваиваний переменных.
Для достаточного уровня абстракции
σ
0
дадим следующее кон-
структивное определение. Если оператор
n
,
входит в наблюдаемое
поведение алгоритма, т.е.
σ
(
n
)
6
=
φ
,
то множество операторов
S N
,
от которых
n
транзитивно зависит по управлению или данным, войдет
в достаточный уровень абстракции вместе с оператором
n
и теми же
наблюдаемыми переменными:
σ
(
n
)
=
φ
)
sigma
0
(
n
)
=
φ
;
σ
(
n
)
6
=
φ
) 8
n
0
2
S
:
σ
0
(
n
0
)
=
σ
(
n
)
.
Докажем, что
σ
≤
σ
0
.
Согласно определению частичного порядка на множестве уров-
ней абстракции, надо доказать, что (1)
8
n
2
Nσ
(
n
)
σ
0
(
n
)
и
(2)
σ
0
(
n
)
=
φ
)
σ
(
n
)
=
φ
.
(1)
В силу определения достаточного уровня абстракции, если опе-
ратор
n
включается в уровень абстракции
σ
,
то он включается с теми
же наблюдаемыми переменными в
σ
0
,
т.е.
σ
(
n
)
σ
0
(
n
)
.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
69
