Formální metody specifikace

Z ωικι.matfyz.cz
Přejít na: navigace, hledání
Formální metody specifikace
Kód předmětu: NTIN043
Přednáší: David Bednárek

Zkouška

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

Zadání

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], Auloží 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, adrje-li A rovno 0, skočí na adresu adr, jinak normálně pokračuje
JMP adrskočí 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í

[DWORD]
[OPCODE]


MEM

data: DWORD → DWORD

dom(data) = 0..227-1


MEM_SET

ΔMEM
addr?: DWORD
value?: DWORD

data' = data - (addr?, data(addr?)) ∪ (addr?, value?)
addr ∈ dom(data)


CPU

ip: DWORD
a: DWORD


SYSTEM

cpu: CPU
mem: MEM

cpu.ip ∈ dom(mem.data)


INSTRUCTION

ΔSYSTEM
code: DWORD
opcode: OPCODE
addr: DWORD

opcode = code >> 27
addr = code & (227-1)
code = mem.data(cpu.ip)

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
cpu'.a = mem.data(addr)
cpu'.ip = cpu.ip + 1
mem' = mem


INSTRUCTION_ST

INSTRUCTION MEM_SET

opcode = 2
value? = cpu.a
addr? = addr
cpu'.a = cpu.a
cpu'.ip = cpu.ip + 4


INSTRUCTION_ADD

INSTRUCTION

opcode = 3
mem' = mem
cpu'.a = cpu.a + mem.data(addr)
cpu'.ip = cpu.ip + 4


INSTRUCTION_JMP

INSTRUCTION

opcode = 4
mem' = mem
cpu'.a = cpu.a
cpu'.ip = addr


INSTRUCTION_JZ

INSTRUCTION

opcode = 5
mem' = mem
cpu'.a = cpu.a
(cpu.a = 0 ∧ cpu'ip = addr) ∨ (cpu.a ≠ 0 ∧ cpu'.ip = cpu.ip + 1)


STEP = INSTRUCTION_LD ∨ INSTRUCTION_LD ∨ ... ∨ INSTRUCTION_JZ

Další zadání

Výtah

(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

(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í

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

(zdroj: mff-info-3)

Specifikovat databazove tabulky (primarni, popr. cizi klice, vkladani a odebirani zaznamu).

Křižovatka

(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

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

Citováno z „http://wiki.matfyz.cz/index.php?title=Formální_metody_specifikace&oldid=19072“