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:30] 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 685: | Řádek 685: | ||
| * ++ 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 711: | Řá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 | ||
