2019/04/15 by Nanevski, Aleksandar, Banerjee, Anindya, Delbianco, Germán Andrés +1
#D.1.1 #D.1.3 #D.2.4 #D.3.2 #Distributed #F.3.1 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Parallel #Programming Languages (cs.PL) #and Cluster Computing (cs.DC)
paper · doi:10.48550/arxiv.1904.07136
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.