Conditional effects in fine-grained region logic

Specification languages have long featured ways to describe what does not change when an imperative procedure is executed: the so-called frame problem. Solutions to the frame problem are needed for formal verification in imperative programming, as otherwise a verification would not be able to accumulate information from one statement to the next. Region logic is one of the approaches to solving the frame problem. We present a modified version of region logic with fine granularity and introduce conditional effects that allows one to specify more precise frame conditions.