{{predmet|Formální metody specifikace|David Bednárek|TIN043}}
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 2<sup>27</sup> 32-bitových hodnot.
CPU umí následující instrukce:
<table border> <tr><th>LD A, [adr]</th><td>načte obsah paměti na adrese adr do registru A</td></tr>
<tr><th>ST [adr], A</th><td>uloží obsah paměti z registru A na adresu adr</td></tr> <tr><th>ADD A, [adr]</th><td>přičte k registru A hodnotu v paměti na adrtese adr</td></tr>
<tr><th>JZ A, adr</th><td>je-li A rovno 0, skočí na adresu adr, jinak normálně pokračuje</td></tr> <tr><th>JMP adr</th><td>skočí na adresu adr</td></tr>
</table>
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]