Teaching specification and verification of event-driven programs using cleanroom software engineering

摘要

Software verification, the process of ensuring that a software artifact meets its specification, is both difficult to perform and difficult to teach. The two principal techniques for software verification are correctness proving and testing. While a correctness proof can demonstrate conclusively that a software artifact meets its specification for all inputs, correctness proving is a difficult, tedious, and error-prone activity [1]. Hence, most software engineers rely in practice upon testing as the primary means of ensuring that a software artifact meets its specification.