A method for extracting syntactic specifications from heap-manipulating code is described. The state of the heap is represented as an environment mapping each variable or field to a relational expression. A procedure is executed symbolically, obtaining an environment for the post-state that gives the value of each variable and field in terms of the val- ues of variables and fields of the pre-state. Approximation is introduced by forming relational unions at merge points in the control flow graph, and by widening union-of-join expressions to transitive closures. The resulting analysis is linear in the length of the code and the number of fields, but capable of producing non-trivial specifications of surprising accuracy.

# Lightweight Extraction of Syntactic Specifications

Autor: | Mana Taghdiri, Robert Seater, Daniel Jackson |
Links: | |
---|---|---|---|

Quelle: | International Symposium on Foundations of Software Engineering (FSE), 2006 |
||

Datum: | Nov. 2006 | ||