This paper presents an extension to Hoare Logic for pointer program verification. The main observation leading to this logic is that the value of an expression e depends only on the contents stored in a finite set of memory units. This set can be specified using another expression (called the memory scope of e) constructed syntactically from e. A set of construction rules are given in this paper for expressions which may contain recursive functions (predicates). It is also observed that the memory scope of e is a super set of the memory scope of the memory scope of e. Based on this, local reasoning can be supported using assertion variables which represent arbitrary assertions. Program-pointspecific expressions are used to specify the relations between different program points. Another feature of this logic is that for formulas with no user-defined functions, the weakest-preconditions can be calculated w.r.t. assignments.
展开▼
