Formální metody specifikace
Formální metody specifikace | ||||
|
Obsah
Zkouška[editovat | editovat zdroj]
Zkouška je ústní a typicky společná s dalšími Bednárkovými zkouškami. Bednárek zadá nějakou situaci a úkolem zkoušeného je napsat příslušnou specifikaci. Jazyk specifikace je libovolný, ale všechna (nebo téměř všechna) zadání jdou popsat v Zetku. Po napsání specifikace si ji Bednárek prohlédne, okomentuje a bez nějakých dalších průtahů oznámkuje.
Pokud chcete přípravu na zkoušku vzít pragmaticky, naučte se tedy jen jazyk Z.
Jedno konkrétní zadání i s řešením[editovat | editovat zdroj]
Zadání[editovat | editovat zdroj]
Máme CPU se dvěma registry - IP (adresa právě vykonávané instrukce) a A (akumulátor). Oba mají 32 bitů. CPU je propojeno 32-bitovou sběrnicí s pamětí, schopnou adresovat 227 32-bitových hodnot.
CPU umí následující instrukce:
LD A, [adr] | načte obsah paměti na adrese adr do registru A |
---|---|
ST [adr], A | uloží obsah paměti z registru A na adresu adr |
ADD A, [adr] | přičte k registru A hodnotu v paměti na adrtese adr |
JZ A, adr | je-li A rovno 0, skočí na adresu adr, jinak normálně pokračuje |
JMP adr | skočí na adresu adr |
Instrukce jsou dlouhé 32 bitů, prvních 5 bitů je opcode, zbylých 27 určuje adresu v paměti (operand).
Specifikujte:
- paměť
- CPU
- celkový stav
- krok procesoru
Řešení[editovat | editovat zdroj]
[DWORD]
[OPCODE]
MEM |
---|
data: DWORD → DWORD |
dom(data) = 0..227-1 |
MEM_SET |
---|
ΔMEM |
data' = data - (addr?, data(addr?)) ∪ (addr?, value?) |
CPU |
---|
ip: DWORD |
SYSTEM |
---|
cpu: CPU |
cpu.ip ∈ dom(mem.data) |
INSTRUCTION |
---|
ΔSYSTEM |
opcode = code >> 27 |
INSTRUCTION je takový céčkový union. C-like kód v predikátech by samozřejmě šel přepsat v normálních aritmetických operacích v Z.
INSTRUCTION_LD |
---|
INSTRUCTION |
opcode = 1 |
INSTRUCTION_ST |
---|
INSTRUCTION MEM_SET |
opcode = 2 |
INSTRUCTION_ADD |
---|
INSTRUCTION |
opcode = 3 |
INSTRUCTION_JMP |
---|
INSTRUCTION |
opcode = 4 |
INSTRUCTION_JZ |
---|
INSTRUCTION |
opcode = 5 |
STEP = INSTRUCTION_LD ∨ INSTRUCTION_LD ∨ ... ∨ INSTRUCTION_JZ
Další zadání[editovat | editovat zdroj]
Výtah[editovat | editovat zdroj]
(zdroj: mff-info-1)
Vytahy v budove, n pater, m vytahu, k - kapacita vytahu.
Úkol: specifikace, ktera zaruci, ze bude kazdy pasazer dopraven.
Poznámka: Vhodné zadefinovat tlačítka na patrech a ty pak napojit na pasažéry.
Instukce[editovat | editovat zdroj]
(zdroj: mff-info-2)
Obrazek:
ALU REG +-----+ A MEM +----+ | | ===>+---+ | | | | D | | | |<==>| | <==>| | +----+ +-----+ +---+
Nejaka instrukce veme data z pameti nebo z registru a vysledek zapise do registru.
Úkol: Modelovat provozovani instrukci na procesoru.
Poznámka: S jistými omezeními lze namodelovat i petriho sítí.
Další varianta instrukcí[editovat | editovat zdroj]
Specifikujte sémantiku programovacího jazyka, který má celočíselné proměnné a umí následující typy příkazů:
a = konst
a = b + c
a = b - c
if (a > 0) b = c
if (a == 0) b = c
Není to moc těžké, jen to chce promyslet do detailů. Program je nejlépe funkce N -> Instruction (pozice instrukce dá instrukci), dále potřebujeme aktuálni stav (IP: N, vars: var_name -> Z) a všechno to nějak slepit. Já jsem to slepoval přímo v instrukcích - vždy se provádí ta instrukce, která je nařadě a pokud nejsme na konci, tak se posune IP. Nezapomeňte někde definovat, jak se stav programu nastaví na začátku běhu a kdy to běh programu skončí.
Relační databáze[editovat | editovat zdroj]
(zdroj: mff-info-3)
Specifikovat databazove tabulky (primarni, popr. cizi klice, vkladani a odebirani zaznamu).
Křižovatka[editovat | editovat zdroj]
(zdroj: mff-info-4)
Krizovatku - nekolik silnic, kazda silnice muze mit vic pruhu pro ruzne smery, kazdy smer ma svuj semafor. Specifikace by mela o zadane krizovatce rozhodnout, jestli je korektni, tj. jestli muze dojit k bouracce, kdyz se ridici budou ridit podle semaforu.
Zkouskove terminy[editovat | editovat zdroj]
Zapisovani na zkouskove terminy, pravidla jako ve skutecnosti: lze byt zapsan jen na jeden termin toho predmetu najednou, maximalne 3krat a to jen pokud predtim dostal 4, zapsat se lze jen na teminy z predmetu, ktere mate zapsane. Na kazdy termin je datum, na ktere se lze prihlasit nebo odhlasit.
typy:
[DATUM, PREDMET, ID, ZNAMKA]
schemata:
STUDENT = skore: PREDMET->{(DATUM, ZNAMKA)} | zapsanePr: PREDMET -> BOOL | zapsaneTer: PREDMET -> DATUM + ty podminky
OBSAZENI = kapacita:N | obsazeno:N + kapacita >= obsazeno
TERMINY = seznam: PREDMET x DATUM -> OBSAZENI
SIS = terminy:TERMINY | studenti:ID -> STUDENT
PRIHLASIT = delta SIS | predmet?: PREDMET | datum?: DATUM | id?: ID + zvetseni "obsazeno" a pridani do zapsaneTer
ODHLASIT = analogicky
VYCERPAT_TERMIN = delta SIS | predmet?: PREDMET | datum?: DATUM | id?: ID | znamka?: ZNAMKA + odebrani ze zapsaneTer, prip. zapsanePre a pridani vysledku do skore
VYPSAT_TERMIN = delta SIS | predmet?: PREDMET | datum?: DATUM | kapacita?: N + pripsani do seznamu terminu - tohle ani nemuselo byt
Az na nejake chyby v syntaxi Z tohle reseni bylo v poradku
Užitečné odkazy[editovat | editovat zdroj]
- [1] oficialni slidy
- Poznámky (35 MB skenované, místy až příliš stručné)
- Analýza a návrh softwarových systémů (státnicové výpisky)
- mff-info: 1 2 3 4
- Z na wikipedii (en) z této stránky jsou skvěle vysvětlené příklady v The Z Notation: a reference manual (každý si může navíc vybrat svůj oblíbený formát :)
- Něco k jazyku Z
- Z FAQ (textový soubor via ftp)
- Zdroj informací k Petriho sítím
- Pěkné příklady na Petriho sítě