Queen's School of Computing

CISC 223/3.0 Software Specifications

Original Authors: David Skillicorn and Bob Tennent
Last Revised: August 30, 2006

Calendar Description

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 specifications.

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 computability, universality.


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.
Possible Textbooks

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", McGraw-Hill., 2002

There are also many texts that discuss predicate-based specification of imperative programs:

  • 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 International, 1994.

  • 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. Addison-Wesley, 1988.

  • 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 International, 1990.

  • 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, 1981.

  • A. M. Stavely. Toward Zero-Defect Programming. Addison-Wesley Longman, 1999.

  • N. Wirth. Systematic Programming, An Introduction. Prentice Hall, 1973.