Interobject Message Passing for Large Equational Specifications

Software engineering (SE) is an important component of an undergraduate computer-science (CS) curriculum. Recently published guidelines recommend that a CS curriculum contain at least three semester-units of SE coursework, including: formal-specification techniques, design techniques, and a team project. This abstract briefly describes how these recommendations are addressed in SE courses at BSU (in Boise, Idaho) and UCD (in Davis, California). However, it is more concerned with a formal-specification problem I have encountered while teaching these courses. Furthermore, it suggests a solution.

Formal-specification techniques include those using model-based and value-based languages. Examples of model-based languages are VDM, Z, and EHDM. Examples of value-based languages are OBJ, Larch, and Affirm. In my courses, I use VDM and OBJ as model-based and value-based representatives (respectively). VDM is also called a state-based language, because its modules contain state variables. OBJ is also called an equational language, because its modules contain equations.

Design techniques include function-oriented and object-oriented design. VDM and OBJ both encourage object-oriented design, but neither provides a complete set of features. For example, VDM does not support overloading or inheritance, and OBJ does not support state variables.

SE curricula guidelines also recognize the importance of a significant project. This should be more than just a large programming assignment. In fact, I feel that the implementation phase should be deemphasized or eliminated, to force students to consider the phases that are too often neglected or underestimated: requirements definition, specification, testing, and maintenance.

In my courses, the project is a term-long simulation of the first two phases of a large software-development effort (viz., requirements definition and specification). Students form teams, select a project from a set of candidates, and produce several documents. Candidates include information systems for a university registrar, a university library, and a dormitory kitchen. They produce a requirements document, a specification document, and a users' manual. Actually, they produce two specification documents: one gives the functional specification in VDM; the other in OBJ.