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. Logicbased techniques such as
loop invariants and class invariants. Automata and grammarbased
techniques, with applications to scanners, parsers, userinterface
dialogs and embedded systems. Computability issues in software
specifications.
Prerequisite: CISC 124/3.0.
Prerequisite or corequisite: CISC 204/3.0
Objectives
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 mathematicallybased Computing Science.
The topics have been chosen because they are both theoretical and
practical. The material on formal languages is integrated into a
specificationoriented framework by treating state diagrams, regular
expressions, and contextfree 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
 CISC322/3.0 (Software Architecture)
 CISC327/3.0 (Software Quality Assurance)
 CISC422/3.0 (Formal Methods)
 CISC423/3.0 (Software Requirements)
 CISC 458/3.0 (Language Processors)
 CISC462/3.0 (Computability and Complexity)
 CISC465/3.0 (Programming Languages)
 CISC481/3.0 (Syntax Systems for Natural Languages)
This course is required in BMCO, CSCI, SODE, COMPMBCH, and COMPGBCP.
Topics
 Regular languages

Expressive power, deterministic finite state automata,
nondeterministic finite state automata, regular grammar, regular
expressions, equivalence of these formalisms (with partial proofs),
closure properties, pumping lemma.
 Contextfree languages

Expressive power, nondeterministic pushdown automata, contextfree
grammars, producematch npdas, equivalence of formalisms, closure
properties, pumping lemma.
 Deterministic contextfree languages

Grammar manipulation for better grammar properties, lookahead, LL
parsing, changing an npda into a dpda, importance for compilation.
 Computability

ChurchTuring thesis, Halting problem and related problems. If time
permits: enumeration of partial functions and implications for
computability, universality.
 Specification

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 Hoarestyle or refinementcalculus 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 HandsOn Introduction, CUP (2002).
There are many texts on formal languages, automata and computability.
The following are suitable to the "boththeoreticalandpractical"
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. AddisonWesley, 1988.
 J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to Automata
Theory, Languages, and Computation. AddisonWesley, 2001.
 P. Linz, An introduction to Formal Languages and Automata, 4th
edition, Jones and Bartlett, 2006.
 D. Kelley, Automata and Formal Languages, PrenticeHall, 1995.
 J.C. Martin, "Introduction to Languages and the Theory of Computation",
McGrawHill., 2002
There are also many texts that discuss predicatebased specification of
imperative programs:
 S. Alagic and M. A. Arbib. The Design of WellStructured and Correct
Programs. SpringerVerlag, 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. McGrawHill
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.
AddisonWesley, 1988.
 G. Dromey. Program Derivation: The Development of Programs from
Specifications. AddisonWesley, 1989.
 M. J. C. Gordon. Programming Language Theory and Its Implementation.
Prentice Hall International, 1988.
 D. Gries. The Science of Programming. SpringerVerlag, 1981.
 A. Kaldewaij. Programming: The Derivation of Algorithms. Prentice Hall
International, 1990.
 B. Liskov and J. Guttag. Program Development in Java: Abstraction,
Specification, and ObjectOriented Design. AddisonWesley, 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 ZeroDefect Programming. AddisonWesley Longman,
1999.
 N. Wirth. Systematic Programming, An Introduction. Prentice Hall, 1973.
