Requirements Specification Research & Practice: Algebraic Specification

THIS PAGE IS UNDER FREQUENT UPDATE:
Please click RELOAD to make sure you have the latest version!

Dr. Chrystopher L. Nehaniv
office location: E361 (Research Hut)

This part of the course involves four weeks with lectures and labwork plus additional preliminary reading and a final week of directed study. It is concerned with formal specification and rigorous verification (mathematical proof) of the correctness of specifications. We will use the approach of algebraic denotational semantics and the OBJ3 system as a tool. OBJ3 is an executable specification language that uses equational logic as a foundation. Equational logic is the logic of substituting equals for equals. We will master the relevant background in general algebra needed to specify a simple imperative programming language and to learn how to prove properties of programs with computer assistance by doing exercises and examples.

Continuous assessment (frequent homework exercises, rather than exams) will be used to assess student performance in this part of the course. The coursework from this part of the course comprises 40% of the coursework mark (equivalent to 20% of the overall mark for the course.)

Text: Algebraic Semantics of Imperative Programming Languages by Joseph A. Goguen and Grant Malcolm, MIT Press, 1996.
ISBN 0-262-07172-X.

A copy of this book is be on reserve at the LRC. The LRC also has several additional copies. We will cover the first five chapters (plus chapter 0), which students are required to read, understand, and apply. (The sooner you start the better!)

Currently OBJ3 is available via telnet to blink.cs.herts.ac.uk and other linux machines in the Computer Science Department, where your normal student directory should be available. To use it : telnet blink, and type ``obj'' on the command line. You may find it helpful to refer to the OBJ3 Survival Guide.

If you are unable to log into the linux machines or blink, see the technical support staff. Even if you are away, you can use OBJ via telnet, e.g. telnet blink.cs.herts.ac.uk.

Syllabus : Readings and Homework

Assigned readings should be done by the beginning of the following class meeting. That is, reading assigned this week should be done before Thursday the following. The material requires time and thought to absorb and will be essential to completing the coursework.

Turn in the two courseworks at computer science reception. You should turn in your input and output, plus any written commentary that you feel is appropriate.

Weekly readings and the assigments due 30 November 2000 (12 noon) and 14 December 2000 (3 pm) are posted here:

8 November 2000 (Thursday)

Read pp. 1-9, Chapter 0 (Introduction) of Algebraic Semantics.

Read pp. 11-29 from Chapter 1 (Background in General Algebra and OBJ) of Algebraic Semantics, and the associated notes.
[Note that Chapter 1 is fundamental and is the most difficult chapter in the book. Much of what you read now will become clearer later on. Don't panic! Everyone finds this material challenging when first exposed to it. ]

16 November 2000 (Thursday)

Read pp. 30-50 from Chapter 1 of Algebraic Semantics; be sure to read the exercises.

Read pp. 51-65, Chapter 2 (Stores, Variables, Values, and Assignment) of Algebraic Semantics.

Do Exercise 1, pp. 43-46 of Algebraic Semantics; hand in your input and output.
Do Exericse 2, pp. pp. 46-48 of Algebraic Semantics using OBJ
Do Exericse 3, pp. pp. 48-50 of Algebraic Semantics

23 November 1999 (Thursday)

Read pp. 67-78, Chapter 3 (Composition and Conditionals) of Algebraic Semantics.

Do Exercise 4, p. 64 of Algebraic Semantics.
Do Exercise 5, p. 64 of Algebraic Semantics.
Do Exercise 6, p.64 of Algebraic Semantics.
Do Exercise 8, p. 64-65 of Algebraic Semantics.
Do Exercise 9, p. 65 of Algebraic Semantics.
Do Exercise 10, p. 65 of Algebraic Semantics.

[Each part of exercises 1-3 is worth 5 marks. E.g. exercise 3 has three parts and so is worth a total of 15 marks. Exercise 8 is worth 5 marks, the remaining exercises (4-6,9,10) listed above are worth 10 marks each. Maximum possible marks: 100 .
I accidentally listed exercise 7 instead of exercise 6 on the assignment briefing sheet. Therefore you can do either of exercise 6 or 7, whichever one you prefer.

All exercises listed above this line are due 30 November 2000 (Thursday) at 12 noon, turn in at Computer Science Reception)

30 November 1999 (Thursday)

Read pp. 79-89, Chapter 4 (Proving Program Correctness) of Algebraic Semantics.

Read pp. 91-108, Chapter 5 (Iteration) of Algebraic Semantics.
Do Exercise 11, p.76 of Algebraic Semantics using OBJ.
Do Exercise 12, pp.76-77 of Algebraic Semantics using OBJ.
Do Exercise 13, p.77 of Algebraic Semantics using OBJ.
Do Exercise 14, pp. 77-78 of Algebraic Semantics using OBJ.
Do Exercise 17, p. 88 of Algebraic Semantics using OBJ.

7 December 2000 (Thursday)

Read Formality and Informality in Requirements Engineering, in Proceedings, Fourth International Conference on Requirements Engineering (IEEE Computer Society, April 1996) pages 102-108 (keynote address by Joseph Goguen). [gzipped postscript] [postscript]. This paper gives an overview of work in requirements capture and analysis, and addressing the appropriateness or inappropriateness of formal methods in particular contents.
Do Exercise 19, p. 89 of Algebraic Semantics using OBJ.
Do Exercise 20, p. 89 of Algebraic Semantics using OBJ.

Do Exercise 22, pp. 105-106 of Chapter 5 using OBJ.

Do Exercise 23, p. 106 of Chapter 5 using OBJ.

Do Exercise 27, p. 108 of Chapter 5 (you may find it helpful to refer to the article of assigned reading.)

[Exercises 11, 12, 13, 14, 17, 19, 20, 22, 23 and 27 are worth 10 marks each.
Maximum possible marks: 100]

The remaining exercises, listed above this line, are due 14 December (Thursday) at 3 pm, turn in at Computer Science Reception).

Some slides from lectures (postscript):

[slides0.ps]: intro, 6 pp.
[slides1.ps]: Early Material from Chapter 1 (mostly from sections 1-3): pp. 1-20
Getting Started with OBJ: p. 20
description of example correctness proof: p. 21
This refers to the small example program verification (see link at bottom of the page) which I handed out and went through in lecture. Stay tuned for notes on the loop invariant in the example proof.
[slides2l.ps]: Some material from chapter 2 and [slides2p.ps], three additional portrait format slides: insert first one as third page in the set slides2l.ps;
2nd and 3rd slides give details of lab practice with proofs using OBJ (Corrected!!) for 23 November 2000.
There are no slides for rest of short chapters 2 & 3, since slides in class were very similiar to the text. Refer to your copy of Algebraic Semantics. Similarly, chapter 4 and 5 slides are very close to the text.

The OBJ3 Manual is available online [postscript] [gnuzipped postscript]; the OBJ3 specs for the integers (ZZ) are at obj/ZZ.html. A small example program verification (discussed in class on 16 November) is here: example.obj. By popular demand, An OBJ3 Survival Guide is now available. If you have a linux machine not running OBJ3, you can download the OBJ3 binary for it here [gnuzipped].

This page is at http://homepages.feis.herts.ac.uk/~nehaniv/RSRP/algspec.html.