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
Translating Separation Logic into Dynamic Frames Using Fine-Grained Region Logic by Yuyan Bao, Gary T. Leavens, and Gidon Ernst Abstract Several techniques have been proposed for specification and verification of frame conditions, making it difficult for specification language designers to know which to pick. Ideally there would be a single mechanism that could be used to express specifications written in all techniques. In this paper we provide a single mechanism that can be used to write specifications in the style of both separation logic and dynamic frames. This mechanism shows common characters between the two methodologies. Keywords: Region logic, sequential programming, separation logic, dynamic frames, formal methods, frame axioms, 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;