Verified object-oriented programs

计算机系统的每个用户都熟悉软件产品的错误和/或不当行为。这是一个恼人的情况，但对于大多数应用程序并不严重。另一方面，特别是在电子商务领域，正确的程序变得越来越重要。例如，这种程序的每个用户都希望确保秘密数据（信用卡号，pin等）未经授权的人员不得进入。另一个例子可能是控制核电站的软件。希望这样的计划不会失败。开发可靠的软件产品的一种方法是程序验证，即提供一个数学证明的正确性与给定的规范。由于上述原因，遵循欧洲ITSEC（信息技术安全评估标准）E4-E6级（该标准的三个最高认证/保证级别）的软件产品认证需要应用正式方法，包括至少部分系统的正确性证明。

Every user of computer systems is familiar with errors and/or misbehavior of software products. This is an annoying situation but for most applications not serious. On the other hand, especially in the area of ebusiness correct programs become more and more important. For example, every user of such a program wants to be sure that secret data (credit card number, pin, etc.) are not accessible to unauthorized persons. Another example might be software controlling a nuclear plant. It is desirable that such a program does not fail. One method for developing reliable software products is program verification, i.e. providing a mathematical proof of correctness versus a given specification. For the reasons mentioned above a certification of a software product following the European ITSEC (Information Technology Security Evaluation Criteria) at level E4-E6 - the three highest certification/assurance levels of that standard - requires the application of formal methods including correctness proofs of at least parts of the system.