English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Dedicated to Tony Hoare.  In a paper published in 1972 Hoare articulated the fundamental notions ofhiding invariants and simulations. Hiding: invariants on encapsulated datarepresentations need not be mentioned in specifications that comprise the APIof a module. Simulation: correctness of a new data representation andimplementation can be established by proving simulation between the old and newimplementations 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 dynamicallyallocated objects. In recent years, progress has been made towards formalizingthe claim, for simulation, though mainly in semantic developments. In thisarticle, hiding and simulation are combined with the idea in Hoare's 1969paper: a logic of programs. For an object-based language with dynamicallocation, we introduce a relational Hoare logic with stateful frameconditions that formalizes encapsulation, hiding of invariants, and couplingsthat relate two implementations. Relations and other assertions are expressedin first-order logic. Specifications can express a wide range of relationalproperties such as conditional equivalence and noninterference withdeclassification. The proof rules facilitate relational reasoning by means ofconvenient alignments and are shown sound with respect to a conventionaloperational semantics. A derived proof rule for equivalence of linked programsdirectly embodies representation independence. Applicability to representativeexamples is demonstrated using an SMT-based implementation.

A Relational Program Logic with Data Abstraction and Dynamic Framing