SPARE: Reference Manual

The Structured Program Analysis Refinement Environment (SPARE) is a tool for rapid prototyping of program analysis algorithms through high-level specifications. An analysis algorithm is specified through denotational specifications. 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. SPARE is designed to be used in conjunction with the Synthesizer Generator [2]. Analysis specifications are translated into specifications in the Synthesizer Language (SSL). The SSL translation, combined with the SSL specification for an editor for the language on which the analysis is defined, can be used to generate an editor for the language. The generated editor performs the specified analysis on programs input to the editor and the results can be displayed to verify the analysis