Software Specifications fall term 2024

Department of Computing and Information Science

CISC/CMPE-223 SOFTWARE SPECIFICATIONS, FALL 2024

Course Description - fall term 2024

For important announcements and information on classes, assignments, midterm, quizzes, teaching assistants, office hours and all other course information please login to your CISC/CMPE-223 onQ page.
Note: CISC/CMPE223 considers the standard School of Computing syllabus https://www.cs.queensu.ca/students/undergraduate/syllabus/ to be part of the syllabus.

Required textbook

Specifying Software
A Hands-On Introduction
Author: R.D. Tennent
Cambridge University Press, 2002

Electronic subscriptions to the textbook are available online through Queen's Library . Direct link here (Queen's access only.)
The textbook's web site has a page of corrections to the published text.

Supplementary reading

Suggested additional reading may be found in the Introductions to Parts A and C and in the additional-reading section at the end of every chapter in the text.

There are many textbooks covering the material in the first half of the course (Part C in our textbook).

The following text is available online through Queen's library

Author/Creator: Peter Linz
Title: An Introduction to Formal Languages and Automata, Fifth Edition
Published: Jones and Bartlett Publishers c2012

Instructor

Kai Salomaa
Email: see the onQ site
When sending me email concerning the course, please make sure to use your Queen's email account and include CISC223 in the subject line. Otherwise I may never see the email.

Teaching assistants: For information on the teaching assistants please login to your CISC/CMPE-223 onQ page.

Goals of the course

The first part of the course provides an introduction to several conceptual tools that are widely used in computing: state diagrams, regular expressions and context-free grammars. In the second part you will learn to verify the correctness of (small) programs using logic based techniques. This part of the course builds on material you have studied, for example, in CISC 204. Additionally, we will briefly discuss the theoretical limits of algorithmic computation.

Learning Outcomes

Design regular expressions, state transition diagrams and context-free grammars for formal languages
Appraise the limitations of regular expressions and context-free grammars and to demonstrate that a language is nonregular
Design specifications for the functional behaviour of algorithmic code fragments
Formally verify the correctness of simple code fragments
Appraise the limitations of algorithmic computation and prove that the halting problem is unsolvable

CISC/CMPE223 considers the standard School of Computing syllabus https://www.cs.queensu.ca/students/undergraduate/syllabus/ to be part of the syllabus.

Academic Integrity

Please see a Statement on Academic Integrity from the Arts and Science web site posted here.

Software

Programming Language

A small fragment of the C programming language is used in the text. A compact reference manual may be found in Appendix A of the text book and on-line as a PDF file.

The text assumes that a file specdef.i of "headers" and definitions has been included into all programs; this is Program 3 on page 7 of the text.

An on-line reference manual on C programming:

C Programming by Steve Summitt, University of Washington.

Programming Platforms

Any implementation of C (or C++) may be used, but for this course we recommend an interpretive implementation of C called EiC. Although its run-time performance is relatively poor (comparable to Java), it has good error messages and run-time checks.

EiC has been installed on the CASLab Linux servers and workstations. For more information about accessing CASLab Linux, consult the CASLab How To.

To use EiC to parse and run a C program file prog.c in the current directory, just enter a

: eic prog.c

at a command-line prompt. Use re-direction to read from a file input or to write to a file output, as in

: eic prog.c < input > output

To get a summary of available command-line options and directives, enter

: eic -h

For more details see the link EiC.

The following on-line tutorials will be useful if you are unfamiliar with Unix-like systems:

Several other free C or C++ implementations which may be of interest are available:

gcc (GNU Compiler Collection) is a collection of production-quality compilers for several languages, including C and C++. It has been installed on zeus. For more details, enter

man gcc

to get a short manual.
tcc (Tiny C Compiler) is an extremely small and fast (but non-optimizing) C compiler.

Program Editors

Any text editor (such as Notepad on Windows) may be used to create and modify C programs. We suggest you use one window as a command-line interface (running EiC as necessary), and a separate window (or windows) to edit C source files.

On Unix-like systems such as Solaris and Linux, the most popular text editors are vi (or an improved version such as vim) and emacs (or an improved version such as xemacs); but if you are not familiar with either of these, we advise you to use nedit at a GUI (graphical user interface) and jed at a CLI (command-line interface).

An "integrated development environment" (IDE) combining a program editor, a compiler or interpreter, and possibly a debugger, won't be needed for the relatively small and, one hopes, verified programs you will be coding in this course.

PDF Readers

Assignments and other documents posted at this web site will be in Portable Document Format (PDF). The CASLab computers you use should have PDF viewers installed.

If you want to install a PDF viewer on your own computer, viewers for most platforms are available at no charge here: