Integrating formalism into undergraduate software engineering

This paper describes an approach and rational for using logic and formal methods in undergraduate software engineering education. Formal methods and logic provide a mathematical basis for modeling software analogous to the role of continuous mathematics in traditional engineering disciplines. Traditional software engineering techniques provide means for modeling software development processes and structuring specifications. Neither formal methods nor traditional approaches subsume the other, but are complimentary in software engineering education and practice. The course described here was a part of the standard Computer Engineering curriculum at The University of Cincinnati from 1993 through 1999. This paper reports on the course and observations over six years of teaching the course to undergraduate and graduate students.