关于目标程序的演算

摘要：

面向对象软件的可扩展性需要一种简单直观的方法来处理引用，这与面向对象程序员如何推理他们的程序密切相关。本文提出的方法是一种目标程序演算，它由四个部分组成：组合逻辑，一个描述程序语义和证明程序属性的框架;负变量，用于处理面向对象编程的细节，特别是限定调用;别名演算，用于确定引用表达式是否可以具有相同的值;对象结构演算，一种在面向对象程序执行过程中出现的结构的规范技术。这篇文章通过证明一个链表反转的标准算法来说明微积分。

英文摘要：

Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here, a Calculus of Object Programs, combines four components: compositional logic, a framework for describing program semantics and proving program properties; negative variables to address the specifics of O-O programming, in particular qualified calls; the alias calculus, which determines whether reference expressions can ever have the same value; and the calculus of object structures, a specification technique for the structures that arise during the execution of an object-oriented program. The article illustrates the Calculus by proving the standard algorithm for reversing a linked list.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。