Jednoduché specifikace

Myšlenka rovnicových algebraických specifikací Velmi jednoduché jednosortové specifikace Příklady grupoidů Speciální vlastnosti abstraktního násobení

Jednoduché specifikace

Jiří Velebil: X01DML

10. prosince 2010: Jednoduché specifikace

1/19


Příklad (Připomenutí) Řešení rovnice ax = b, a 6= 0, probíhá stejně v Q, v R, v C, i v jakémkoli Zp , p prvočíslo. (Jde o tělesa!) ax · (ax) (a−1 · a) · x 1·x x a−1

= = = = =

b a−1 · b a−1 · b a−1 · b a−1 · b

(a má inversi a násobení je operace) (násobení je asociativní) (a−1 · a = 1) (1 je neutrální k násobení)

Polymorfní algoritmus, protože pracujeme s modely abstraktního datového typu (ADT) těleso.



2/19


Příklad (Specifikace seznamů jako ADT) 1 spec LIST is 2 sorts: list 3 operations: nil: --> list; 4 _#_:list,list --> list 5 variables: x,y,z:list 6 equations: x#nil=x; 7 nil#x=x; 8 x#(y#z)=(x#y)#z 9 endspec



3/19


Příklad (Specifikace zásobníků jako ADT) 1 spec STACK is 2 sorts: alphabet, stack 3 operations: a1: --> alphabet; 4 a2: --> alphabet; 5 a3: --> alphabet; 6 a4: --> alphabet; 7 nil: --> stack; 8 pop(_): stack --> stack; 9 push(_,_): alphabet,stack --> stack 10 variables: x:alphabet, s:stack 11 equations: pop(nil)=nil; 12 pop(push(x,s))=s 13 endspec Jiří Velebil: X01DML


4/19


Zápis je pseudokód, připomínající specifikační jazyk OBJ3. Viz například 1

K. Richta a J. Velebil, Sémantika programovacích jazyků, Karolinum, Praha 1997

2

J. A. Goguen, D. Coleman a R. Gallimore (eds.), Applications of Algebraic Specification Using OBJ, Cambridge University Press, 1992 http://www-cse.ucsd.edu/users/goguen/sys/obj.html

3

Předmět Prototypování algebraických specifikací, katedra počítačů.



5/19


Další specifikační jazyky 1

CASL (Common Algebraic Specification Language), viz http://www.cofi.info/CASL.html

2

. . . a řada dalších.

Možná literatura 1 W. Wechler, Universal Algebra for Computer Scientists, Springer-Verlag, Berlin, 1992



6/19


Problémy: 1

Co je operace? Co je rovnice?

2

Co je model rovnicové specifikace?

3

Jak modely porovnávat?

4

Co je zamýšlená sémantika rovnicové specifikace?

Odpovědi: 1

Operace jsou popsány finitárním typem. Rovnice jsou dvojice termů.

2

Modelem rovnicové specifikace je algebra daného typu, která splňuje dané rovnice.

3

Modely porovnáváme pomocí homomorfismů algeber.

4

Zamýšlená sémantika je iniciální algebra (doktrína no-junk-no-confusion). Jiří Velebil: X01DML


7/19


Příklad (Nejjednodušší jednosortová specifikace) spec NO_OPERATIONS is sorts: something endspec 1

Jedna sorta, žádné operace, žádné rovnice.

2

Model je jakákoli množina: X

3

Homomorfismus modelů je jakékoli zobrazení x

/ f (x)

X


f

/Y


8/19


Příklad (Abstraktní násobení bez axiomů — specifikace grupoidu) spec BINARY is sorts: binary operations: _*_:binary,binary --> binary endspec 1

Jedna sorta, jedna binární operace, žádné rovnice.

2

Model je jakákoli množina, vybavena binární operací: X ×X

?X

/X

Modelu říkáme grupoid.



9/19


Příklad (grupoidy, pokrač.) 3

Homomorfismus modelů je jakékoli zobrazení, které respektuje dané operace: (x, x 0 )

/ (f (x), f (x 0 )) _

_

X ×X ?X

X

x ?X x 0

f ×f

/Y ×Y

f

?Y

/Y / f (x ?X x 0 )


f (x) ?Y f (x 0 )


10/19


Příklad (Grupoidy) 1

Na X = ∅ existuje jediná binární operace, prázdné zobrazení ∅ : ∅ × ∅ → ∅. Proto h∅, ∅i je příklad grupoidu.

2

Na X = {a, b, c} definujeme binární operaci ? takto: x ?X y = x pro všechna x, y ∈ X . Popis ?X tabulkou: ?X a b c a a a a b b b b c c c c Je-li x v i-tém řádku a y v j-tém sloupci tabulky, pak v položce (i, j) je zapsán výsledek x ?X y . Dvojice hX , ?X i je grupoid.



11/19


Příklad (Grupoidy, pokrač.) 3

Ať X je množina všech zobrazení z {0, 1} do {0, 1}. Množina X má čtyři prvky: f1 : 0 7→ 0 f2 : 0 → 7 0 1 7→ 1 1→ 7 0 f3 : 0 7→ 1 f4 : 0 7→ 1 1 7→ 1 1 7→ 0 Skládání funkcí ◦ je binární operace na množině X , a hX , ◦i grupoid. Příslušná tabulka je: ◦ f1 f2 f3 f1 f1 f2 f3 f2 f2 f2 f2 f3 f3 f3 f3 f4 f4 f3 f2


proto je f4 f4 f2 f3 f1


12/19


Asociativita, komutativita, neutralita Abstraktní výpočty

Definice (Vlastnosti abstraktního násobení) Ať ? je binární operace na množině X . 1

Operace ? je asociativní, pokud pro všechna x, y , z ∈ X platí rovnost x ? (y ? z) = (x ? y ) ? z.

2

Operace ? je komutativní, pokud pro všechna x, y ∈ X platí rovnost x ? y = y ? x.

3

Prvek el je levý neutrální prvek operace ?, pokud pro všechna x ∈ X platí rovnost el ? x = x.

4

Prvek er je pravý neutrální prvek operace ?, pokud pro všechna x ∈ X platí rovnost x ? er = x.

5

Prvek e je neutrální prvek operace ?, pokud je pravým i levým neutrálním prvkem, tj. když pro všechna x ∈ X platí rovnost e ? x = x ? e = x. Jiří Velebil: X01DML


13/19



Příklad Operace ?X : ?X a b c a a a a b b b b c c c c 1 Je asociativní, protože podle definice pro všechna x, y , z ∈ {a, b, c} platí x ?X (y ?X z) = x a (x ?X y ) ?X z = x ?X z = x. 2

Není komutativní, protože například platí a = a ?X b 6= b ?X a = b.

3

Každý prvek množiny {a, b, c} je pravým neutrálním prvkem operace ?X : například a je pravý neutrální prvek, protože pro všechna x ∈ {a, b, c} platí x ?X a = x. Podobně: b i c jsou pravé neutrální prvky. Jiří Velebil: X01DML


14/19



Příklad (pokrač.) 4

Operace ?X nemá žádný levý neutrální prvek, a tudíž žádný neutrální prvek.

Příklad Na množině N definujeme: n ? m = nm . Protože platí 227 = 2 ? (3 ? 3) 6= (2 ? 3) ? 3 = 29 není binární operace ? asociativní.



15/19



Příklad abstraktního výpočtu: Lemma Jestliže binární operace ? na množině X má levý neutrální prvek el a pravý neutrální prvek er , pak platí el = er . Důkaz. el ? x = x pro všechna x ∈ X (protože el je levý neutrální). Speciálně: el ? er = er . Ale el = el ? er (protože er je pravý neutrální). Celkem: el = er .



16/19



Další příklad abstraktního výpočtu: Lemma Každá binární operace má nanejvýš jeden neutrální prvek. Důkaz. Pokud e a e 0 jsou neutrální prvky, potom e je pravý neutrální prvek a e 0 je levý neutrální prvek, a proto podle předchozího musí platit rovnost e = e 0 .



17/19



Ve zbytku semestru vybudujeme 1

„Rozumnéÿ násobení: ADT, ve kterém jdou „dobřeÿ řešit lineární rovnice. Výsledný ADT = grupa.

2

Další možný projekt (viz skripta): „klasickéÿ pravdivostní hodnoty: ADT, ve kterém jde „dobře dělatÿ klasická výroková logika. Výsledný ADT = Booleova algebra. Dělat nebudeme!



18/19



Použitá metoda = refinement ADT 1 Začneme se základním (velmi jednoduchým) ADT. 2

3

Postupně přidáváme sorty, operace, rovnice (= „zjemňováníÿ původního ADT). Ve specifikačních jazycích = import jednoduššího ADT do výsledného složitějšího ADT. Problémy: 1 2 3 4

Nedojde ke kolizi starého ADT s novým ADT? Nepřidáváme zbytečně mnoho operací, rovnic? Změní se homomorfismy nového ADT? Pokud ano, jak? . . . a řada dalších.



19/19

Jednoduché specifikace

Recommend Documents