Document in text mode:

ThisisBoogie2K.RustanM.LeinoMicrosoftResearch,Redmond,WA,[email protected],workingdraft24June2008.Abstract.Boogieisanintermediateverificationlanguage,designedtomaketheprescriptionofverificationconditionsnaturalandconvenient.Itservesasacom-monintermediaterepresentationforstaticprogramverifiersofvarioussourcelanguages,anditabstractsovertheinterfacestovarioustheoremprovers.Boogiecanalsobeusedasasharedinputandoutputformatfortechniqueslikeabstractinterpretationandpredicateabstraction.Asalanguage,Boogiehasbothmathe-maticalandimperativecomponents.TheimperativecomponentsofBoogiespec-ifysetsofexecutiontraces,thestatesofwhicharedescribedandconstrainedbythemathematicalcomponents.Thelanguageincludesfeatureslikeparamet-ricpolymorphism,partialorders,logicalquantifications,nondeterminism,totalexpressions,partialstatements,andflexiblecontrolflow.TheBoogielanguagewaspreviouslyknownasBoogiePL.ThispaperisareferencemanualforBoogieversion2.Hello,mynameisRustanLeino.I’macomputerscientist.Iwr...