Semantiek en Correctheid

Werkvormen

  • 16 uur hoorcollege
  • 16 uur responsie-college
  • 52 uur zelfstudie

Toelichting werkvormen

Deze cursus is taakgestuurd opgezet. Je volgt een wekelijkse cyclus van oriëntatie (hoorcollege), zelfstudie (leertaak) en nabespreking (responsiecollege). Elke leertaak heeft een vaste structuur, waarin bijvoorbeeld precies de leerdoelen en de op te leveren producten zijn gespecificeerd. Zo kun je ook (als je dat wilt) het cursusmateriaal zelfstandig en doelgericht doorwerken.

Vereiste voorkennis

Je hebt programmeerervaring met imperatieve programmeertalen. Verder kun je:

  • de taal van de predicatenlogica gebruiken om beweringen te formuleren; in redeneringen de elementaire stappen onderscheiden en bewijzen weergeven in een geschikt afleidingssysteem;
  • (programmeer)talen en taaluitbreidingen specificeren met behulp van reguliere expressies en contextvrije grammatica's;
  • helder formuleren, zowel bij het motiveren van oplossingen als het weergeven van wiskundige redeneringen.

Deze voorkennis kun je opbouwen via de cursussen rond programmeren en de cursussen Talen en automaten, Berekenbaarheid, Beweren en bewijzen.

Leerdoelen

Na afloop van deze cursus kunnen de deelnemers:

  • Betekenis van imperatieve taalconstructies vastleggen met behulp van inductieve technieken zoals toestandsovergangssystemen. Het effect van verschillende ontwerpkeuzen verklaren. Berekeningen in imperatieve talen analyseren, bijvoorbeeld terminatiegedrag en semantische equivalentie.
  • Eigenschappen van programma's aantonen met behulp van correctheidscalculi.

Inleiding

In deze cursus leer je formalismen om de betekenis (operationele semantiek) van programmeertalen nauwkeurig vast te leggen. Deze technieken worden toegepast bij het ontwerpen van programmeertalen en het toevoegen van nieuwe taalconstructies. Verder komen ze van pas bij het analyseren van het gedrag van programma's.
Als informaticus zul je formele methoden niet alleen toepassen, maar ook zelf formalismen moeten beoordelen, uitbreiden of ontwikkelen. Daarom gaat deze cursus ook over de eigenschappen van de formele systemen zelf: de metatheorie.

Onderwerpen

  • Semantiek van imperatieve talen en constructies: expressie-evaluatie, natuurlijke semantiek, structurele operationele semantiek, scope, recursie, procedure-evaluatie, semantische equivalentie
  • Correctheid van programma's: axiomatische semantiek, specificaties, Floyd-Hoare calculus

Toetsvorm

Het vak wordt afgesloten met een schriftelijk tentamen.

Literatuur

Al het materiaal is als PDF beschikbaar via de website van het vak. De belangrijkste bron is het boek 'Semantics with Applications' van Nielson en Nielson.

Website


Vakcode
NWI-IBC026
Studiepunten
3 ec
Periode
derde kwartaal
Collegerooster opvragen
SWS / PersoonlijkRooster

Docenten

Opgenomen in

  • Bachelor Informatica