Инвариантные соотношения. Тема 7

1.

Инвариантные соотношения
• Соотношение x= инвариантно на дуге
e, если для любого маршрута =e1,…en,
нач(e1)=vстарт, en=e
x =
• Множество инвариантных соотношений
дуги e:
ω
ω
{x=τ | x =τ }¿

2.

Пример
старт(z)
x := z
x := f(x)
y := z
y := f(y)
Как связаны x и y?
x==y?
• Inv(e)={
x=x,
y=y,
z=z,
x=y,
y=x}
p(y)
1
стоп(x,y)
0
• В операторе
стоп(x,y)
можно y
заменить на x

3.

Функциональные сети
• Способ эффективного представления
множества утверждений вида x= .
• Пример:
z=f(h(y),a), y=a, v=h(y), u=g(v,z),
v=h(a), z=f(v,a), u=g(h(a), f(h(y),a)),
u=g(h(a),z), z=f(h(y),h(y)),
…..
x=x, y=y, z=z, u=u, v=v
Кодируем компактным
способом

4.

Функциональные сети: пример
• «Базовые» утверждения
x1 = a
x2 = f(x1,x1)
x3 = f(x2,x2)
...
xn = f(xn-1,xn-1)
• Общее количество утверждений:
– c1=2
– ci+1=1+ci2
экспненциальное кол-во утверждений

5.

Функциональные сети
• Функциональная сеть s=(
См пример дальше
– {c1,…cn} - конечное множество
элементов(квадратики)
– = { 1,…, k} – разбиение на классы(овалы)
равенства: i j = , 1 … k =
– : X C F (дуги к квадратикам)
(c) – символ переменной или константы или
функциональный символ, приписанный элементу
– : x N (дуги к овалам)
(с,i) - класс равенства, соответствующий i-ому
аргументу. Определён при i=1..r( (с))

6.

Функциональные сети: пример
z=f(h(y),a)
y=a
v=h(y)
u=g(v,z)
1. Сгруппируем
«равные» термы
(овалами)
2. Дуги к «классам
равных»
u
g
z
v
f
h
y
a

7.

Ациклические сети
• Ациклическая сеть
Подкласс функ-их сетей
(более правильные сети)
– Нет дублей.
Элементы с1,c2 – дубли, если (c1)= (c2)
& i : (c1,i) = (c2,i)
– Нет контуров.
Последовательность элементов c1,…,cm –
контур, если
• c1 = cm
• i=1..m-1 j : ci+1 (ci,j)
• Далее – только ациклические сети

8.

Множество утверждений
• Элемент(вершина) с знает терм , если
– = (c), если (c) X C
– =f( 1,…, n) , если (c)=f F
& i=1..n : (c,i) знает i
• Класс знает , если c : с знает
• Множество утверждений сети s:
утв(s) = {x= | знает x
знает }
Все&
возм
вершины
т.ч.

9.

Приведённая сеть
• Приведённая сеть ред(s)
– Нет пустых классов.
Удаление = (итеративно):
Ациклические, без
дублей, но нет пуст.
классов вершин
(ничего не дающих)
• Удаляем все c , такие что (c,i)= для некоторого i
• Удаляем
– Нет недостижимых классов (итеративно):
Класс недостижим, если
( c i N : (c,i) ) & ( c : (c) X)
• Обозначение: FS – множество приведённых
функциональных сетей

10.

Приведённые сети
• Лемма. утв(ред(s)) = утв(s).
• Лемма. Если s1, s2 - приведённые, то
s1=s2 утв(s1)=утв(s2)
изоморфны

11.

Манипуляции над приведёнными сетями
Пересечение
• Произведение сетей s1 s2 = ( :
если sk=( k k k k k=1,2, то
– = {(c1,c2) | c1 1 & c2 2 & 1(c1)= 2(c2) }
– ((c1,c2)) = 1(c1) = 2(c2)
– = { 1 2 | 1 1 & 2 2 }
– ((c1,c2),i)= 1(c1,i) 2(c2,i)
• Пересечение сетей s1 s2 = ред(s1 s2)

12.

Пример
Появятся
пустые и не
достижимые
элементы, их
выкинем
s2
z
u
f
v
y
f
a
h
s1 s
s2
s1
u
u
g
z
v
z
f
f
f
h
h
y
a
y
v
a

13.

!!!
утв(s1 s2)=утв(s1) утв(s1) ?
• Лемма. 1 2 знает
1 знает & 2 знает
• Доказательство.
Ранг элемента с:
– ранг(с)=0, если (c) X C (перем или
конст)
– ранг(с)=1+max { ранг( 1(c,i)) | i=1..r( (с))
Ранг класса :
– ранг( )= max { ранг(с) | c }
Индукция по рангу...

14.

Доказательство
1 2 знает
c1,c2) 1 2 : c1,c2) знает
c1 1,c2 2 :
((c1,c2))= 1(c1)= 2(c2) & c1,c2) знает
c1 1,c2 2 : ((c1,c2))= 1(c1)= 2(c2) &
& ( ((c1,c2))=x X C & =x
V ((c1,c2))=f F &
& =f( 1,…, n)& i=1..n: ((c1,c2),i)знает i)

15.

Индукция по рангу
• ранг( 1 2 )=0 X C
c1 1,c2 2 : ((c1,c2))= 1(c1)= 2(c2) &
& ( ((c1,c2))=x X C & =x
V ((c1,c2))=f F &
=f( 1,…, n)& i=1..n: ((c1,c2),i)знает i)
c1 1,c2 2 : 1(c1)= 2(c2) X C
c1 1,c2 2 : c1знает & c2знает
1знает & 2знает

16.

Индукция по рангу
• ранг( 1 2 )=k>0 X C
• c1 1,c2 2 : ((c1,c2))= 1(c1)= 2(c2) &
& ( ((c1,c2))=x X C & =x
V ((c1,c2))=f F &
=f( 1,…, n)& i=1..n: ((c1,c2),i)знает i)
c1 1,c2 2 : 1(c1)= 2(c2)=f F &
& =f( 1,…, n)& i=1..n:
1(c1,i) 2(c2,i) знает i
c1 1: 1(c1)=f F & =f( 1,…, n)& i=1..n: 1(c1,i) знает i
& c2 2: …
1знает & 2знает
Конец доказательства

17.

утв(s1 s2)=утв(s1) утв(s1) ?
• Лемма. утв(s1 s2)=утв(s1) утв(s1)
• Доказательство.
утв(s1 s2)=(по опр ред.)=утв(s1 s2)=
= {x= | 1 1, 2 2 : 1 2 знает x
& 1 2 знает } =
= {x= | 1 1, 2 2 : 1знает x
& 1знает & 2знает x & 2знает } =(лемма)
= {x= | 1 1 : 1знает x & 1знает }
{x= | 2 2 : 2знает x & 2знает } =
= утв(s1) утв(s1)
• Конец доказательства.

18.

Оценка размера s1 s2
Пример: размер сети = произведению сети
s2
… x2n-1
xn
x1
… xn
…
h
…
xn-1
s1 s2
s1
y1
x1
yn
… y2n-1
x1
y2n-1
h
…
h
xn
h
xn+1
…
h
xn+1
h
h
h
…
,,,
yn+1
h
…
h
h
h
yn+1
…
yn
x2n-1
…
yn-1
yn
y1
y1
h
h
y2n-1
x2n-1
xn-1
yn-1
h

19.

Полурешётка
• Теорема. (FS, ) – полурешётка.
• Доказательство.
– Коммутативность:
s1 s2=s2 s1 утв(s1 s2)=утв(s2 s1)
утв(s1 s2) = утв(s1) утв(s2) =
= утв(s2) утв(s1) = утв(s2 s1)
– Ассоциативность, идемпотентность –
аналогично
• Конец доказательства.

20.

Полурешётка
• (FS, ) – ограничена, т.к. для любой s утв(s)
конечно, а
s1 s2 утв(s1) утв(s2)
• Наибольший элемент 1
утв(1) = { x= | x X, T } ← утв-ет, что все утв-ия
выполняются
- недостижимость, противоречие.
Не представим в виде функциональной сети.
• (FS {1}, ) – полурешётка с обрывом цепей
s:s 1=s

21.

Преобразователи
• Добавление
терма
(аналог
вычисления
выражения)
func Eval(s : FS, : T) :
if = x X C then
if c : (c)=x then
return c
См слайд 24
n := 0; f := x
else // = f( 1,… n)
for i:=1..n
ci := Eval(s, i)
if c : (c)=f & i: (c,i)=ci then
return c
:= c // новый элемент
(c ) = f
for i=1..n
(c ,i) := i ci i
:= {c }
return c

22.

Преобразователи
• Утверждение. Если c =Eval(s, ), то c
знает .
• Доказательство. Индукция по
структуре терма .

23.

Преобразователи
proc Exec(s : FS, x:X, : T) : FS
• Эффект
присваивания c := Eval(s, ); c
[x:= ] (s)
\ {c | (c)=x }
:= cx // новый элемент
(cx) = x
:= {cx}
return ред(s)

24.

Эффект присваивания: пример
• z=f(h(y),a)
• y=a
• v=h(y)
u g
• u=g(v,z)
Достроим
[ y := f(z,h(y)) ] вершины
которые знают
который мы
• z=f(h(a),a) терм,
вычисляем
• y=f(z,a)
v
• v=h(a)
Принесение инфии переносится по
• u=g(v,z) присваиваниям и
тождественно
f
y
z
f
h
y
a

25.

Согласованность
Пусть А – присваивание.
• Лемма. Если {x= x = } = утв(s)
то {x= x Ae = Ae} = утв([A](s))
• Лемма. [A](s1 s2) = [A](s1) [A](s2)
Дистрибутивность

26.

Задача анализа инвариантов
(Задача глобального анализа)
• (FS, ) – полурешётка.
• Начальная разметка (для входных дуг)
0(
{x1,x2,…,xn}
)=
x1
x2
…
xn
• Функция переноса (не тождественна
только для присваиваний):
e
f(e1,e2) = [x:=
x :=
1
e2

27.

Согласованность
Теорема. Для стационарной разметки с
и любой дуги e
Утв( с e) = Inv(e)
Доказательство.
По лемме
I это П