Local Reasoning and Information Hiding in SCAPLast modified: Sat Mar 29 17:39:15 2008 GMT. AuthorsXinyu FengZhong Shao AbstractSeparation logic supports state-modular program verification in two aspects: local reasoning by means of the ordinary (first-order) frame rule and information hiding by the hypothetical frame rule (a second-order frame rule). In this paper, we show the support of local reasoning and information hiding in SCAP, a program logic for low-level programs with stack-based control abstractions. We show that, using intuitionistic assertions as preconditions, and using a binary relation over program states to specify program behaviors, SCAP naturally supports local reasoning without requiring a frame rule. Then we show the hypothetical frame rule can be proved as an admissible rule in SCAP, given some natural constraints over SCAP specifications. Published |
Copyright © 1996-2024 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science |
colophon |