SamenvattingHEADmaster

2 files changed, 26 insertions, 0 deletions

diff --git a/summ.tex b/summ.tex
new file mode 100644
index 0000000..f308ee0
--- /dev/null
+++ b/summ.tex
@@ -0,0 +1,25 @@
+% vim: spelllang=nl:
+\section{Samenvatting}
+\label{sec:summ}
+
+We hebben de natuurlijke semantiek van Smurf nauwkeurig beschreven. Hierbij
+zijn we zo dicht mogelijk bij de specificatie~\cite{safalra} gebleven, ook al
+moesten we hier en daar andere keuzes maken of de specificatie nader
+specificeren.
+
+Vervolgens hebben we laten zien dat de structurele operationele semantiek van
+Smurf er niet erg zou verschillen van de natuurlijke semantiek, door een paar
+voorbeelden van regels te geven.
+
+We hebben laten zien dat semantiekregels zich makkelijk laten vertalen naar een
+implementatie van de taal, door een simpele interpreter voor Smurf,
+\emph{CleanSmurf} te beschrijven. We hebben dit programma uitgebreid zodat het
+ook afleidingsbomen kan genereren en als simpele bewijshulp kan dienen.
+
+Ten slotte hebben we het nut van de semantiek en de bewijshulp middels een
+case study duidelijk gemaakt. Met onze regels en de bewijshulp is een inductief
+bewijs over een Smurfprogramma vrij makkelijk te maken, ook al vergt het nog
+wel enige precisie.
+
+Onze specificatie, het voorbeeld van het bewijs met inductie en de bewijshulp
+kunnen Smurfontwikkelaars helpen bij hun werk.
diff --git a/werkstuk.tex b/werkstuk.tex
index b719ce9..9adde46 100644
--- a/werkstuk.tex
+++ b/werkstuk.tex
@@ -61,6 +61,7 @@
 \input{sosexamp}
 \input{cleansmurf}
 \input{analyse}
+\input{summ}
 \input{refs}
 
 \clearpage