language-boogie-0.2: Interpreter and language infrastructure for Boogie.

Safe HaskellNone




Interpreter for Boogie 2


Executing programs

executeProgramDet :: Program -> Context -> Maybe Integer -> Id -> TestCaseSource

executeProgramDet p tc entryPoint : Execute program p deterministically in type context tc starting from procedure entryPoint and return a single outcome. Whenever a value is unspecified, a default value of the required type is used.

executeProgram :: Program -> Context -> Generator Stream -> Maybe Integer -> Id -> [TestCase]Source

executeProgram p tc entryPoint : Execute program p non-deterministically in type context tc starting from procedure entryPoint and return an infinite list of possible outcomes (each either runtime failure or the final variable store). Whenever a value is unspecified, all values of the required type are tried exhaustively.

executeProgramGeneric :: (Monad m, Functor m) => Program -> Context -> Generator m -> Maybe Integer -> Id -> m TestCaseSource

executeProgramGeneric p tc generator qbound entryPoint : Execute program p in type context tc with input generator generator, starting from procedure entryPoint, and return the outcome(s) embedded into the generator's monad.

Run-time failures

data FailureSource Source


SpecViolation SpecClause

Violation of user-defined specification


Division by zero

UnsupportedConstruct String

Language construct is not yet supported (should disappear in later versions)

InfiniteDomain Id Interval

Quantification over an infinite set

MapEquality Value Value

Equality of two maps cannot be determined

InternalException InternalCode

Must be cought inside the interpreter and never reach the user


data StackFrame Source

Information about a procedure or function call




callPos :: SourcePos

Source code position of the call

callName :: Id

Name of procedure or function


data RuntimeFailure Source

Failures that occur during execution




rtfSource :: FailureSource

Source of the failure

rtfPos :: SourcePos

Location where the failure occurred

rtfMemory :: Memory

Memory state at the time of failure

rtfTrace :: StackTrace

Stack trace from the program entry point to the procedure where the failure occurred

runtimeFailureDoc :: Bool -> RuntimeFailure -> DocSource

Pretty-printed run-time failure

data FailureKind Source

Kinds of run-time failures



Error state reached (assertion violation)


Unreachable state reached (assumption violation)


The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter


failureKind :: RuntimeFailure -> FailureKindSource

Kind of a run-time failure

Execution outcomes

data TestCase Source

Description of an execution




tcProcedure :: PSig

Root procedure (entry point) of the execution

tcMemory :: Memory

Final memory state (at the exit from the root procedure)

tcFailure :: Maybe RuntimeFailure

Failure the execution eded with, or Nothing if the execution ended in a valid state

isPass :: TestCase -> BoolSource

isPass tc: Does tc end in a valid state?

isInvalid :: TestCase -> BoolSource

isInvalid tc: Does tc and in an unreachable state?

isNonexecutable :: TestCase -> BoolSource

isNonexecutable tc: Does tc end in a non-executable state?

isFail :: TestCase -> BoolSource

isFail tc: Does tc end in an error state?

testCaseSummary :: Bool -> TestCase -> DocSource

testCaseSummary debug tc : Summary of tc's inputs and outcome, displayed in user or debug format depending on debug

finalStateDoc :: Bool -> TestCase -> DocSource

finalStateDoc debug tc : outputs of tc, displayed in user or debug format depending on debug

data Summary Source

Test session summary




sPassCount :: Int

Number of passing test cases

sFailCount :: Int

Number of failing test cases

sInvalidCount :: Int

Number of invalid test cases

sNonExecutableCount :: Int

Number of nonexecutable test cases

sUniqueFailures :: [TestCase]

Unique failing test cases


testSessionSummary :: [TestCase] -> SummarySource

Summary of a set of test cases

summaryDoc :: Summary -> DocSource

Pretty-printed test session summary

Executing parts of programs

eval :: (Monad m, Functor m) => Expression -> Execution m ValueSource

Evaluate an expression; can have a side-effect of initializing variables that were not previously defined

exec :: (Monad m, Functor m) => Statement -> Execution m ()Source

Execute a basic statement (no jump, if or while statements allowed)

execProcedure :: (Monad m, Functor m) => PSig -> PDef -> [Expression] -> [Expression] -> Execution m [Value]Source

execProcedure sig def args lhss : Execute definition def of procedure sig with actual arguments args and call left-hand sides lhss

preprocess :: (Monad m, Functor m) => Program -> SafeExecution m ()Source

Collect procedure implementations, and constantfunctionglobal variable constraints