%include intro.fmt

%% switch language to dutch
\selectlanguage{dutch}

\chapter*{Samenvatting}
\markboth{Samenvatting}{Samenvatting}
\addcontentsline{toc}{chapter}{Samenvatting}
\label{chapt.samenvatting}

Computers zijn niet meer uit onze maatschappij weg te denken.
Computerprogramma's worden steeds omvangrijker.
De keerzijde is dat deze programma's meer tijd kosten om te maken en
te testen, en bovendien ook meer fouten bevatten.
Helaas ervaren we regelmatig de consequenties ervan.
Autofabrikanten roepen bijvoorbeeld auto's terug
om een software-update door
te voeren, omdat door fouten in de programmering de auto's
op hol konden slaan.
Ook fouten in web-browsers worden door duistere figuren uitgebuit
om zogenaamde \emph{keyloggers}
op computers te installeren die toetsaanslagen afluisteren om
uiteindelijk bankrekeningen te plunderen.
Oplossingen voor dergelijke problemen kunnen deels in programmeertalen
gezocht worden.
Onderzoek naar programmeertalen helpt om zowel de onderhoudskosten
en de kwaliteit van software te verbeteren.

Met geavanceerde programmeertalen is het mogelijk om computerprogramma's
van hoge kwaliteit te maken. Daarvoor is een belangrijk stuk gereedschap van
belang: de \emph{compiler}. Een compiler zet een programma wat een programmeur
geschreven heeft om in machine-instructies die door de computer uitgevoerd
kunnen worden. Hoe geavanceerder de programmeertaal, hoe lastiger het is om
een compiler te maken.

Met attributengrammatica's kunnen compilers op een aantrekkelijke manier
gemaakt worden. Programmeertalen met ingewikkelde typesystemen zijn echter
lastig met attributengrammatica's te schrijven.
In dit proefschrift beschouwen we uitbreidingen om
attributengrammatica's ook voor het ontwikkelen van compilers voor
ingewikkelde programmeertalen in te kunnen zetten.

\paragraph{Programmeertalen en compilers.}
Een computerprogramma verwerkt gegevens die zich in het geheugen van
de computer bevinden. In een programmeertaal wordt deze verwerking
beschreven. Voor dergelijke beschrijvingen stelt een programmeertaal elementaire
verwerkingstaken ter beschikking. Tijdens de uitvoering van het programma
krijgt zo'n taak gegevens uit het geheugen van de computer als invoer en
laat het resultaten in het geheugen van de computer achter.
Bekeken vanaf een hoog niveau kunnen we zeggen dat programmeren het
samenstellen van verwerkingstaken is door de uitvoer en invoer van
verwerkingstaken aan elkaar te knopen.

Een programmeertaal biedt
abstractiemechanismen aan om dergelijke samenstellingen te beschrijven.
Programmeren is het opstellen van zo'n beschrijving: de \emph{broncode}.
Een \emph{compiler} vertaalt broncode naar instructies die door een
computer uitgevoerd kunnen worden: de \emph{machinecode}.
Een compiler handelt details af zoals hoe de invoer en uitvoer van
taken in het geheugen van de computer gerepresenteerd zijn.
In de broncode is het niet nodig om dergelijke details te specificeren, wat het gemak
om verwerkingstaken samen te stellen ten goede komt.

De mate waarin een programmeur een verwerkingstaak uit deeltaken kan samenstellen
is van grote invloed op de kwaliteit van een programma, en de tijd die het kost om
het programma te ontwikkelen en te onderhouden.
Wanneer de broncode overzichtelijk is, worden
er minder fouten gemaakt. Bovendien hoeft de broncode van een deeltaak maar een keer
geschreven te worden.
De mate waarin een programmeertaal abstractie van details toestaat speelt hierbij een
belangrijke rol.

Programmeertalen bieden vaak voor specifieke domeinen speciale abstractiemechanismen aan.
De taal SQL voor het raadplegen van
databases is hier een goed voorbeeld van. In SQL beschrijft men het combineren van informatie
uit tabellen, terwijl van de representatie van de gegevens in de tabellen en van de volgorde
van het combineren geabstraheerd wordt.
Idealiter richt de programmeur zich op het totaalplaatje, terwijl de compiler voor een
correcte invulling van de details zorgt, eventueel aan de hand van wat expliciete hints
die door de programmeur gegeven worden.
Met behulp van een relatie tussen broncode en
machine-instructies kan dit gedrag gespecificeerd worden.

Een programmeertaal stelt bovendien eisen aan de broncode. Bijvoorbeeld, in een samenstelling
van taken dient iedere taak een correct gestructureerde invoer te hebben.
Een \emph{type} is een beschrijving van de structuur van een waarde.
Ofwel, de invoer dient het juiste type te hebben.
De compiler controleert als onderdeel van het vertaalproces of de broncode inderdaad aan deze
eisen voldoet, en vormt dus een implementatie van het typesysteem.
Een \emph{statische semantiek} in de vorm van een \emph{type system} specificeert deze eisen
met een relatie tussen broncode en typen.
Het afdwingen van deze eisen voorkomt dat bepaalde (triviale) fouten tijdens de uitvoering van
het programma op kunnen treden.

Als onderdeel van het vertaalproces controleert de compiler of de broncode aan de eisen
voldoet door een \emph{bewijs} af te leiden dat de broncode relateert aan een type.
De machine-instructies worden verkregen door een bewijs af te leiden dat een relatie
legt met machine-instructies. Als dit niet lukt, dan
bevat het programma een \emph{statische fout} en is het programma ongeldig.
Relaties in een semantiek worden doorgaans met afleidingsregels gedefinieerd.
Het afleiden van zo'n bewijs wordt \emph{inferentie} of \emph{afleiden} genoemd.
De bewijzen hebben een boomstructuur waarin de toepassing van afleidingsregels zichtbaar is.

Vrijheid in het bepalen van het bewijs geeft de compiler de mogelijkheid om details in
te vullen. Echter, er bestaan harde theoretische grenzen aan wat voor bewijzen er
automatisch afgeleid kunnen worden. Door de taal ingewikkelder te maken, kan er op een
hoger niveau geredeneerd worden. Dan is het mogelijk
een programma duidelijker uit te drukken, zodat de broncode meer structuur heeft, en er
meer aannames zijn om het bewijs mee rond te krijgen.
Een direct gevolg is dat de compiler daardoor lastiger wordt om te maken.

\paragraph{Attributengrammatica's.}
Als initi\"{e}le stap ontleedt een compiler de
broncode aan de hand van de grammatica van de programmeertaal. Het resultaat is een
boomstructuur, de \emph{abstracte syntaxboom} (AST), dat een expliciete representatie is
van de compositionele structuur van de broncode.
Deze boomstructuur is geschikt voor syntax-gestuurde vertaling. In dit geval heeft een
semantiek een afleidingsregel voor ieder stukje syntax. De structuur van een bewijs komt
dan vrijwel overeen met de AST.

Een compiler is ook een computerprogramma, en worden in een programmeertaal geschreven.
Attributengrammatica's (AG's) zijn een domein-specifieke programmeertaal voor
het uitdrukken van eigenschappen van ASTs, en daarmee dus ook het afleiden van
bewijzen voor relaties van een syntax-gestuurde semantiek.
Een AG relateert attributen met elke knoop in de AST,
en specificeert functies die waarden van attributen berekenen aan de hand van waarden
van andere attributen van een knoop en kinderen van de knoop.
De attributen stellen eigenschappen van de broncode voor, en zijn aspecten of
\emph{getuigen} van het bewijs, zoals typen, lijsten van instructies en foutmeldingen.

De voordelen van AG's ten opzichte van algemene programmeertalen zijn dat
niet beschreven wordt \emph{hoe} de AST afgelopen wordt. Daardoor kunnen de
berekeningen van attributen in
afzondering beschreven worden, wat vele voordelen biedt in termen van hergebruik,
overzicht en documentatie. De samenstelling van deze berekeningen wordt automatisch
bepaald. Voor dit aanzienlijke voordeel is vereist dat het bewijs als
attributengrammatica uit te drukken is, wat het geval is wanneer de semantiek
\emph{syntax-gestuurd} is.

\paragraph{Inferentie.}
Voor programmeertalen met een complexe (statische) semantiek is de structuur van het
bewijs niet gelijk aan de AST. Tenslotte, om vrijheid in de invulling van het bewijs
te hebben, dienen delen van het bewijs van de broncode afleidbaar te zijn, maar niet door
de structuur ervan te worden bepaald.
Daarvoor bestaan een aantal gangbare algoritmen, zoals het berekenen van een dekpunt van
een stelsel van randvoorwaarden, en de gedeeltelijke verkenning van een bos van
kandidaat-deelbewijzen.
Deze algoritmen hebben als eigenschap dat de attributen wederzijds afhankelijk zijn van
\emph{tussentoestanden} van het bewijs. Om bijvoorbeeld een kandidaat te selecteren is het nodig
om eigenschappen ervan in te zien.
In een attributengrammatica zijn attributen gedefinieerd in termen van het uiteindelijke
bewijs, waardoor het lastig is om dergelijke algoritmen met een AG te beschrijven.

In dit proefschrift richten we ons op \emph{geordende} attributtengrammatica's, en breiden
deze uit met de mogelijkheid om tussentoestanden te inspecteren en te manipuleren.
In een geordende AG kan de berekening van de attributen als een eindige sequentie van
toestandsveranderingen beschreven worden. Deze beschrijving maakt het mogelijk om over
deelbewijzen in een gegeven toestand te redeneren, berekeningsstrategie\"{e}n te
specificeren, en attributen die in deze toestand beschikbaar zijn te inspecteren.
Daarvoor schrijven we geen AGs voor de abstracte syntax van de taal, maar AGs voor de
abstracte syntax van de bewijsregels van de semantiek.

\paragraph{Uitbreidingen.}
In hoofdstuk~\rref{chapt.side-effect} introduceren we notatie om een sequentie
van \emph{visits} voor een nonterminal te specificeren. Een visit is een eenheid van
evaluatie voor een knoop in de (bewijs)boom. Ieder attribuut is gerelateerd aan een
visit. De attributen van een vorige visit zijn beschikbaar in een opvolgende visit.
Bovendien kunnen berekeningen voor attributen aan specifieke visits toegekend worden
om af te dwingen dat berekeningen in een vaste volgorde plaatsvinden.
Deze uitbreiding maakt het mogelijk om monadische operaties met AGs te combineren.

In hoofdstuk~\rref{chapt.iterative} laten we zien hoe we berekeningsstrategie\"{e}n
aan visits koppelen. Door het voorwaardelijk herhalen van een visit aan een knoop
kan een dekpunt berekend worden. Met \emph{clauses} kunnen voorwaardelijke
berekeningen van attributen en kinderen van de knoop gespecificeerd worden, zodat
het mogelijk is om deelbewijzen te verkennen.
Ook kunnen knopen ontkoppeld worden en op een andere
locatie in de boom weer aangekoppeld worden, waarbij we statische garanties geven
over de toestand van dergelijke verplaatsbare knopen. Zo kunnen berekeningen die afhangen van
bewijzen die nog niet voltooid zijn uitgesteld worden tot deze bewijzen beschikbaar komen.
Hiermee kunnen we \emph{constraints} representeren.

In hoofdstuk~\rref{chapt.breadthfirst} gaan we een stapje verder dan visits.
Tussenresultaten die tijdens de uitvoering van een visit beschikbaar komen kunnen met
technieken uit dit hoofdstuk stapsgewijs ge\"{i}nspecteerd worden. Door om de beurt
kandidaat-knopen een stap te laten zetten, kunnen de bewijzen gelijktijdig verkend
worden, zonder de bewijzen van te voren al helemaal op te bouwen.

In hoodstuk~\rref{chapt.dependent-ags} presenteren we AGs met \emph{afhankelijke typen}.
Dit zijn AGs waarin het type van een attribuut mag verwijzen naar de waarden van
andere attributen. Deze uitbreiding maakt het mogelijk om invarianten op attributen
te specificeren en bewijzen ervoor uit te drukken.
Voor deze uitbreiding maken we gretig gebruik van de mogelijkheden die door
voorgaande hoofdstukken besproken zijn.

De uitbreiding vormen een conservatieve uitbreiding van AGs. De mate van abstractie,
zoals deze door AGs aangeboden wordt, blijft behouden.
De uitbreidingen maken het mogelijk om eigenschappen van de berekeningsvolgorde te
specificeren en te inspecteren, zonder daarbij het automatisch ordenen van
attribuutberekeningen te breken.
Met de uitbreidingen heeft de programmeur een stel krachtige bouwstenen in handen om
compilers mee te implementeren.


%% revert language back to english
\selectlanguage{english}