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

Safe HaskellNone




Various properties and transformations of Boogie program elements



type TypeBinding = Map Id TypeSource

Mapping from type variables to types

typeSubst :: TypeBinding -> Type -> TypeSource

typeSubst binding t : Substitute all free type variables in t according to binding; all variables in the domain of bindings are considered free if not explicitly bound

renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBindingSource

renameTypeVars tv newTV binding : binding with each occurrence of one of tv replaced with corresponding newTV (in both domain and range)

fromTVNames :: [Id] -> [Id] -> TypeBindingSource

fromTVNames tvs tvs' : type binding that replaces type variables tvs with type variables tvs'

isFreeIn :: Id -> Type -> BoolSource

x isFreeIn t : does x occur free in t?

isTypeVar :: [Id] -> Id -> BoolSource

isTypeVar contextTypeVars v : Is v either one of contextTypeVars or a freash type variable generated by freshTVName?

unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBindingSource

unifier fv xs ys : most general unifier of xs and ys with shared free type variables of the context fv

freshTVName :: Show a => a -> [Char]Source

'freshTVName n : Fresh type variable with a unique identifier n

tupleType :: [Type] -> TypeSource

Internal tuple type constructor (used for representing procedure returns as a single type)


freeVarsTwoState :: Expression -> ([Id], [Id])Source

Free variables in an expression, referred to in current state and old state

freeVars :: Expression -> [Id]Source

Free variables in an expression, in current state

freeOldVars :: Expression -> [Id]Source

Free variables in an expression, in old state

type VarBinding = Map Id BareExpressionSource

Mapping from variables to expressions

exprSubst :: VarBinding -> Expression -> ExpressionSource

exprSubst binding e : substitute all free variables in e according to binding; all variables in the domain of bindings are considered free if not explicitly bound

paramSubst :: PSig -> PDef -> Expression -> ExpressionSource

paramSubst sig def : Substitute parameter names from sig in an expression with their equivalents from def

freeSelections :: Expression -> [(Id, [Expression])]Source

freeSelections expr : all map selections that occur in expr, where the map is a free variable

applications :: Expression -> [(Id, [Expression])]Source

applications expr : all function applications that occur in expr


preconditions :: [Contract] -> [SpecClause]Source

preconditions specs : all precondition clauses in specs

postconditions :: [Contract] -> [SpecClause]Source

postconditions specs : all postcondition clauses in specs

modifies :: [Contract] -> [Id]Source

modifies specs : all modifies clauses in specs

assumePreconditions :: PSig -> PSigSource

Make all preconditions in contracts free

assumePostconditions :: PSig -> PSigSource

Make all postconditions in contracts free

Functions and procedures

data FSig Source

Function signature




fsigName :: Id

Function name

fsigTypeVars :: [Id]

Type variables

fsigArgTypes :: [Type]

Argument types

fsigRetType :: Type

Return type


fsigType :: FSig -> TypeSource

Function signature as a map type

fsigFromType :: Type -> FSigSource

Map type as a function signature

data FDef Source

Function definition




fdefName :: Id

Entity to which the definition belongs

fdefTV :: [Id]

Type variables

fdefArgs :: [IdType]

Arguments (types may be less general than in the corresponding signature)

fdefGuard :: Expression

Condition under which the definition applies

fdefBody :: Expression


type ConstraintSet = ([FDef], [FDef])Source

Constraint set: contains a list of definitions and a list of constraints

type AbstractStore = Map Id ConstraintSetSource

Abstract store: maps names to their constraints

asUnion :: AbstractStore -> AbstractStore -> AbstractStoreSource

Union of abstract stores (values at the same key are concatenated)

data PSig Source

Procedure signature




psigName :: Id

Procedure name

psigTypeVars :: [Id]

Type variables

psigArgs :: [IdTypeWhere]


psigRets :: [IdTypeWhere]


psigContracts :: [Contract]



psigParams :: PSig -> [IdTypeWhere]Source

All parameters of a procedure signature

psigArgTypes :: PSig -> [Type]Source

Types of in-parameters of a procedure signature

psigRetTypes :: PSig -> [Type]Source

Types of out-parameters of a procedure signature

psigModifies :: PSig -> [Id]Source

Modifies clauses of a procedure signature

psigRequires :: PSig -> [SpecClause]Source

Preconditions of a procedure signature

psigEnsures :: PSig -> [SpecClause]Source

Postconditions of a procedure signature

psigType :: PSig -> TypeSource

Procedure signature as a map type

data PDef Source

Procedure definition; a single procedure might have multiple definitions (one per body)




pdefIns :: [Id]

In-parameter names (in the same order as psigArgs in the corresponding signature)

pdefOuts :: [Id]

Out-parameter names (in the same order as psigRets in the corresponding signature)

pdefParamsRenamed :: Bool

Are any parameter names in this definition different for the procedure signature? (used for optimizing parameter renaming, True is a safe default)

pdefBody :: BasicBody


pdefConstraints :: AbstractStore

Constraints on local names

pdefPos :: SourcePos

Location of the (first line of the) procedure definition in the source

pdefLocals :: PDef -> [Id]Source

All local names of a procedure definition

Code generation


interval :: Enum t => (t, t) -> [t]Source

interval (lo, hi) : Interval from lo to hi

fromRight :: Either a b -> bSource

Extract the element out of a Right and throw an error if its argument is Left

deleteAll :: Ord k => [k] -> Map k a -> Map k aSource

deleteAll keys m : map m with keys removed from its domain

restrictDomain :: Ord k => Set k -> Map k a -> Map k aSource

restrictDomain keys m : map m restricted on the set of keys keys

removeDomain :: Ord k => Set k -> Map k a -> Map k aSource

removeDomain keys m : map m with the set of keys keys removed from its domain

anyM :: Monad m => (a -> m Bool) -> [a] -> m BoolSource

Monadic version of any (executes boolean-valued computation for all arguments in a list until the first True is found)

changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m aSource

Execute a computation with state of type t inside a computation with state of type s

withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m aSource

withLocalState localState e : Execute e in current state modified by localState, and then restore current state