| |
Na afloop van deze cursus kunnen de deelnemers:
- De betekenis van imperatieve taalconstructies vastleggen met behulp van inductieve technieken.
- 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.
|
| 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. |
|
|
|
 • 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 |
| Het vak wordt afgesloten met een schriftelijk tentamen. |
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. |
| http://www.cs.ru.nl/~hubbers/courses/sc |
We gebruiken een boek en een dictaat:
• Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999
• Engelbert Hubbers: Annotated Programs, een alternatieve notatie voor correctheidsbewijzen
Beide zijn als PDF beschikbaar. |
• 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). Deze nabespreking is alleen toegankelijk voor studenten die serieus hebben geprobeerd de leertaak te maken. Elke leertaak heeft een vaste structuur, waarin bijvoorbeeld precies de leerdoelen en de op te leveren producten zijn gespecificeerd. Het is niet verplicht om naar de colleges te komen, maar het feedbackmoment is het responsiecollege, dus ga daar zoveel mogelijk naar toe. |
| | Verplicht materiaalBoek| Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999. Het boek is gratis beschikbaar als PDF. |
| Dictaat| Engelbert Hubbers: Annotated Programs, een alternatieve notatie voor correctheidsbewijzen. Het dictaat is beschikbaar als PDF. |
|
|
WerkvormenCursus| Aanwezigheidsplicht | | Ja |
| Hoorcollege
| Responsiecollege
Voorbereiding bijeenkomstenDe bijbehorende leertaak dient serieus te zijn geprobeerd.
| Zelfstudie
|
|
ToetsenTentamen| Weging | | 1 |
| Gelegenheden | | Blok KW2, Blok KW4 |
|
|
| |