Rozdíly

Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.

--- courses:a4m33tvs:okruhy [2017/01/14 14:19]
marekp11 [(d) Přímé propagování min/max chyby.]
+++ courses:a4m33tvs:okruhy [2025/01/03 18:29] (aktuální)
@@ Řádek 586: / Řádek 586: @@
 ====(a) Z notace - principy a základní vlastnosti.====
-- 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
-- je zalozena na teorii mnozin a matematicke logice
+  * Z notace je zalozena na:
-Matematickou logikou je predikatovy kalkulus prveho radu.
+    * teorii mnozin
-Z je zalozena na modelech. System je modelovan pomoci:
+    * matematicke logice (predikatovy kalkulus prveho radu)
- - stavu (na zaklade stavovych promennych a jejich hodnot)
+    * na modelech
- - operaci, ktere mohou menit stav
+  * System je modelovan pomoci:
+    * stavu (na zaklade stavovych promennych a jejich hodnot)
+    * operaci, ktere mohou menit stav
 Schema = vzory deklaraci a omezeni
@@ Řádek 622: / Řádek 624: @@
 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=====
 ====(a) Architektura systemu JPF a vlastnosti systemu.====
+slidy(pdf strany) 30-37
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf
 ====(b) Pouziti systemu JPF pro generovani testovacich pripadu.====
+slidy(pdf strany) 19-28
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/11.javapathfinder.pdf
 =====10. testování OO softwaru=====
 ====(a) Anomálie DU párů====
@@ Řádek 632: / Řádek 725: @@
 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
   - SDIH - podobné SDA ale potomek přepíše něco v prarodiči a rodič pak používá špatně definovanou proměnnou
@@ Řádek 710: / Řádek 803: @@
 ====(d) Přímé propagování min/max chyby.====
-slidy 44-47  https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/13.statisticketestovani.pdf
+slidy(pdf strany) 19-21
+https://cw.fel.cvut.cz/wiki/_media/courses/a4m33tvs/prednasky/13.statisticketestovani.pdf
 ~~DISCUSSION~~

courses/a4m33tvs/okruhy.1484399964.txt.gz · Poslední úprava: 2025/01/03 18:24 (upraveno mimo DokuWiki)

Nahoru