I00090 (I00090)
Semantiek en logica 1*
< 2006/2007 > 05-02-2007 t/m 01-07-2007 () L
Informatica - Bachelor (2003) Software: Programmeren en algoritmiek (3 ec) (3 ec) Grondslagen (3 ec) (3 ec)
Informatica - Master na HBO Artificial Intelligence variant MT (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Artificial Intelligence variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Computer Security variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Computer Security variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Embedded Systems variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Embedded Systems variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Information Systems variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Information Systems variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Software Construction variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Software Construction variant O (2004) Schakelcursussen (6 ec)
omvang
6 ec (168 uur) : 36 uur plenair college, 36 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.), 96 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.35 u/student/ec)
inzet tentatief

examinator
afdeling
tijdbesteding

prof. dr. Erik Barendsen
sws
115u.

docent
afdeling
tijdbesteding

prof. dr. Herman Geuvers
sws
115u.

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. Met een variant van predicatenlogica is het mogelijk om tijdafhankelijke eigenschappen van systemen te specificeren en beredeneren. Je gebruikt computergereedschap (een proof tool) om die eigenschappen automatisch te verifiëren.

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.
  • Tijdafhankelijke eigenschappen van systemen uitdrukken in modale (temporele) logica. Deze eigenschappen toetsen met behulp van computergereedschap.

Onderwerpen

a

  • Semantiek van imperatieve talen en constructies: expressie-evaluatie, natuurlijke semantiek, semantische equivalentie
  • Propositie- en predicatenlogica: natuurlijke deductie, constructieve en klassieke redeneerwijzen, modellen, consistentie en volledigheid
  • Correctheid van programma's: axiomatische semantiek, specificaties, Floyd-Hoare calculus
  • Semantiek van functionele talen en constructies: termherschrijven, reductie, normalisatie, confluentie
  • Temporeel redeneren: modale en temporele logica, tijd-afhankelijke eigenschappen, model checking, proof tools.

Werkvormen

Taakgestuurd onderwijs, met een cyclus van oriƫntatie (hoorcolleges), zelfstudie (leertaken) en nabespreking (responsiecolleges). Werkstuk aan de hand van een case study.

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 vijf resultaten:

  • een deeltentamen over het onderdeel semantiek van imperatieve talen,
  • een deeltentamen over programmacorrectheid,
  • een deeltentamen over propositie- en predicatenlogica,
  • een deeltentamen over het onderdeel termherschrijven,
  • het werkstuk over systeemverificatie.

Als je voor hooguit één van de deeltentamens een beoordeling lager dan 5 hebt en bovendien voor het werkstuk minstens een 6 hebt behaald, is het eindcijfer voor Semantiek en Logica het gewogen gemiddelde van de vijf resultaten (ze tellen mee voor respectievelijk 20%, 20%, 20%, 20%, 20%). In andere gevallen is het eindcijfer het laagste van de vijf.

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)
  • J.F.A.K. van Benthem, H.P. van Ditmarsch, J. Ketting, J.S. Lodder en W.P.M. Meyer-Viol: Logica voor informatica, derde editie, Pearson Education, 2003, ISBN 90-430-0722-6.
    (Dit boek wordt ook in de cursus Beweren en Bewijzen gebruikt.)

Diversen

  • Dictaat en opgavenbundel Termherschrijfsystemen (verschijnt nog)
  • Aanvullend materiaal over temporele logica: Michael Huth and Mark Ryan: Logic in Computer Science, second edition, Cambridge University Press, 2005, ISBN 0-521-54310-X. (Hoewel dit een interessant boek is, is het voor deze cursus niet nodig het boek aan te schaffen.)


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