Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Conditional Effects in Fine-grained Region Logic by Yuyan Bao, Gary T. Leavens, and Gidon Ernst Abstract 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. General terms: Verification Keywords: Frame axiom, modifies clause, separation logic, dynamic frames, region logic, formal methods, Dafny language, DafnyR language. 2013 CR Categories: D.2.4 [Software Engineering] Software/Program Verification — Formal methods, programming by contract; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs — Assertions, logics of programs, pre- and post-conditions, specification techniques.