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 16:20] marekp11 [(c) Alloy - prvky syntaxe jazyka, signatura, pole, relace, množinové operátory, relační operátory, fakta, funkce, predikáty, tvrzení, jak se provádí analýza specifikace.] |
courses:a4m33tvs:okruhy [2025/01/03 18:29] (aktuální) |
||
|---|---|---|---|
| Řádek 669: | Řádek 669: | ||
| **relační operátory** | **relační operátory** | ||
| - | * -> sipka (soucin) | + | * -> sipka (soucin) ... konkatenace |
| - | * ~ transpozice | + | * ~ transpozice ... zrcadlovy obraz |
| * . dot join | * . dot join | ||
| - | * [] box join | + | * {(a,b)}.{(a,c)} = {} |
| - | * ^ tranzitivni uzaver | + | * {(a,b)}.{(b,c)} = {(a,c)} |
| - | * reflexivne-tranzitivni uzaver | + | * {(a)}.{(a)} = nedefinovano !! je definovano, tehdy a jen tehdy, jestlize obe nejsou unarni relace !! |
| - | * <: omezeni domeny | + | * 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 | * :> omezeni obrazu | ||
| * ++ prepsani | * ++ prepsani | ||
| - | **fakta** | + | **fakta** jsou dalsi omezeni na signatury |
| + | * fact selfAncestor { no p: Person | p in p.^parents } | ||
| - | **funkce** | + | **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** | + | **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í** | + | **tvrzení** slouzi jako dodatecna omezeni k overeni. Neni-li omezeni vyjadrene tvrzenim splneno, vyprodukuje se protipriklad. |
| - | **jak se provádí analýza specifikace** | + | **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 705: | Řá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 | ||
