CIS 376 Assignment 4

Winter 2003

Your fourth assignment will give you an opportunity to work with formal software engineering methods. You will need to identify a software product you have already written a complete set of natural language specifications for. You then need to write a set of formal specifications for this product. You may work with a partner if you wish.

You will need to write algebraic specifications for each data structure or object used in your program. You are to write formal specifications for each ordinary function, procedure, or method used in your design. You will need to formally prove the correctness of one of the algorithms defined as a function, procedure, or method.

This assignment is due in 3 weeks. Your assignment write-up should include a brief overview of the software product, the algebraic specifications for the data structures and objects, the formal specifications for your algorithms, one algorithm correctness proof, and a list of defects in the original specifications that were corrected in your revised specifications.

Assigned: 3/17/03

Date due: 4/07/03