CISC 223/3.0 Software Specifications
Original Authors: David Skillicorn and Bob Tennent
Last Revised: August 30, 2006
Introduction to techniques for specifying the behaviour of software,
with applications of these techniques to design, verification
and construction of software. Logic-based techniques such as
loop invariants and class invariants. Automata and grammar-based
techniques, with applications to scanners, parsers, user-interface
dialogs and embedded systems. Computability issues in software
Prerequisite: CISC 124/3.0.
Prerequisite or co-requisite: CISC 204/3.0
This course is intended to provide students in 2nd or 3rd year of a
Computing program essential material on formal languages and automata,
and on imperative program specification using logical predicates. Such
material is often taught from either a purely theoretical point of
view (for example, emphasizing complexity hierarchies or completeness
results) or from a strictly practical point of view (for example,
in courses on compilers or software validation); the aim here is to
demonstrate the practical use of mathematically-based Computing Science.
The topics have been chosen because they are both theoretical and
practical. The material on formal languages is integrated into a
specification-oriented framework by treating state diagrams, regular
expressions, and context-free grammars as specialized specification
languages: formalisms for specifying language recognizers. Computability
issues arise because certain specifications are unimplementable.
The courses to which this course is a prerequisite are
- CISC-322/3.0 (Software Architecture)
- CISC-327/3.0 (Software Quality Assurance)
- CISC-422/3.0 (Formal Methods)
- CISC-423/3.0 (Software Requirements)
- CISC 458/3.0 (Language Processors)
- CISC-462/3.0 (Computability and Complexity)
- CISC-465/3.0 (Programming Languages)
- CISC-481/3.0 (Syntax Systems for Natural Languages)
This course is required in BMCO, CSCI, SODE, COMP-M-BCH, and COMP-G-BCP.
- Regular languages
Expressive power, deterministic finite state automata,
non-deterministic finite state automata, regular grammar, regular
expressions, equivalence of these formalisms (with partial proofs),
closure properties, pumping lemma.
- Context-free languages
Expressive power, nondeterministic pushdown automata, context-free
grammars, produce-match npdas, equivalence of formalisms, closure
properties, pumping lemma.
- Deterministic context-free languages
Grammar manipulation for better grammar properties, lookahead, LL
parsing, changing an npda into a dpda, importance for compilation.
Church-Turing thesis, Halting problem and related problems. If time
permits: enumeration of partial functions and implications for
Alphabets of observations, predicates to describe program states,
specifications as predicate transformers, programs as executable
specifications, verification vs calculation.
- Introduction to a specification methodology
Reasoning with programs: assignment statements, sequential
composition, conditional statements, loops (including loop invariants,
proof of termination), array/vector assignment. If time permits:
procedure/method call or class invariants.
Either Hoare-style or refinement-calculus methodologies may be used.
Currently, the only text at an appropriate level that covers both major
topics seems to be:
Tennent, Specifying Software, A Hands-On Introduction, CUP (2002).
There are many texts on formal languages, automata and computability.
The following are suitable to the "both-theoretical-and-practical"
orientation of this course:
- A. V. Aho and J. D. Ullman. Foundations of Computer Science.
W. H. Freeman, 1992.
- K. J. Gough. Syntax Analysis and Software Tools. Addison-Wesley, 1988.
- J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to Automata
Theory, Languages, and Computation. Addison-Wesley, 2001.
- P. Linz, An introduction to Formal Languages and Automata, 4th
edition, Jones and Bartlett, 2006.
- D. Kelley, Automata and Formal Languages, Prentice-Hall, 1995.
- J.C. Martin, "Introduction to Languages and the Theory of Computation",
There are also many texts that discuss predicate-based specification of
- S. Alagic and M. A. Arbib. The Design of Well-Structured and Correct
Programs. Springer-Verlag, 1978.
- R. C. Backhouse. Program Construction: Calculating Implementations
from Specifications, Wiley 2003.
- K. Broda, S. Eisenbach, H. Khoshnevisan, and S. Vickers.
Reasoned Programming. Prentice Hall International, 1994.
- C. Casey. A Programming Approach to Formal Methods. McGraw-Hill
- E. Cohen. Programming in the 1990s: An Introduction to the Calculation
of Programs. Springer Verlag, 1990.
- O.-J. Dahl. Verifiable Programming. Prentice Hall International, 1992.
- E. W. Dijkstra and W. H. J. Feijen. A Method of Programming.
- G. Dromey. Program Derivation: The Development of Programs from
Specifications. Addison-Wesley, 1989.
- M. J. C. Gordon. Programming Language Theory and Its Implementation.
Prentice Hall International, 1988.
- D. Gries. The Science of Programming. Springer-Verlag, 1981.
- A. Kaldewaij. Programming: The Derivation of Algorithms. Prentice Hall
- B. Liskov and J. Guttag. Program Development in Java: Abstraction,
Specification, and Object-Oriented Design. Addison-Wesley, 2000.
- C. C. Morgan. Programming from Specifications, 2nd edition. Prentice
Hall International, 1994.
- J. J. Mead and A. M. Shende. Persuasive Programming. ABF Content,
Franklin, Beedle, and Associates, 2001.
- J. C. Reynolds. The Craft of Programming. Prentice Hall International,
- A. M. Stavely. Toward Zero-Defect Programming. Addison-Wesley Longman,
- N. Wirth. Systematic Programming, An Introduction. Prentice Hall, 1973.