I00163 (I00163)
Semantiek en Logica 1 (schakelcursus)*
< 2006/2007 > 05-02-2007 t/m 10-07-2007 () L
Informatica - Master na HBO Artificial Intelligence variant MT (2004) Schakelcursussen (3 ec)
Informatica - Master na HBO Artificial Intelligence variant O (2004) Schakelcursussen (3 ec)
Informatica - Master na HBO Computer Security variant MT (2003) Schakelcursussen (3 ec) (3 ec)
Informatica - Master na HBO Computer Security variant O (2004) Schakelcursussen (3 ec) (3 ec)
Informatica - Master na HBO Embedded Systems variant MT (2003) Schakelcursussen (3 ec)
Informatica - Master na HBO Embedded Systems variant O (2004) Schakelcursussen (3 ec)
Informatica - Master na HBO Information Systems variant MT (2003) Schakelcursussen (3 ec)
Informatica - Master na HBO Information Systems variant O (2004) Schakelcursussen (3 ec)
Informatica - Master na HBO Software Construction variant MT (2003) Schakelcursussen (3 ec)
Informatica - Master na HBO Software Construction variant O (2004) Schakelcursussen (3 ec)
omvang
3 ec (84 uur) (3sp) : 18 uur plenair college, 18 uur groepsgewijs college, 0 uur computerpracticum, 0 uur 'droog' practicum, 0 uur gesprekken met de docent, 0 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 48 uur zelfstudie
investering
3 ec * 0 u/ec + #std * (1 + 3ec * 0.35 u/student/ec)
Dit is de eerste helft van I00090.

docent
afdeling
tijdbesteding

dr. Engelbert Hubbers
dis
15u.

speciale web-site
http://www.cs.ru.nl/~spitters/onderwijs/sl1/

 

In deze cursus leer je formele methoden ontwikkelen en gebruiken in de informatica.

We bekijken 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.

Verder leer je om beweringen en redeneringen te analyseren. We gebruiken propositie- en predicatenlogica als formalisme en onderzoeken afleidingen in natuurlijke deductie.

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.

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 met behulp van de semantiekbeschrijving. Berekeningen in imperatieve talen analyseren, bijvoorbeeld terminatiegedrag.
  • Afleidingen voor propositie- en predicaatlogica opstellen in natuurlijke-deductiestijl. Constructieve en (essentieel) niet-constructieve constructies onderscheiden.
  • De relatie tussen syntaxis (taal) en semantiek (model) aanduiden. Enkele veelgebruikte modeltheoretische eigenschappen onderzoeken en hun onderlinge verbanden verklaren.
  • Eigenschappen van programma's (waaronder correctheid) aantonen met behulp van correctheidscalculi.
  • Berekeningen in functionele talen modelleren met behulp van termherschrijfsystemen. Berekeningen in herschrijfsystemen analyseren, bijvoorbeeld confluentie- en terminatiegedrag.

Onderwerpen

a

  • Semantiek van imperatieve talen en constructies: expressie-evaluatie, natuurlijke semantiek, semantische equivalentie
  • Correctheid van programma's: axiomatische semantiek, specificaties, Floyd-Hoare calculus
  • Semantiek van functionele talen en constructies: termherschrijven, reductie, normalisatie, confluentie

Werkvormen

Taakgestuurd onderwijs, met een cyclus van oriƫntatie (hoorcolleges), zelfstudie (leertaken) en nabespreking (responsiecolleges).

Voor communicatie (mededelingen, e-mail, beoordelingen) gebruiken we Blackboard.

Vereiste voorkennis

  • Programmeerervaring met zowel imperatieve als functionele talen (zoals in de cursussen rond programmeren, eventueel parallel te volgen).
  • De taal van de predicatenlogica kunnen gebruiken om beweringen te formuleren. In redeneringen de elementaire stappen kunnen onderscheiden en bewijzen kunnen weergeven in een geschikt afleidingssysteem (zoals in de cursussen Beweren en bewijzen en Discrete wiskunde).
  • (Programmeer)talen en taaluitbreidingen kunnen specificeren met behulp van reguliere expressies en contextvrije grammatica's (zoals in de cursus Talen en automaten).
  • Helder kunnen formuleren, zowel bij het motiveren van oplossingen als het weergeven van wiskundige redeneringen (zoals in de voorafgaande cursussen in de wiskunde en de theoretische informatica).

Tentaminering

De beoordeling is gebaseerd op drie resultaten:

  • een deeltentamen over het onderdeel semantiek van imperatieve talen,
  • een deeltentamen over de onderdelen programmacorrectheid en
  • een deeltentamen over het onderdeel termherschrijven.

Als je voor hooguit één van de deeltentamens een beoordeling lager dan 5 hebt, is het eindcijfer voor Semantiek en Logica het gewogen gemiddelde van de vier resultaten (ze tellen mee voor respectievelijk 33%, 33%, 33%). In andere gevallen is het eindcijfer het laagste van de drie.

Combinatiemogelijkheden

In veel informaticagebieden wordt gewerkt met een of ander formalisme (bijvoorbeeld specificatietalen, programmeertalen, grafische talen, HTML). Explicietere koppelingen zijn aan te wijzen met Vertalerbouw (correctheid van vertalingen), Semantiek, Betrouwbaarheid van softwaresystemen (statische analyse via semantische technieken), Protocolvalidatie.

Literatuur

Boeken

  • Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (via internet)

Diversen

  • Dictaat en opgavenbundel Termherschrijfsystemen (verschijnt nog)


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 23 begonnen, 22 echt meegedaan, 4 geslaagd met 1e kans, 10 geslaagd totaal
Q: