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.      The existing tools and methods are very limited in providing mechanisms to transfer properties, their proofs and proof methods from one construction to another. One is forced to start on a very basic level, which generates a huge amount of proof obligations. In real world examples proving all obligations is often not feasible or at least too expensive. A system and its underlying methodology, which allows less expensive development of verified programs would be of great benefit for software developers and finally for all users. My objective is to establish such a system and methodology, and, thus, to transfer theoretical results to real world applications.      The overwhelming success of object-oriented programming languages is based on reuse of software components. I will apply the same idea to the corresponding proof system. Properties of programs and their proof will be integrated into the class hierarchy such that a suitable inheritance mechanism transfers operations as well as the related properties and proofs to subclasses.