navigation
hledat
Rozdíly
Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.
|
courses:a4m33tvs:okruhy [2017/01/17 13:50] marekp11 [(a) Z notace - principy a základní vlastnosti.] |
courses:a4m33tvs:okruhy [2025/01/03 18:29] (aktuální) |
||
|---|---|---|---|
| Řádek 587: | Řádek 587: | ||
| * je jedna ze standartizovanych notaci | * je jedna ze standartizovanych notaci | ||
| - | * Z je prave jenom notace | + | * Z je prave jenom notace |
| * neni exekucni | * neni exekucni | ||
| * neni to programovaci jazyk | * neni to programovaci jazyk | ||
| Řádek 624: | Řádek 624: | ||
| https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/05.alloy.pdf | https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/05.alloy.pdf | ||
| + | |||
| + | **atom** je primitivni entita | ||
| + | * nedelitelna | ||
| + | * nemenna | ||
| + | * neinterpretovana (nema zadnou vestavenou vlastnost) | ||
| + | |||
| + | **relace** je struktura, ktera zachycuje vztahy mezi atomy. je to mnozina n-tic, kazda n-tice je sekvence atomu | ||
| + | |||
| + | **signatura** zavadi mnozinu atomu, je vrcholova pokud je deklarovana nezavisle na ostatnich signaturach | ||
| + | * deklarace: sig A {} | ||
| + | * rozsireni: sig A1 extends A {} | ||
| + | * podmnozina: sig A1 in A {} | ||
| + | * abstraktni (nema zadne elementy): abstract sig A {} | ||
| + | |||
| + | **pole**, relace se deklaruji jako pole v signature: | ||
| + | * sig A { f: e} ... domena A, obraz e | ||
| + | * sig A { f1: A} ... binarnirelace, f1 je podmnozinou A x A | ||
| + | * sig B { f2: A -> A } .. ternarni relace, f2 je podmnozinou B x A x A | ||
| + | |||
| + | **nasobnosti** | ||
| + | * signatury: m sig A { f: e} | ||
| + | * poli: sig A { f: m e}, sig A { f: e1 m -> n e2} | ||
| + | * mozne nasobnosti (m, n): | ||
| + | * set: jakykoli pocet | ||
| + | * some: jeden a vice | ||
| + | * lone: nula nebo jeden | ||
| + | * one: presne jeden | ||
| + | |||
| + | **kvantifikatory:** all, some, no, lone, one | ||
| + | |||
| + | **logicke operatory:** not (!), and (&&), or (||), implies (=>), else, (<=>) | ||
| + | |||
| + | **množinové konstanty** | ||
| + | * none: prazdna mnozina | ||
| + | * univ: univerzalni mnozina | ||
| + | * ident: identita | ||
| + | |||
| + | **množinové operátory** | ||
| + | * + : sjednoceni | ||
| + | * & : prunik | ||
| + | * - : rozdil | ||
| + | * in : podmnozina | ||
| + | * = : rovnost | ||
| + | |||
| + | **relační operátory** | ||
| + | * -> sipka (soucin) ... konkatenace | ||
| + | * ~ transpozice ... zrcadlovy obraz | ||
| + | * . dot join | ||
| + | * {(a,b)}.{(a,c)} = {} | ||
| + | * {(a,b)}.{(b,c)} = {(a,c)} | ||
| + | * {(a)}.{(a)} = nedefinovano !! je definovano, tehdy a jen tehdy, jestlize obe nejsou unarni relace !! | ||
| + | * p a q | ||
| + | * jsou dve relace a nejsou obe unarni | ||
| + | * p.q je relace, ktera vznikne kombinaci vsech n-tic z p a m-tic z q a pridanim jejich spojeni, pokud tento existuje. | ||
| + | * [] box join ... p[q] == q.p | ||
| + | * ^ tranzitivni uzaver ... ^r = r + r.r + r.r.r + ... | ||
| + | * * reflexivne-tranzitivni uzaver ... *r = ^r + iden | ||
| + | * <: omezeni domeny | ||
| + | * :> omezeni obrazu | ||
| + | * ++ prepsani | ||
| + | |||
| + | **fakta** jsou dalsi omezeni na signatury | ||
| + | * fact selfAncestor { no p: Person | p in p.^parents } | ||
| + | |||
| + | **funkce** (makra) jsou pojmenovane vyrazy | ||
| + | * 0 a vice argumentu | ||
| + | * navratova hodnota je vyraz | ||
| + | * vyvolavaji se pouze, pokud je na ne odkazovano | ||
| + | * fun sisters [p: Person]: { { w: Woman | w in p.siblings } } | ||
| + | |||
| + | **predikáty** jsou dobre v situacich: | ||
| + | * omezeni, ktera nechceme zaznamenat jako fakta | ||
| + | * omezeni, ktera chceme pouzivat vicekrat | ||
| + | * vyvolavaji se pouze, pokud ne na ne odkazovano | ||
| + | * pred BloodRelated [p: Person, q: Person] { some p.*parents & q.*parents } | ||
| + | |||
| + | **tvrzení** slouzi jako dodatecna omezeni k overeni. Neni-li omezeni vyjadrene tvrzenim splneno, vyprodukuje se protipriklad. | ||
| + | |||
| + | **jak se provádí analýza specifikace** | ||
| + | * prikazem **run** (pouze prvni prikaz v souboru) se pusti analyza modelu, tzn. hledej instance modelu | ||
| + | * hleda se pouze v omezenem prostoru instanci urcenem rozsahem | ||
| + | * run {} .. prednastaveny rozsah 3 | ||
| + | * run {} for 5 ... rozsah 5 | ||
| + | * run { some Man && no Married } ... s podminkami | ||
| =====9. JPF===== | =====9. JPF===== | ||
| Řádek 641: | Řádek 725: | ||
| Souvisi to s dedenim a polymorfismem. | Souvisi to s dedenim a polymorfismem. | ||
| - | - SDA - state definition anomaly - přepisící metoda má jinou def množinu než přepisovaná | + | - SDA - state definition anomaly - přepisující metoda má jinou def množinu než přepisovaná |
| - ITU - inconsistent type use - nepřepisování ale volání parent metod | - ITU - inconsistent type use - nepřepisování ale volání parent metod | ||
| - SDIH - podobné SDA ale potomek přepíše něco v prarodiči a rodič pak používá špatně definovanou proměnnou | - SDIH - podobné SDA ale potomek přepíše něco v prarodiči a rodič pak používá špatně definovanou proměnnou | ||
