diff options
| -rw-r--r-- | summ.tex | 25 | ||||
| -rw-r--r-- | werkstuk.tex | 1 |
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 |