| Date |
Class |
| 01/21/03 |
Instructional Objectives:
Be able to answer the following questions
- What is a formal method?
- What are some well-known formal methods applied in software engineering?
- What is the difference between a software requirement and
a software specification?
- The introductory lecture identified phases of the software development
life cycle.
List each of these phases and explain the purpose/activities of each.
- A particular software engineering formal method is often targeted
at a particular phase of software development. List the formal methods
that we will cover in this class along with the development phase in which
they will be used.
- What are the perceived strengths of formal methods in software engineering?
- What are the perceived weaknesses of formal methods in software engineering?
- What do we mean by strong formal method and why are such
methods potentially more attractive than "non-strong" methods?
Class Notes:
Course Overview
Required Readings:
[vLam00]
Optional Readings:
[Clark96]
|
| 01/23/03 |
Instructional Objectives:
- Be able to define the following: set, relation, function, scalar, partial
function, total function.
- Be able to define and compute the following operations on sets and
relations
- set union, intersection, difference, complement, inclusion
- relation composition, transposition
- Be able to define the following properties of binary relations: reflexive,
transitive, symmetric, anti-symmetric.
- Understand the implicit constraints associated with relation
multiplicity declarations.
Class Notes:
Sets and Relations
Required Readings:
[vLam00]
Optional Readings:
[Clark96]
Exercises:
Sets and Relations
|
| 01/28/03 |
Instructional Objectives:
- Understand the basic concepts of Alloy definitions including:
- domains
- relations with Alloy's multiplicity notations (!,+,*,?)
- invariants
- Be able to run the Alloy constraint checker on existing examples.
|
| 01/30/03 |
Instructional Objectives:
- Understand more basic concepts of Alloy definitions including:
- conditions
- assertions
- indexed relations
- Be able to run the Alloy constraint checker on existing examples.
|
| 02/04/03 |
Instructional Objectives:
- Be able to understand the semantics of Alloy formulas
- Be able to write and read realistic Alloy models.
- Be able to use the Alloy constraint analyzer to build and debug medium-sized examples
|
| 02/06/03 |
Instructional Objectives:
- Be able to understand the semantics of Alloy formulas
- Be able to write and read realistic Alloy models.
- Be able to use the Alloy constraint analyzer
to build and debug medium-sized examples
|
| 02/11/03 |
Instructional Objectives:
- Understand the basic concepts of dynamic models in Alloy including ...
- Primed variables
- Operations
- Mutabilities
- Be able to define the ideas of pre-condition, post-condition, and frame-condition and identify them in an Alloy operation.
- Be able to use ACA to analyze operations.
|
| 02/13/03 |
Instructional Objectives:
- Understand the basic concepts of dynamic models in Alloy including ...
- Primed variables
- Operations
- Mutabilities
- Be able to define the ideas of pre-condition, post-condition, and frame-condition and identify them in an Alloy operation.
- Be able to use ACA to analyze operations.
|
| 02/18/03 |
Instructional Objectives:
- Be able to apply Alloy and the checker to a realistic system.
- Be able to recognize situations where using Alloy could be effective and situations where it may not be especially effective.
|
| 02/20/03 |
Instructional Objectives:
- Be able to apply Alloy and the checker to a realistic system.
- Be able to recognize situations where using Alloy could be effective and situations where it may not be especially effective.
|
| 02/25/03 |
Instructional Objectives:
- Be able to apply Alloy and the checker to a real world problem.
- Be able to use Alloy to evaluate the design of abstract algorithms.
|
| 02/27/03 |
Instructional Objectives:
- Be able to apply Alloy and the checker to a real world problem.
- Be able to use Alloy to evaluate the design of abstract algorithms.
|
| 03/04/03 |
Instructional Objectives:
- be able to give a one paragraph summary of UML class diagrams
explaining
- their purpose
- their primary semantic components
- forms of commercially available tool support.
- Be able read and draw UML class diagrams.
- Understand how to render a UML class diagram as an object model in USE.
- Be able to create object and association instances in USE.
|
| 03/06/03 |
Instructional Objectives:
- Understand basic OCL constraint syntax and semantics
- be able to write simple invariants in OCL/USE
|
| 03/11/03 |
Instructional Objectives:
- Be able to describe the type hierarchy of OCL including how subtyping relation interacts with collection types.
- Be able to apply the collection operations such as select, reject, include, etc. and understand when operations return bags or sets.
Be able to phrase the other collection operations in terms of the 'iterate' operation.
- Be able to write invariants in OCL/USE using iterative
constructs and quantifiers.
|
| 03/13/03 |
Midterm
|
| 03/18/03 |
No class (Spring break)
|
| 03/20/03 |
No class (Spring break)
|
| 03/25/03 |
Instructional Objectives:
- Understand midterm solutions.
- Be able code operations that compute transitive closure using recursive operations.
- Be able to use constructs such as let, enum types, sequences, and ordered associations.
|
| 03/27/03 |
Instructional Objectives:
- Be able code operations that compute transitive closure using recursive operations.
- Be able to use constructs such as let, enum types, sequences, and ordered associations.
- Understand situations in which operations may be undefined and how USE propagates undefined values.
- Understand how nested collections are handled differently in the OCL specification (they are always flattened) vs. USE (they are not flattened).
|
| 04/01/03 |
Instructional Objectives:
- Be able extract ocl constraint from UML class diagrams
- Be able to identify invariants by navigating cycles in class diagrams
|
| 04/03/03 |
No class
|
| 04/08/03 |
Instructional Objectives:
- Be able specify in OCL operations with side effects by means of pre- and post-considitions
- Be able to check pre- and post-conditions with the USE tool
|
| 04/10/03 |
Instructional Objectives:
- Group exercises on:
- writing OCL invariants
- specifying in OCL operations with side effects by means of pre- and post-considitions
|
| 04/15/03 |
Instructional Objectives:
- Understand the principles of design-by-contract
- Be able to relate these principles to the notions of pre and post-condition as discussed earlier in the course.
|
| 04/17/03 |
Instructional Objectives:
- Be able to annotate Java code with class invariant, pre and postconditions
- Be aware of the different ways and degrees in which design-by-contract can be implemented
- Know about a few of the tools or programming languages that emphasize design-by-contract.
|
| 04/22/03 |
Instructional Objectives:
- Understand how to write class invariants in ESC/Java
- Understand how to write basic pre/post-conditions in ESC/JavaBe able to annotate Java code with class invariants, pre and postconditions
|
| 04/24/03 |
Instructional Objectives:
- Have an overview of the ESC/Java annotation language and of the tools desging philosophy
- Understand the unsoundness and incompleteness limitations of the tool and their rationale
- Be able to incrementally annotate Java programs and check them with ESC/Java
| Class Notes: |
ESC/JAVA Basics
|
| Required Readings: |
[Lei00]
|
| Exercises: |
Exercises in the class notes,
Tutorial exercise in Section 0 of [Lei00]
|
|
| 04/29/03 |
Instructional Objectives:
- Understand how ESC/Java carries out modular checking and
how this affects how a user should use class invariants and pre/post-conditions.
- Understand the ESC/Java concept of owner.
|
| 05/01/03 |
Instructional Objectives:
- Be able to apply ESC/Java ghost variables to e.g., carry out static type-checking on elements of containers.
- practice with ESC/Java specifications
|