Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extended to encompass dynamically allocated objects. In recent years, progress has been made towards formalizing the claim, for simulation, though mainly in semantic developments. In this article, hiding and simulation are combined with the idea in Hoare's 1969 paper: a logic of programs. For an object-based language with dynamic allocation, we introduce a relational Hoare logic with stateful frame conditions that formalizes encapsulation, hiding of invariants, and couplings that relate two implementations. Relations and other assertions are expressed in first-order logic. Specifications can express a wide range of relational properties such as conditional equivalence and noninterference with declassification. The proof rules facilitate relational reasoning by means of convenient alignments and are shown sound with respect to a conventional operational semantics. A derived proof rule for equivalence of linked programs directly embodies representation independence. Applicability to representative examples is demonstrated using an SMT-based implementation.
翻译:在1972年出版的一篇论文中,Hoare阐述了隐藏变数和模拟的基本概念。 隐含:封装数据表示的变数不必在构成模块的API的规格中提及。 模拟:新数据表示和执行的正确性可以通过利用封装状态上界定的混合关系对旧和新实施进行模拟来确立。 这些结果是正式的语义和简单的国家模式,尽管文件声称这可以扩大到包括动态分配的对象。 近年来,在正式确定关于模拟的主张方面取得了进展,但主要是在语义发展方面。在本篇文章中,隐藏和模拟与Hoare1969年的论文中的概念:程序逻辑相结合。 对于基于目标的语言,我们采用动态分配,我们采用了一种关联的Hare逻辑与固定封装、隐藏变数和以两种执行为基础的组合。 在一阶逻辑中表述了关系和其他说法。 具体描述可以表达广泛的关系属性关系关系,主要是在模拟方面,在Hoareetality Process 上展示了一种固定定等值和不妥协性原则的推理。