Site Map | College of Engineering | UC Davis | MyUCDavis

ECS 262 FORMAL SPECIFICATION (3) II

Lecture: 3 hours

Prerequisite: Course ECS 261

Grading: Letter; based on homework, midterm, final and project

Catalog Description:
Formal specification of modules, and its relationship to top-down programming development and verification. Abstract data types, together with methods for specifying them. Implementations and proofs of implementation. Using specifications to reason about programs. Parameterized types. Constructing good formal specifications. Offered in alternate years.

Expanded Course Description:

  1. Formal Specification of Modules
    1. What constitutes a specification
    2. The place of formal module specifications in the scheme of things
  2. Abstract Data Types
    1. Many-sorted algebras
    2. Non-deterministic algebras
    3. The notion of abstractness
    4. Abstract type as specification
  3. Implementation
    1. Why implementations preserve program correctness
    2. Partial implementations
  4. Survey and Comparison of Specification Methods and Their Semantics
    1. Pre-post, initial algebra, and final algebra specifications; perhaps others
    2. Associated methods for proving correctness of implementations
    3. Advantages and disadvantages of the various methods
  5. Parameterized Data Types
    1. Specification
    2. Implementation
  6. Reasoning about Programs using Formally Specified Modules
  7. Constructing Good Formal Specification
    1. Specifying a module
    2. Using the specification in a program verification

Textbook:
Selected from the current literature.

ABET Category Content:
Engineering Science: 2 units
Engineering Design: 1 units

Instructor: K. Levitt

Prepared By: K. Levitt (Jan 1996)

THIS COURSE DOES NOT DUPLICATE ANY EXISTING COURSE

Last revised:4/97

Back to Course Descriptions