The locality principle, paired with suitable frame rules, is a fundamental feature in resource-aware program logics, which enables modular and scalable reasoning. However, depending on the analysis, ad hoc axioms and frame rules must be crafted each time. In his work on the calculational design of program logics, Cousot covers a wide spectrum of correctness and incorrectness analyses, outlining a method for deriving proof systems directly from program semantics, but his approach does not inherently capture the locality principle. In this work, we propose a general technique to systematically determine the minimal heap required in pre- and postconditions starting from a set of semantic closure properties and show that our methodology can improve exisisting proposals in terms of succintness, applicability, generalization and uniformity.
