1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
% vim: spelllang=nl:
\subsection{Hulp bij bewijzen}
\label{sec:cleansmurf:proofs}
Omdat aan de linkerkant van Smurftransities niet alleen het programma en de
toestand, maar ook de input staat, heeft een Smurfprogramma voor iedere input
een andere afleidingsboom. Deze afleidingsbomen zijn vervolgens met
\emph{CleanSmurf} te genereren. Vaak zullen we echter uitspraken willen doen
die abstraheren van de input, zoals ``Voor iedere input $s_1:s_2:\Nil$ zal de
output $s_2:\Nil$ zijn.'' Hier kan \emph{CleanSmurf} niet mee overweg, wat het
een weinig behulpzame toepassing voor bewijshulp maakt.
Een uitbreiding op \emph{CleanSmurf} implementeert een simplistische bewijshulp
die in sommige gevallen met variabelen overweg kan. Op dit moment is het een
\emph{proof of concept}. Sommige delen zijn nog niet geïmplementeerd. Wel is
het al bruikbaar in bepaalde gevallen, zoals we in \autoref{sec:analyse} zullen
zien. De bewijshulp is te vinden in de \texttt{prover} branch van
\emph{CleanSmurf}~\cite{cleansmurf}.
De oplossing hiervoor is complex. Waar hierboven de stack werd gemodelleerd met
een lijst van strings, zal dit nu niet meer voldoende zijn: we moeten
onderscheid maken tussen \emph{literals} en \emph{bewijsvariabelen}. Voor de
duidelijkheid maken we vanaf nu onderscheid tussen variabelen (elementen op de
stack of in de variable store) en bewijsvariabelen (variabelen waar de
bewijshulp mee werkt).
Combinaties van literals en bewijsvariabelen moeten ook voor kunnen komen (bv.
literal \lit{s} geconcateneerd met variabele $t$). Bovendien kunnen
bewijsvariabelen ook in een Smurfprogramma terechtkomen, omdat Smurf geen
duidelijk onderscheid kent tussen variabelen en Smurfprogramma's (middels
$\StmExec$ kan een variabele uitgevoerd worden). Dit laatste moet de bewijshulp
ten minste deels ondersteunen: variabelen komen al snel in programma's terecht
op het moment dat iteratie gewenst is. Zolang de variabele in een
$\StmPush$-commando wordt gebruikt kan de bewijshulp er mee omgaan.
Om variabelen te modelleren definiëren we een nieuw type, \CI{Expr}:
\lstinputlisting[firstline=15,lastline=20]{CleanSmurfProver/Smurf.dcl}
Vervolgens vervangen we \CI{String} door \CI{Expr} in de definities van
\CI{Stm}, \CI{Stack} en \CI{Store}.
Dit heeft gevolgen voor de \CI{step}-functie en zijn hulpfuncties. Waar we
eerst \CI{head} op een \CI{String} toepasten, doen we dat nu op een \CI{Expr}.
Deze functie moeten we dus herschrijven naar de onderstaande code. Soortgelijke
aanpassingen moeten we maken voor andere functies.
\lstinputlisting[firstline=272,lastline=277]{CleanSmurfProver/Smurf.icl}
Op deze manier kunnen we de head van een variabele nemen. Dit wordt, volgens
het laatste alternatief, opgeslagen als \CI{EHead (Var ..)}. Er wordt in dit
geval niet gecontroleerd of die variabele niet leeg is. Het is aan de gebruiker
van de bewijshulp dit na te gaan. In het bijzonder kunnen er dingen fout gaan
voor expressies als \CI{ECat (Var "s") (Lit "xyz")}: nemen we hier de head van,
dan zal dit worden opgeslagen als \CI{EHead (Var "s")}, terwijl dit \CI{Lit
"x"} zou moeten zijn als \CI{s} leeg is. Dit zijn dingen waar uiteindelijk wel
op te controleren valt, maar nog niet volledig geïmplementeerd zijn.
Helaas werkt de oude functie om een boom te maken, \CI{tree}, niet meer na deze
veranderingen: op een gegeven moment zal \CI{step} moeten weten wat de inhoud
van een bewijsvariabele is.
Om dit op te lossen introduceren we \emph{bewijshints}. Dit zijn transities
waarvan we de bewijshulp vertellen dat hij mag aannemen dat die bestaan. De
\CI{prover}, de bewijshulp-variant van \CI{tree}, zal bomen slechts maken tot
het punt dat zo'n bewijshint gevonden wordt. Het type van \CI{prover} is
hetzelfde als dat van \CI{tree}, behalve dat een extra argument is toegevoegd
voor de bewijshints:
\lstinputlisting[firstline=72,lastline=73]{CleanSmurfProver/Smurf.dcl}
Het eerste argument is een functie die voor een argument \CI{(pgm,i,st)} een
\CI{Just (i',o,st')} oplevert dan en slechts dan als de bewijshulp mag aannemen
dat er een afleidingsboom bestaat voor de transitie
$\trans\pgm\ip\st{\ip'}\op{\st'}$. Willen we geen bewijshints meegeven, dan
kunnen we hier simpelweg \CI{(\\_ -> Nothing)} voor invullen. De oude \CI{tree}
is dus te herdefiniëren als:
\lstinputlisting[firstline=74,lastline=74]{CleanSmurfProver/Smurf.dcl}
De bewijshulp kan afleidingsbomen in \TeX{} genereren. Hiervoor wordt
\texttt{prooftree.sty}~\cite{prooftree} gebruikt. Door een probleem in dit
package, dat niet herzien is sinds 1996, kan bij grote bomen \TeX{}'s
\emph{grouping limit} worden overschreven. Dit kan verholpen worden door
LuaLaTeX te gebruiken. Alle bomen in \autoref{sec:app:trees} zijn op deze
manier gegenereerd.
|
