necessity of formal methods education has developed from its increasing assimilation into systems development within industry. Organizations responsible for a wide range of applications have found it necessary to find an improved means of intellectual control over their complex system development and that formal methods can meet this need. To this end, the International Survey of Industrial Applications of Formal Methods concluded and recommended: The current educational base in the US is weak in teaching formal methods in the context of software engineering . . . There is a clear need for improved integration of formal methods techniques with other software engineering practices[2]There exists a number of articles in the current literature expressing the belief that the current educational program offered for a computer science degree does not stress the fundamental mathematical and engineering principles that should form the basis of software engineering[3,4,5,6]. theory learned in mathematics and science classes is applied in other engineering classes, but unfortunately has not been applied in software engineering. inability to apply logic in practical circumstances prevents the student from doing the systematic analysis necessary to solve practical problems.For these reasons, it is desirable to include the definition and application of a formal method into the undergraduate curriculum with the goal of increasing the complex problem solving skills of the software engineer. Formal analysis should be introduced early into the undergraduate curriculum to ensure substantial learning, use, and training in formal methods application.

Semi-formal specification and verification in the style of the cleanroom method, combined with testing, have proven to be exceptionally effective in reducing the number of defects in software, as well as being cost-effective in practice. A course based on these principles is described, and the results of class projects and projects by graduates of the course are presented. These results provide evidence that cleanroom techniques, as adapted for the course, are indeed effective, and that these techniques can be taught successfully, even to undergraduates.

Methods are presented for verifying loops which iterate over elements of data structures. This verification is done in the functional style developed by Mills and others, in which code is verified against the function that the code is intended to compute. The methods allow the verifier to concentrate on the essential computation performed on each element of the structure, and separate out such concerns as data-structure access and termination so that they do not need to be verified again for every loop in the program. The methods are applicable to a large class of data structures and iterations over them.>

A modeling scheme is presented which provides a medium for the rigorous, formal, and abstract specification of large-scale software system components. The scheme allows the description of component behavior without revealing or requiring the description of a component's internal operation. Both collections of sequential processes and the data objects which they share may be described. The scheme is of particular value during the early stages of software system design, when the system's modules are being delineated and their interactions designed, and when rigorous, well-defined specification of undesigned components allows formal and informal arguments concerning the design's correctness to be formulated.