Hiding global invariants by local reasoning in region logic

Опубликовано 6 сентября 2016, 17:18

Higher order frame rules in separation logic provide a way to understand disciplines such as ownership for information hiding in object based programs. Recent work of Banerjee, Naumann, and Rosenberg uses explicit regions to express, in classical first-order assertions, the read-footprints of predicates and write-footprints of commands, supporting an ordinary frame rule. On this basis, I give a second order frame rule, show its admissibility, and describe its use in encoding disciplines like ownership.