Rozwiązania należy dostarczyć w postaci pliku
Imie_Nazwisko_Assignment_3.tar.gz,
zawierającego spakowany katalog
Imie_Nazwisko_Assignment_3,
w którym znajdować się będą oryginalne pliki
- Smallstep.v
- StlcProp.v
- MoreStlc.v
- Norm.v
zmodyfikowane zgodnie z poniższymi poleceniami.
|
Zadanie 1 (10 p.) Rozwiąż zadanie
compiler_is_correct w
pliku Smallstep.v, przy
założeniu, że interesuje nas poprawność
kompilatora w odniesieniu do semantyki małych
kroków wyrażeń arytmetycznych (przechodnio-zwrotne
domknięcie
relacji astep).
|
Zadanie 2 (20 p.) Rozwiąż zadanie
stlc_arith w
pliku StlcProp.v.
|
Zadanie 3 (20 p.) Uzupełnij wszystkie
brakujące fragmenty kodu w
module STLCExtended
znajdującym się w
pliku MoreStlc.v.
|
Zadanie 4 (20 p.) Uzupełnij wszystkie
brakujące fragmenty kodu w
pliku Norm.v.
|
|
Uwaga: Pewien wpływ na ocenę rozwiązań
będzie miała zwięzłość dowodów. Zachęcam do
używania takich taktyk
jak auto
i eauto oraz taktyk
złożonych.
|