Lightweight extraction of syntactic specifications

A method for extracting syntactic specifications from heapmanipulating 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 values 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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification--formal methods; F.3.1 [Logics]: Reasoning about Programs--pre- and post-conditions, specification techniques General Terms Verification Keywords Modular Abstraction, Symbolic Su...

• Type: Conference
• Year: 2006
• Where: SIGSOFT
• Authors: Mana Taghdiri, Robert Seater, Daniel Jackson
• Keywords: SIGSOFT 2006, Software Engineering, Syntactic Specification, Syntactic Specifications, Terms Verification Keywords