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 tasemel. Kindlasti on puhas programmi disain väga oluline samm headuse poole, sest halba tegemise tõenäosus on oluliselt vähem. Kuidas saaks aga olla kindel, et programm ikkagi midagi halba ei tee?
Üks võimalus on kasutada selline keskkond, 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 seda siis endale paigaldada. Tegemist on iseseisva Java rakendusega, mille paigaldamine peaks üsna lihtne olema. Esimesel käivitamisel ehitab ta valmis oma standardteeki, mis võtab üsna palju aega!
Eeldused
Selle ülesanne lahendamiseks pead olema valmis endale funktsionaalprogrammeerimise mõned põhitõdesid väga põgusa sissejuhatuse põhjal endale selgeks tegema: valguse tee ei ole lihtne tee.
Teiseks on vaja kõigepealt lahendada ExprTransformer.java ülesandeid. Kui meetod elimNeg on Javas lahendatud, siis saame nüüd 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 seda selliseks, kus kõik miinusmärgid on ainult lehtedes.
Programmi mall
Kõigepealt tuleks siis luua endale uus fail nimega akt.thy ja selle sisse kirjutada meie avaldise andmestruktuuri:
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 ka mooduli nimi (theory akt) langema kokku faili nimega. Me defineerime siis oma exp tüüpi andmestruktuuri meie tuttavate variantidega. Avaldis on kas arvkonstant (Num), kahest avaldisest koosnes liitmine (Add) või avaldise vastand (Neg). Need konstruktorid 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 meetod eval. Siin tuleb lihtsalt täita lüngad (???). Me defineerime funktsioone kasutades loogikavõrdus, mida pannakse jutumärkidesse. See on väga veider asi Isabelle süntaksi juures, 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, siis saame avaldise väärtust küsida selle value käsuga. Selleks peab ka kursus viia sellele reale ja all output aknas peaks ilmuma ka tulemus. |
 |
Lehtedes esinevad arvud
Defineerime nüüd meetod, mis oli Transformer.java klassis nimega valueList, aga siin on tal lühem nimi, sest IDE automaatselt ei kirjuta nimed 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 singleton ja listi ühendamise süntaksit. Võid jälle proovida arvutada value "vals ex1", aga nüüd on Sinu kord implementeerida funktsiooni, mis oli Java harjutuses nimega signedValueList. See peaks tagastama väärtuste listi, kus on arvud "õigete" märkidega. Lihtsam on seda defineerida abifunktsiooni kaudu, mis võtab märk 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 me arvutame selle sigvals listi summa (kasutades Isabelle standardteeki funktsiooni sum_list), siis peaksime saama avaldise väärtust 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 output (või paremal state) vaadet. 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 on kinni 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 seda 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ärki. 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 Isabelli süntaks ei tohiks vaja minna kui siin lehel kirjas. Kuna aga kasutame siin automatiseeritud tõestamistaktikad, siis võib asi raskeks minna, kui kasutad (samaväärseid) aga erineva kujuga valemid kui need, millega mina katsetasin. Seega on parem abi küsida, kui asi hakkab minema väga keeruliseks.
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, sisi võib tagastada tühja listi ka. Teine nõua 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
Meil oli Java ülesandes ka meetod elimNeg. Selle jaoks on kõik üsna analoogiline nagu meil 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
Koodi tuleb esitada moodle'is, aga lisaks tuleb oma lahendust ka Vesalile loengu või praktikumi järel selgitada ja oma kogemustest rääkida.