This note defines BoogiePL, an intermediate language for program analysis and program verification. The language is a simple coarsely typed imperative language with procedures and arrays, plus support for introducing mathematical functions and declaring properties of these functions. BoogiePL can be used to represent programs written in an imperative source language (like an object-oriented .NET language), along with a logical encoding of the semantics of such a source language. From the resulting BoogiePL program, one can then generate verification conditions or perform other program analyses such as the inference of program invariants. In this way, BoogiePL also serves as a programming-notation front end to theorem provers. BoogiePL is accepted as input to Boogie, the Spec# static program verifier.

PDF file

Details