blob: f308ee05927ee329e8dbf36005bb0e8152a41aee (
plain) (
blame)
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
|
% 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.
|
