SPARE: Formal Semantics

Abstract

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.