Arvutiteaduse instituut
  1. Esileht
  2. Automaadid, keeled ja translaatorid
EN
Logi sisse

Automaadid, keeled ja translaatorid

  • Üldinfo
  • Ajakava
  • Eksami näidised
  • Teemad
    • 1. Soojendus
    • 2. Regulaaravaldised
    • 3. Automaadid
    • 4. Avaldise struktuur
      • Avaldispuu läbimine
      • Eksami alusosa!
      • Regulaaravaldiste analüüs
        • Raskemad harjutused*
        • Isabelle*
      • Kodutöö
    • 5. Grammatikad ja lekser
    • 6. Käsitsi parsimine
    • 7. ANTLRiga töötamine
    • 8. Interpretaator
    • 9. Kompilaator
    • 10. Edasi!
  • Süvendus
  • Bitbucket
  • Moodle
  • Zulip
  • Zoom

Isabelle: Kui halba teha ei täi

Tihti väidame siin kursusel, et tahame kirjutada sellist usaldusväärsemat koodi, aga see jääb natuke intuitsiooni tasemele. Kindlasti on puhas programmi disain väga oluline samm headuse poole, sest nii on halba tegemise tõenäosus oluliselt väiksem. Kuidas saaks aga olla kindel, et programm ikkagi midagi halba ei tee?

Üks võimalus on kasutada sellist keskkonda, kus saame programmi kohta väiteid tõestada, ja arvuti kontrollib, kas ta on nende väidetega nõus. Selles ülesandes tutvume süsteemiga Isabelle. Kõigepealt tuleb see endale paigaldada. Tegemist on iseseisva Java rakendusega, mille paigaldamine peaks üsna lihtne olema. Esimesel käivitamisel ehitab ta valmis oma standardteegi, mis võtab üsna palju aega!

Eeldused

Selle ülesanne lahendamiseks pead olema valmis väga põgusa sissejuhatuse põhjal endale mõned funktsionaalprogrammeerimise põhitõed selgeks tegema: valguse tee ei ole lihtne tee.

Teiseks on vaja kõigepealt lahendada ExprMaster ülesandeid. Kui meetod elimNeg on Javas lahendatud, saame keskenduda sellele, et programmi kohta väiteid tõestada. Meil on siis aritmeetiline avaldis, kus esineb ainult liitmine ja unaarne miinus. Tahame lõpuks teisendada selle selliseks, kus kõik miinusmärgid on ainult lehtedes.

Programmi mall

Kõigepealt tuleks luua endale uus fail nimega akt.thy ja selle sisse kirjutada meie avaldise andmestruktuur:

theory akt
imports Main
begin

datatype exp = Num int | Add exp exp | Neg exp

definition ex1 :: exp where 
"ex1 = Neg (Add (Num 5) (Add (Neg (Num 3)) (Num (-4))))"

end

NB! Siin peab mooduli nimi (theory akt) langema kokku faili nimega. Defineerime meile tuttavate variantidega oma exp tüüpi andmestruktuuri. Avaldis on kas arvkonstant (Num), kahest avaldisest koosnes liitmine (Add) või avaldise vastand (Neg). Neid konstruktoreid saab kasutada peaaegu nagu Java. Kasutame aga matemaatilist funktsiooni rakendamise notatsiooni, nagu näiteks cos (x+1) + sin y + 1.

Avaldise väärtustamine

Defineerime nüüd meetodi eval. Siin tuleb lihtsalt täita lüngad (???). Funktsioone defineerime kasutades loogikavõrdust, mis pannakse jutumärkidesse. See on Isabelle süntaksi juures üks väga veider asi, millega tuleb praegu lihtsalt leppida, et nii on...

fun eval :: "exp ⇒ int" where
"eval (Num n) = ??? " |
"eval (Add e1 e2) = eval e1 ??? eval e2" |
"eval (Neg e) = ??? (eval e)"

value "eval ex1"

Kui oled definitsiooni korda saanud, saame avaldise väärtust küsida selle value käsuga. Selleks tuleb viia kursor sellele reale ja all output aknas peaks ilmuma tulemus.

Lehtedes esinevad arvud

Nüüd defineerime meetodi, mis oli ExprMaster klassis nimega valueList, aga siin on tal lühem nimi, sest IDE ei kirjuta automaatselt nimesid lõpuni...

fun vals :: "exp ⇒ int list" where
"vals (Num n) = [n]" |
"vals (Add e1 e2) = vals e1 @ vals e2" |
"vals (Neg e) = vals e"

Selles näites kasutame Isabelle'i liste: jälgi singletoni ja listi ühendamise süntaksit. Võid jälle proovida arvutada value "vals ex1", aga nüüd on Sinu kord implementeerida funktsioon, mis oli Java harjutuses nimega signedValueList. See peaks tagastama väärtuste listi, kus on arvud „õigete“ märkidega. Lihtsam on see defineerida abifunktsiooni abil, mis võtab märgi endale argumendina:

fun sigvals' :: "exp ⇒ int ⇒ int list" where
"sigvals' (Num n) sign = ???" |
"sigvals' (Add e1 e2) sign = ???" |
"sigvals' (Neg e) sign = ???"

fun sigvals :: "exp ⇒ int list" where
"sigvals e = sigvals' e 1"

Nüüd tõestamine!

Kui arvutame selle sigvals listi summa (kasutades Isabelle standardteegi funktsiooni sum_list), peaksime saama avaldise väärtuse tagasi. Proovi kõigepealt value "sum_list (sigvals ex1)", aga üldiselt peaks siis kehtima järgmine teoreem, mida üritame kohe induktsiooniga tõestada!

theorem "sum_list (sigvals e) = eval e"
apply (induction e)
apply auto
done

Nüüd tuleb liikuda sinna, kus Isabelle on pahandanud ja vaadata väljundit (sel juhul vaja sisse lülitada "Proof state" checkbox output kasti juures. Teine variant on paremal "state" vaadet avada). Seal peaks olema kirjas, et kinni on ta jäänud sellise asja tõestmisega:

sum_list (sigvals' e 1) = eval e ⟹ sum_list (sigvals' e (-1)) = - eval e

See on tegelikult üsna sisuline koht, kus Isabelle kinni on jäänud. Tegelikult oleksime pidanud midagi taolist induktsiooniga tõestama ja siis saame seda oma põhitulemuses kasutada:

lemma sigval_sum: "sum_list (sigvals' e (-1)) = - eval e"
apply (induction e)
apply auto
done

theorem "sum_list (sigvals e) = eval e"
apply (auto simp: sigval_sum)
done

See ka ei tööta, sest meil on ikkagi paralleelselt vaja induktsiooniga tõestada võrdused nii positiivse kui ka negatiivse argumendi korral. Pane kokku õige sigval_sum lemma, et teoreem läbi läheks. Konjunktsiooni kirjutamiseks võib toksida järjest /\ ja see teisendatakse õigeks märgiks. Lahenduse vaatamiseks vajuta siia:

sum_list (sigvals' e 1) = eval e ∧ sum_list (sigvals' e (-1)) = - eval e

Kui oled sellega hakkama saanud, siis proovi oma koodis sisse viia mõned vead, näiteks „unustame“ mõnes definitsioonis Neg harus miinusmärgi. Kas Isabelle saab aru, et kood on vigane?

Ülesandeid iseseisvaks lahendamiseks

Edasi on siis kaks ülesannet, mida võiks analoogia põhjal saada iseseisvalt lahendada. Need on lihtsad tõestused ja rohkem Isabelle-i süntaksit ei tohiks vaja minna, kui siin lehel kirjas on. Kuna aga kasutame siin automatiseeritud tõestamistaktikad, võib asi raskeks minna, kui kasutad (samaväärseid), aga erineva kujuga valemid kui need, millega mina katsetasin. Seega kui asi hakkab väga keeruliseks minema, on mõistlik abi küsida.

1. Sigval korrektsus

Isabelle kontrollib ainult, et meie tõestus on korrektne, aga kas teoreem ise on ka õige asi? Ta ei ole nüüd otseselt vale, aga nagu ka järjestamisel on see, et kui nõuad ainult, et järjestus algoritmi tulemus oleks järjestatud list, siis võib tagastada tühja listi ka. Teine nõue järjestamise puhul on see, et tulemus peaks sisaldama kõik sisendis ette antud elemente! Meil on siin ka samamoodi. Jääb tõestada: List.map abs (vals x) = List.map abs (sigvals x).

2. Eituste elimineerimine

Java ülesandes oli meil ka meetod elimNeg. Selle jaoks on kõik üsna analoogiline nagu oli sigval puhul. Defineeri järgmine funktsioon ja tõesta tema kohta vastav teoreem!

fun elim_neg :: "exp ⇒ exp" 
theorem "vals (elim_neg x) = sigvals x"

Esitamine

Kood tuleb esitada Moodle'isse, aga lisaks võiks oma lahendust ka Vesalile selgitada ja oma kogemustest rääkida.

  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Tartu Ülikooli arvutiteaduse instituudi kursuste läbiviimist toetavad järgmised programmid:
euroopa sotsiaalfondi logo