CS424/824 - Software Specification and Development

2000 (full year) - 24 credit points

Subject Profile

Lecturing staff

	Room	Phone	E-mail: @csee.uq.edu.au	Subject coordinator
David Carrington	323	3365-3310	davec	semester 1
Roger Duke	324	3365-3335	rduke
Ian Hayes	326	3365-2386	ianh
Paul Strooper	305	3365-1628	pstroop	semester 2

Subject aims

The aim of this subject is to develop an ability to formally specify and refine a system towards implementation, and to use the formal specification as the basis for testing the implementation. Formality implies a mathematical basis so that specification and refinement statements are precise, unambiguous and supportive of formal reasoning as in mathematical theorem proving. Formally specified software is subjected to considerable analysis before the design process starts thereby resolving system issues or misunderstandings and removing errors at an early stage.

Assumed background

Prerequisites: Permission of Head of Department + (i) (CS160 or 162) + (CS161 or 164) + MT108 + #24 level 3 CS subjects or (ii) CS362

Because this subject concentrates on formal methods for software development, a reasonable level of mathematical maturity, especially with discrete mathematics, and a reasonable maturity in software engineering is assumed. The prerequisite knowledge required includes:

programming experience including control structures and recursive procedures,

familiarity with common data structures and representations used to implement them,

familiarity with proofs by mathematical induction, and

understanding of program assertions (preconditions, postconditions, invariants), loop variants, and how to reason that a program is correct using these.

Teaching Mode

Lectures: Wednesday 2-4 pm, Room 78-621 (General Purpose South)
Tutorial: Wednesday 4-5 pm, Room 78-621 (General Purpose South) - tutorials begin in the second week of semester.

Detailed syllabus

The subject is one fifth of a full-time honours work-load (20 credit points total, distributed as 10 hours commitment per week throughout the year). Weekly contact hours comprise two lectures and one tutorial per week.

The material in the first semester focuses on refinement of executable programs (code) from specifications. The correctness of programs has been of interest since the early days of computing, but it was only in the late 1960s that it became a research topic [2, 3].
Initially the emphasis was on proving that a given program met its specification, given in terms of a precondition and a postcondition, but it was soon recognised that a better approach is to develop the program and the proof on correctness hand-in-hand [4].

In the late 1970s, Ralph-Johan Back developed the first refinement calculus. The main innovation was the introduction of a specification command as part of a programming language. The specification command is not executable. However, it allows a specification to be considered as a program. The development of an executable program begins with a single specification command, and step-by-step refines, via intermediate programs that are combinations of specification commands and executable code, to a final program that is code. In semester 1, CS424/CS824 introduces the concept of refining abstract specifications into implementation code. It demonstrates the refinement calculus approach for both procedural and data refinement and provides students with experience using the refinement calculus and an appreciation of its capabilities.

The following summary is intended as a guide to the material covered in semester 1 and its relationship to the first semester text book [1].

Algorithm refinement [Chapters 1-10] The important new concepts are the specification command and the idea that one program refines another. Algorithm refinement covers the development of programs making use of specification commands as well as standard programming language constructs such as assignment, sequential composition, alternation (if), and iteration (do).

Procedures, parameters and recursion [Chapters 11-15] Procedures define named building blocks for programs. Every procedure has a specification, which programmers using the procedure make use of to determine the behaviour of the procedure, and an implementation, which is usually considerably more complex (and deterministic) than the specification. Of course, provided the implementation of the procedure satisfies (refines) the specification of the procedure the clients of the procedure will be satisfied.

Data refinement [Chapters 16-18] An important technique in developing larger programs is the use of modules that collect together data and operations on that data. As with procedures, we distinguish between the specification of a module, which typically specifies the behaviour of the module in terms of data abstractions (sets, relations, functions, etc.), and the implementation of a module, which must make use of those data structures available in the implementation language (arrays, etc.) or other modules. Data refinement is a technique used to justify the relation between the abstract specification of a module, and the concrete implementation of the module. It does this by relating the abstract and concrete data structures, and showing that the operations on the concrete structures of the implementation simulate those on the abstract structures of the specification.

Refinement methodologies and tools An overview of the currently available refinement methods and tools for supporting those methods.

The material in the second semester focuses on formal object-oriented specification and processes, and specification-based testing. The specification section reviews the logic and set theoretic bases used throughout specification and refinement. The object-oriented specification language Object-Z, an extension of the Z specification language, is covered in detail including several medium-scale case studies. This specification style is model oriented, focusing on states and transitions (operations) and includes a calculus for operation composition. Z provides a rich set of notations and constructs, is being progressively used in industry, and is currently undergoing international standardisation. The specification-based testing section uses formal specifications as a starting point for deriving test cases and oracles. Testing is a verification and validation activity that can be enhanced by using systematic approaches based on formal specifications.

Details of the Semester 2 program will be provided at the beginning of Semester 2.

Resources

Textbook (Semester 1)

[1]	Carroll Morgan. Programming from Specifications. Prentice Hall, second edition, 1994.
	This is an excellent introduction to this material and we will be following the book reasonably closely. Since it is already out of print, we have permission to supply students with a photocopy.

Reference material (Semester 1)

The papers by Floyd [2] and Hoare [3] are important historically, as is the the book by Dijkstra [4]. The basic ideas behind refinement were first developed by Ralph-Johan Back [5]. The version of the refinement calculus that we deal with was developed by Carroll Morgan and Ken Robinson [1, 6].

An early paper on data refinement is that by Hoare [7]. The Vienna Development Method (VDM) makes extensive use of data refinement [8]. A more recent development is the B method [9], due to Jean-Raymond Abrial, who was also primarily responsible for Z. B is a close relative of the refinement calculus. The text [10] for the subject CS362 will also be of some use.

[2] R. W. Floyd, Assigning meaning to programs, Mathematical Aspects of Computer Science, pp.19-32, 19, 1967

This paper is the starting point of research on reasoning about software. It is based on showing the correctness of programs represented as flowcharts. The paper is difficult to follow for the uninitiated.

[3] C. A. R. Hoare, An axiomatic approach to computer programming, Communications of the ACM, pp.576-580, 583, 12, 1969. PSE Per. QA76.A715.

This paper first introduced the axiomatic style of reasoning about programs written using structured programming constructs. It follows on from the pioneering work of R.W. Floyd [2] but is more readable and in a style closer to that used these days.

[4] E. W. Dijkstra, A Discipline of Programming, Prentice Hall, Englewood Cliffs, 1976 PSE QA76.6.D56.

This is a classic in the area by a pioneer in the field, it introduced the guarded command language and weakest preconditions, and the style of developing programs along side their proof of correctness.

[5] R.-J. Back and J. von Wright, Refinement calculus : A systematic introduction Springer, 1998. PSE QA76.6 .B28

[6] Carroll Morgan and Trevor Vickers, On the Refinement Calculus, Springer-Verlag, 1994. PSE QA76.6.O49.

This book contains a collection of research papers on the refinement calculus.

[7] C.A.R. Hoare, Proof of correctness of data representations, Acta Informatica, 1:271-281, 1972.

[8] C. B. Jones, Systematic Software Development using VDM, Second edition, Prentice Hall, 1990. PSE QA76.76.D47J66

This book deals with the Vienna Development Method (VDM). It is in a different style to that used in this subject but has an excellent treatment of specification and data refinement.

[9] Jean-Raymond Abrial, The B-Book: Assigning programs to meanings, Cambridge University Press, 1996.

[10] Anne Kaldewaij, Programming: The Derivation of Algorithms, Prentice Hall, 1990. PSE QA76.6.K3417.

The textbook used in the prerequisite subject CS362.

[11] D. Gries, The Science of Programming, Springer Verlag, 1981. PSE QA76.6.G747.

The first good introductory text in the area in a style similar to that used by Dijkstra [4].

[12] E. W. Dijkstra and W. H. J. Feijen, A Method of Programming, Addison Wesley, 1988. PSE QA76.6.D5513.

A good introductory text in a style similar to that used in Dijkstra [4].

[13] Eric C. R. Hehner, A practical theory of programming, Springer-Verlag, 1993 PSE QA76.6.H428.

Another good introductory text in a different style.

Reference material (Semester 2)

The following material is recommended reading for Semester 2.

Ben Potter, Jane Sinclair, and David Till. An Introduction to Formal Specification and Z. Prentice Hall International, London, 1991. PSE QA76.76.D47P68.
Jim Woodcock and Martin Loomes. Software Engineering Mathematics. Pitman, 1988. PSE QA76.758.W66. An alternative introduction to Z.
Ian Hayes, editor. Specification Case Studies. Prentice Hall International, 1987. Second edition 1993. PSE QA76.6.S667. A collection of specification case studies using Z.
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992. PSE QA76.73.Z2S665. An excellent reference book on the Z notation, but not an introduction to Z.
D.M. Hoffman and P.A. Strooper. ClassBench: A methodology and framework for automated class testing. Software Practice and Experience, 27(5):573-597, May 1997.
David Carrington, Ian MacColl, Jason McDonald, Leesa Murray, and Paul Strooper. From Object-Z specifications to ClassBench test suites. SVRC Technical Report SVRC-TR-98-22, October 1998.

Handouts

Detailed class notes, printed solutions to tutorials, and all assignments will be distributed in the lectures and tutorials.

Computer/Laboratory facilities

Access to computer terminals is available for preparation of assignment solutions.

Consultation availability

The lecturers will be available for consultation at prescribed times and locations.

Collection/distribution of submitted material

Assignments will be collected and returned during the lectures.

Expected student outcomes: criteria for assessment

Students are expected to gain an understanding of formal specification, and the role of formal specifications in further development and formal refinement, including the use of formal specifications in testing. They are expected to develop practical skills in formal specification, refinement and testing.

Assessment

The assessment for the subject in the first semester is based on three assignments (40%) and an end-of-semester examination (60%). The assignments must be handed in at the beginning of the lecture period in the week they are due. The assignments are used to assess the practical ability of the students on small to medium-sized problems. The examination is used to assess both the practical ability of the students on small problems and the understanding of the lecture material.

Details of assessment in Semester 2 will be provided at the beginning of Semester 2.

Grades

A grade of 7 will be awarded to students who demonstrate excellence in both the understanding of the lecture material and the practical work.

A grade of 6 will be awarded to students who demonstrate excellence in at least one of the two areas (understanding of lecture material and practical work) and perform soundly in the other.

A grade of 5 will be awarded to students who perform at least soundly in both areas.

A grade of 4 will be awarded to students who perform at least soundly in one area and perform at a basic level in the other.

Otherwise a failing grade will be awarded.

The meanings of the terms "excellence", "soundly", and "basic level" will be discussed for each assessment item, including the final examination.

[2]	R. W. Floyd, Assigning meaning to programs, Mathematical Aspects of Computer Science, pp.19-32, 19, 1967
	This paper is the starting point of research on reasoning about software. It is based on showing the correctness of programs represented as flowcharts. The paper is difficult to follow for the uninitiated.

[3]	C. A. R. Hoare, An axiomatic approach to computer programming, Communications of the ACM, pp.576-580, 583, 12, 1969. PSE Per. QA76.A715.
	This paper first introduced the axiomatic style of reasoning about programs written using structured programming constructs. It follows on from the pioneering work of R.W. Floyd [2] but is more readable and in a style closer to that used these days.

[4]	E. W. Dijkstra, A Discipline of Programming, Prentice Hall, Englewood Cliffs, 1976 PSE QA76.6.D56.
	This is a classic in the area by a pioneer in the field, it introduced the guarded command language and weakest preconditions, and the style of developing programs along side their proof of correctness.

[6]	Carroll Morgan and Trevor Vickers, On the Refinement Calculus, Springer-Verlag, 1994. PSE QA76.6.O49.
	This book contains a collection of research papers on the refinement calculus.

[8]	C. B. Jones, Systematic Software Development using VDM, Second edition, Prentice Hall, 1990. PSE QA76.76.D47J66
	This book deals with the Vienna Development Method (VDM). It is in a different style to that used in this subject but has an excellent treatment of specification and data refinement.

[10]	Anne Kaldewaij, Programming: The Derivation of Algorithms, Prentice Hall, 1990. PSE QA76.6.K3417.
	The textbook used in the prerequisite subject CS362.

[11]	D. Gries, The Science of Programming, Springer Verlag, 1981. PSE QA76.6.G747.
	The first good introductory text in the area in a style similar to that used by Dijkstra [4].

[12]	E. W. Dijkstra and W. H. J. Feijen, A Method of Programming, Addison Wesley, 1988. PSE QA76.6.D5513.
	A good introductory text in a style similar to that used in Dijkstra [4].

[13]	Eric C. R. Hehner, A practical theory of programming, Springer-Verlag, 1993 PSE QA76.6.H428.
	Another good introductory text in a different style.