Verified object-oriented programs

计算机系统的每个用户都熟悉软件产品的错误和/或错误行为。这是一个令人讨厌的情况，但对大多数应用程序来说并不严重。另一方面，特别是在电子商务领域，正确的程序变得越来越重要。例如，此类程序的每个用户都希望确保机密数据（信用卡号码、密码等）不会被未经授权的人访问。另一个例子可能是控制核电站的软件。希望这样的程序不会失败。开发可靠软件产品的一种方法是程序验证，即根据给定的规范提供正确性的数学证明。由于上述原因，软件产品要符合欧洲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.