Nem ellenőrzött!!!
Multiplexer
Tartalom Csatorna: .................................................................................................................................... 2 Jelölések: ............................................................................................................................................. 2 Megjegyzés: ..................................................................................................................................... 2 műveletei:............................................................................................................................................ 2 Tulajdonságai:...................................................................................................................................... 3
split: ............................................................................................................................................ 4 Definíció:.............................................................................................................................................. 4 Létezik-e split? ................................................................................................................................. 4
MUX ............................................................................................................................................ 4 Feltételek: ............................................................................................................................................ 4 Program specifikáció: .......................................................................................................................... 5 Program: .............................................................................................................................................. 5 Megfelel- e a program a specifikációnak? ........................................................................................... 5
1
Nem ellenőrzött!!!
Multiplexer
Csatorna: P1
x
P2
P1, P2 folyamatok, az x a csatorna, amely a P1 folyamat outputját kapja meg és a P2 inputjának teszi hozzáférhetővé az adatokat. Maga a csatorna aszinkron üzenetküldés tárolására alkalma eszköz.
Jelölések: Ch(IH) : IH halmazbeli elemek tárolására alkalmas csatorna. Megjegyzés:
Sosem írunk le csatornaváltozót egymagába. Mindig kell egy x csatornáról (papíron) tárolni az aktuális tartalmát, mostantól ez lesz az x és kell a története, az x ami azt mutatja, hogy a keletkezése óta milyen elemek voltak rajta. Az x -re csak rakni lehet és az értékadás jobb oldalára csak saját magának való értékadás esetén kerülhet: x : x ; e Előbbiekből következik, hogy az implementációból ki lehet hagyni. Ezt csak a bizonyítások egyszerűsítésére/feltétel bizonyíthatóságára használjuk. Kihagyása a helyességet nem rontja el, és nem kell foglalkoznunk azzal a nehézséggel, hogy hogyan implementáljunk egy megszámlálható hosszú sort. A csatorna sor adatszerkezetű, tehát
műveletei: lf számítása x:=<>
x
,x
x:=hiext(x,e) x:=lorem(x)
lf(x:=<>, R) = R lf(x:=hiext(x,e),R) = R x x;e, x x ;e lf(x:=lorem(x) ha x <>, R) = ( x
x.lov x.dom~|x|
utolsó elemét az x-nek visszaadja, ha van ha nincs „elszál” x elemszáma
Rx←lorem(x))
(x
R)
// a x;e jelölés az x-hez jobbról hozzáfőzi az e-t
2
Nem ellenőrzött!!!
Multiplexer
Tulajdonságai: 1. Az x mindig az x prefixe
2. x -lorem(x) = ( x - x); x.lov
3
Nem ellenőrzött!!!
Multiplexer
split: split: Ch(IH) x Ch(IH) x Ch(IH)→IL
Definíció: 1. split(<>, <>, <>) = ↑ 2. split(a, b, c) ⇒ x ∊IH: split(a;x, b;x, c) ⋏ split(a;x, b, c;x) 3. A split a legszűkebb 1, 2 tulajdonságú függvény A 3-dik feltételre azért van szükség, hogy például a mindenre igazat visszaadó függvény ne feleljen meg a definíciónak. /* a logikai függvények jellemezhetők az igazsághalmazukkal, és a legszűkebb az lesz amelyiknek az igazsághalmaza a legkisebb.*/ Létezik-e split?
Olyan függvény van ami az 1, 2 tulajdonságokkal rendelkezik, de van-e legszűkebb? Van-e a metszetnek közös eleme? Van, mert az 1 tulajdonsággal rendelkeznie kell Van-e legkisebb? Van. Bizonyítás: 1. lépés: split1(<>, <>, <>) = ↑ split1∪2(<>, <>, <>) = ↑ split2(<>, <>, <>) = ↑ 2. lépés: tegyük fel, hogy valamely a, b, c ∊IH - ra: split1(a, b, c) ⋏ split2(a, b, c) teljesül ⇒ split 2. tulajdonsága miatt x ∊IH: split1(a;x, b;x, c) ⋏ split1(a;x, b, c;x) ⇒ x ∊IH: split2(a;x, b;x, c) ⋏ split2(a;x, b, c;x) split1∪2(a, b, c)
MUX x y
MUX
z
Feltételek: adat ne vesszen el adat ne keletkezzen legyen sorrendtartó mindig dolgozzon, ha van x-en vagy y-on adat.
4
Nem ellenőrzött!!!
Multiplexer
Program specifikáció: A= Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) ¯x
x
¯y
y
¯z
z
B= Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) x Ch(IH) x’
Q=( x
¯x’
x
x
x
¯y’
y’
y
y
y
y
¯z’
z’
z
z
z
z
)
INIT h
1) K = split( z , x - x, y - y) invh (Q) 2) | x | |y|
k ↪h | x -x| k ↪h | y -y|
k k
/* Vegyük észre, hogy mindkét csatornáról le kell szedni az elemeket! */
Program: S = (SKIP, { x, z := lorem(x), hiext(z, x.lov), ha x y, z := lorem(y), hiext(z, y.lov), ha y } ) /* Vegyük észre, hogy a program is mindkét csatornáról vesz le. */
Megfelel- e a program a specifikációnak? 1) invariáns Q ⇒ lf(s0, K) = K = split( z , x - x, y - y) <>,<>-<>,<>-<> <> <>
split(<>,<>,<>) = ↑ //split 1. def.
K ⇒ lf(S, K) feltétel átvihető, SKIP elhagyható s1 ) split( z , x - x, y - y) ⋏ x <>⇒ split( z ; x.lov, x - lorem(x), y - y) split 2. tulajdonsága miatt: x - lorem(x) = ( x -x); x.lov ⇒ ⇒ split 2. def s2 ) split( z , x - x, y - y) ⋏ x <>⇒ split( z ; y.lov, x - x, y - lorem(y)) split 2. tulajdonsága miatt y - lorem(y) = ( y - y); y.lov ⇒ ⇒ split 2. def
5
Nem ellenőrzött!!!
Multiplexer
2) haladás: a. | x | k ↪h | x -x| k variáns függvény tétele: t=k-(| x - x|)
x
k ⋏ (| x - x |
0
k-(„k-nál kisebb szám”) > 0 x k ⋏ (| x - x |
k ⋏ t < m ) ⋎ |x - x |
k
Azt mondom, hogy én tudnám bizonyítani:
x
k ⋏ (| x - x |
k⋏t<m
Amiből: 1. ↪ definíció első pontja alapján:
x
k ⋏ (| x - x |
2. Jobb oldal gyengítésével: x k ⋏ (| x - x |
k⋏t<m k ⋏ t < m ) ⋎ |x - x |
k
k ⋏ t < m:
∃ s1 Nézzük először meg a P ⋏ ┒Q –t hátha egyszerűsíthető. (x
k ⋏ (| x - x |
(x
k ⋏ (| x - x |
⋎ (x
k ⋏ (| x - x |
A sárga ellentmondás, így az a része a vagy ágnak elhagyható, A kékkel írt közül a t = m a szűkebb tehát a másik elhagyható. feltétel teljesülése esetén: Feltétel átvihető x k ⋏ (| x - x | ⇒ ⇒x
k ⋏(k – | x - lorem(x)| <m)
Az | x - lorem(x) |= | x - x|+1 ⇒ ⇒k – (| x - x |) – 1 < k – (| x - x |) = m
6
Nem ellenőrzött!!!
Multiplexer SKIP ág: x k ⋏ (| x - x | x = <> ⇒| x - x |= | x | ,de
x
k és | x |
⊳ S s2 feltétel átvihető SKIP elhagyható x k ⋏ (| x - x | ⇒ ⇒( x
k ⋏ (| x - x |
Mivel ⋎ az elválasztás elég az egyik oldalnak elég következnie. b. s1 – hez hasonlóan
7
