Formele Methoden

A. Eliëns
studiegids , Programma

Literatuur

Rooster

di 12.45-14.30, S203, 6-12, 15-18, 20-22

Opmerkingen

College

Het college Formele Methoden beoogt een inleiding te geven in het gebruik van formele technieken voor het specificeren van complexe software-systemen. In het college zal de nadruk liggen op model-gebaseerde specificaties waarmee data types met interne toestand beschreven kunnen worden. Uitgangspunt voor het college is de specificatie taal Z. Het college omvat een introductie in het gebruik van Z en de bijbehorende bibliotheek van specificatie schema's waaronder de standaard mathematische toolkit van Z. Tevens zullen een aantal case-studies behandeld worden. De nadruk zal daarbij liggen op de rol die een formele specificatie speelt als leidraad voor ontwerp-beslissingen. Ruime aandacht zal ook besteed worden aan het redeneren over en het bewijzen van eigenschappen van specificaties. Een belangrijk instrument daarbij is de refinement-calculus voor schema specificaties. Ook zal ingegaan worden op Object-Z . In / -lome/eliens/dv/hush/tutorial/Z staan voorbeelden.

Opdracht

De beoordeling omvat behalve een tentamen ook een opdracht . Voor de opdracht is er een harde deadline: de opdracht moet tenminste een week voor het tentamen ingeleverd zijn.

Meer informatie wordt op het college gegeven.

Voordrachten

Het is niet verplicht maar wel wenselijk dat studenten een (gedeelte) van een voordracht verzorgen waarin een toepassing van Z besproken wordt.

Een voordracht bestaat uit 

(1) een probleemstelling, 
(2) een beschrijving van de opzet van de specificatie,
(3) de illustratie van een paar technische hoogtepunten, en
(4) een evaluatie.

Oude tentamens

Typechecker voor Z en Object-Z

Zie (Unix) Wizard for Z.

Overig materiaal