ON THIS PAGE:

Assumptions

Prerequisites

Approach

Typical Text

Course Outline

Assumptions
Students should have

• had a COMP 523-like course, been exposed to the basic lifecycle of requirements, specs, design, coding, testing, maintenance.
• had an algorithms course, but no formal verification
• had a languages course in which basic run-time structure is learned for basic imperative languages
• learned basics of data abstraction
• student are not assumed to have learned formal semantics

Prerequisites
COMP 550, 524.

Approach
This class is designed to provide students with knowledge of development of software, from formal specification through to working systems. The student will learn graduate level material that presumes an undergraduate preparation in programming languages and software engineering. The material, therefore, is heavy on formal methods for supporting software development, which are founded on formal semantics of programming languages. While we are leaving a deep treatment of formal language semantics for advanced courses, we will introduce some semantics and verification in support of commonly used specification methods. It also presents disciplined engineering practices such as design and testing.

The "software" part of the class covers specifications, design, coding (as mentioned), testing methods, and an overall look at methods for continuous improvement of the software development process. The overall goal is to give a broad introduction to SE techniques used in practice, along with an introduction to formal methods in SE and their current limitations.

The "languages" part of the class gives practical experience with module coding in different language paradigms, covering modern imperative object-oriented languages (Eiffel and C++), modern functional languages (Haskell), and logic-based languages (Prolog).

The intent is to treat very small problems using completely formal methods from spec to code, using axiomatic verification. Some larger, but still relatively simple and well-defined problems would be used to present functional design and to introduce Haskell (or ML) and Prolog as examples of languages that support the expression of these sorts of designs.

A larger portion of the time would be spent in describing object-oriented design methods and the support for the expression of such designs using object-oriented languages. We suggest using Eiffel as the carrier language because it is a clean language, simple to learn, that supports both formal and informal methods in OO software construction. An additional set of lectures could be used to relate the constructs and facilities of Eiffel to C++, the language that is most used in practice for this approach.

Typical Text
Ghezzi, Jazayeri, Mandrioli, Fundamentals of SE (General & some formal methods)
Gries, Science of Programming (Verification)
Betrand Meyer Object Oriented Software Construction (OO Design and Eiffel)
general Programming Language Texts (chapters of functional and logic programming)

Course Outline

• specs: specs (Z, VDM, predicates--axiomatic semantics and verification)
• design: OO, functional
• coding: (language examples) Eiffel, Haskell, prolog
• testing: black box, white box, mutation, statistical methods
• process: process modeling methods (Marvel, Weaver, etc.) SEI CMM; continuous process improvement

Week 1
• class overview
• software engineering
• introduction to the development process
• traditional process models like spiral, evolutionary

Week 2

• predicate logic
• formal specifications (axiomatic)
• axiomatic verification
• axioms for ADTs
• the Z specification language

Week 4

• Software design: functional methods
• realizing functional design in Prolog
• realizing functional design in Haskell

Week 7

• software design: object-oriented methods
• realizing an OO design in Eiffel
• realizing an OO design in C++

Week 12

• common testing methods (white box, black box, coverage metrics)
• axiomatic testing
• mutation testing
• statistical methods

Week 13

• SEI Capability Maturity Model and process modeling
• continuous process improvement
• Cleanroom as an example of a non-traditional development process