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.