A Relational Program Logic with Data Abstraction and Dynamic Framing

Anindya Banerjee, Ramana Nagasamudram, David A. Naumann +1

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 repres…