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

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

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

Computability

Church-Turing 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 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.