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.