Introduction to formal specification

Introduction to Formal Specification

The info for the year 2011 course can be found here.

General information

The re-sit of the exam will be on 17.2.2011 and you should register (I do not know if that is possible yet) through the NettiOpsu web service.

Due to Eleni Berki's illness, there was no lecture on 13.12.2010. The planned lecture was based on two research papers. In the compensation (7th) exercises, there are also exercises based on these papers.

An online book about Z notation - it is not exactly a reference manual and the structure of the book is not the same as how the lectures advanced, but at least it is something.

Introductory DisCo slides in pdf format.

DisCo Windows installation executable to be used on 32-bit Windows.

The Taxi example for DisCo. Save the file and unzip it to try out the example. It provides examples of several DisCo features.

The first part of the course follows the book by Magee and Kramer.

The course has weekly exercises, an exam, and a course work. The weekly exercises are compulsory, and it is compulsory to do 30% of the exercises. If you cannot attend the exercises sessions, discuss the situation with me.

The scoring goes as follows:

The exam gives a maximum of 24 points. You need to score at least roughly half of the points to pass.
The weekly exercises over 30% give you points: 40% gives 1, 50% gives you 2, ..., 90% gives you 6, which is the maximum.
The course work will be scored in the scale of 0 to 6.
The marking scale has not been decided yet, but 30 points is guaranteed to give you the full mark 5.

Weekly exercises

Weekly exercises will be published here. I try to get them done after the Friday's lectures are done, so they should be here some time between Friday and Sunday.

Bonus exercises to be submitted with the course work.
Sixth exercises to be solved for Friday 10.12.
Fourth exercises to be solved for Friday 26.11. and some solutions.
Fifth exercises to be solved for Friday 3.12. and some solutions.
Fourth exercises to be solved for Friday 26.11. and some solutions.
Third exercises to be solved for Friday 19.11. and some solutions.
Second exercises to be solved for Friday 12.11. and some solutions
First exercises to be solved for Friday 5.11. and some solutions

Coursework

For the minimum ECTS, you need to a coursework on specification, where specify some target system, which you should choose yourself. It is difficult to define exactly how large the specification should be, but it should be a "complete" although maybe a small system, definately larger than any of the exercises. If it appears too small, I will advice you to extend it. You should also do something to analyse the specification or behaviours admitted by your specification.

Submit your coursework by e-mail to jyrki . nummenmaa @ uta . fi - deadline is 9.1.2011. Include some explanation of what you have done, including what you have done to check your specification.

If you want full credits, then you need to do some kind of an implementation of your specification, which could follow the ideas in the book by Magee and Kramer, but it can be also completely independent of those ideas.

Coursework will be published here. I try to get them done after the Friday's lectures are done, so they should be here some time between Friday and Sunday.