SPARE: Formal Semantics

The Structured Program Analysis Refinement Environment (SPARE) [9] is a tool for rapid prototyping of program analysis algorithms through high-level specifications. An analysis algorithm is specified through denotational specifications. This report provides the formal semantics for the specification language. The specification language is based on the notation of lambda-calculus and the conventions used for writing denotational specifications for semantics of programming languages. Language features have been specially designed to express analysis algorithms in a clear and concise fashion. The semantics is presented using a formalism based on Natural Semantics [5]. The semantics specification consists of a set of logical inference rules and facilitates the derivation of proofs for the correctness of translations for SPARE as well as the correctness of analysis algorithms specified in SPARE.

Download this report (PDF)

Return to tech report index