Plans

Latest update: February 19, 2010

Below the dates, topics and material covered in each of the lectures and problem sessions are listed. Be aware that the information is tentative and might change.

In the tables below, numbers in the Material column generally refer to chapters and sections in the book The RAISE Specification Language. In addition the following shorthands are used:

AS = Mandatory assignment.
LM = Lecture Notes on the RAISE Development Method.
OHi = Copies of overheads set no. i.
Ex and Ex.y = Exercises, from Formal Software Specification using RAISE: Exercises, where x is the number and y the part of the exercise.
EXyy = Examination questions, from the exercise collection, where yy is the year.

1. Friday 5/2:

Time	Activity	Topics	Material
8:15 - 10:45	Lecture	Introduction to course. Introduction to RAISE. Logic.	1, 2, 3, OH0, OH1, 4, OH2
11:00 - 12:00	E databar	Install the RAISE tools under Linux in the E-bar: follow step 3 in the installation guide	DTU Linux installation guide
11:00 - 12:00	E databar	Test installation: create, type check and print COUNTER	DTU user guide sections 3-5
11:00 - 12:00	E databar / PC	Test installation: translate and execute X as described in sec. 6.4	DTU user guide section 6

2. Friday 12/2:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Products. Functions. Sets.	5, 6, 7.1-7.11, 8 OH3, OH4, OH5
8:15-10:00	Lecture	Test cases.	DTU user guide
10:00-11:15	Problem session	Logic. Products. Functions. Sets.	E2.3-5, E3.1-2, E4.1-2, E4.10, E5.1
11:15-12:00	E databar / PC	type check your solutions to E3.1-2

3. Friday 19/2:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Lists. Maps	9,10, OH6, OH7
10:00-12:00	Problem session	Sets. Lists.	E19.2, E6.5, E6.1b, E6.2

4. Friday 26/2:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Subtypes.	11, OH8
8:15-10:00	Lecture	Model-oriented specification	E9.4, OH9:p.1-7,15-21
10:00-12:00	Problem session	Maps. Subtypes. Model-oriented specification.	E7.1, E8.1-2, Ex98.1

5. Friday 5/3 (by guest lecturer Morten Lindegaard):

Time	Activity	Topics	Material
8:15-10:00	Lecture	Model-oriented specification.	E9.3, OH9:p.8-14
8:15-10:00	Lecture	Algebraic specification. Variants.	7.12-7.14, 34.6, 12, OH10
10:00-12:00	Problem session	Variants (enumerations).	E10.5, EX92.2
10:00-12:00	Problem session	Questions to mandatory assignment 1.	See Assignment on CampusNet

Mandatory assignment number 1 must be handed in not later than 18 March.

6. Friday 12/3:

Today you must come for the lecture 11.00-12:00 about Tools for VDM in Industry that will be given by Professor Peter Gorm Larsen from IHA in Århus. It takes place in the same rooom as the problem session.

Time	Activity	Topics	Material
8:15-10:00	Lecture	Variants. Unions and short records.	OH10, 15, OH11
8:15-10:00	Lecture	Underspec/non-determinism.	16, OH12
8:15-10:00	Lecture	Case and let expressions.	13, 14, OH12
	Self study	Overloading.	17, OH12
10:00-11:00	Problem session	Questions to mandatory assignment 1.	See Assignment on CampusNet
10:00-11:00	Problem session	Variants, unions & records	E10.2-3, E10.7, E12.1
10:00-11:00	Problem session	Case and let expressions.	E11.1-2.
11:00-12:00	Lecture	Tools for VDM in Industry	-

In the lecture today, I will complete the stuff about variants and give only a summary of sections 13-17 emphasizing what is important and difficult. Then, in next lecture, I will present an important application area - how to model language based systems using the language constructs you have just learnt.

7. Friday 19/3:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Language specification.	OH16
10:00-12:00	Problem session	Language specification.	E18.1, OH16 page 26 (COMPILER.rsl)
10:00-12:00	Problem session	Model-oriented specification	EX99.1

8. Friday 26/3:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Imperative specification.	18 - 20, 23, OH13
8:15-10:00	Lecture	Structuring mechanisms	28 - 30.6, 31, OH14
10:00-12:00	Problem session	Imperative specification.	E13.2-3, E13.5, EX92.1
10:00-12:00	Problem session	Structuring	E15.1(a)-(b)

Holiday. Friday 2/4.

9. Friday 9/4:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Method, part 1	LM, OH15
10:00-12:00	Problem session	Refinement	E16.1-3, E17.1-2
10:00-12:00	Problem session	Verification	E17.3

10. Friday 16/4:

Time	Activity	Topics	Material
8:15-10:00	Lecture	Method, part 2 (case study)	LM, OH15
8:15-10:00	Lecture	A railway formal methods project
8:15-10:00	Lecture	Introduction to mandatory assignment 2
10:00-12:00	Problem session	Specification of safety-critical systems	EX98.3, EX99.3

You must come today. During the lecture you will be introduced to the assignment.

11. Friday 23/4:

Time	Activity	Topics	Material
10:00-11:00	Question time	Mandatory assignment 2	AS

Takes place in the usual exercise room (which is reserved for you from 8:00-12:00).

In order to be sure to complete the assignment in time, our advice is that you prepare you well and start on the assignment before the question hours so that you can ask questions if you are in doubt about the assignment text or any practical matters.

Holiday (St. Bededag). Friday 30/4.

12. Friday 7/5:

Time	Activity	Topics	Material
10:00-11:00	Question time	Mandatory assignment 2	AS

Holiday. Friday 14/5.

13. Tuesday 11/5:

Time	Activity	Topics	Material
10:00-11:00	Question time	Mandatory assignment 2	AS

Mandatory assignment number 2 must be handed in NOT LATER THAN May 14th at 12 a.m. More details about that later on.