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

Safe HaskellSafe-Inferred

Language.Boogie.Util

Contents

Description

Various properties and transformations of Boogie program elements

Synopsis

Types

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

isFreeIn :: Id -> Type -> BoolSource

x isFreeIn t : does x occur as a free type variable in t? x must not be a name of a type constructor

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

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

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

oneSidedUnifier fv xs tv ys : Most general unifier of xs and ys, where only xs contain free variables (fv), while ys contain rigid type variables tv, which might clash with fv

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

boundUnifier fv bv1 xs bv2 ys : Most general unifier of xs and ys, where bv1 are bound type variables in xs and bv2 are bound type variables in ys, and fv are free type variables of the enclosing context

(<==>) :: Type -> Type -> BoolSource

Semantic equivalence on types (equality up to renaming of bound type variables)

Expressions

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

Specs

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

Funstions and procedures

data FSig Source

Function signature

Constructors

FSig 

Fields

fsigName :: Id

Function name

fsigTypeVars :: [Id]

Type variables

fsigArgTypes :: [Type]

Argument types

fsigRetType :: Type

Return type

data FDef Source

Function definition

Constructors

FDef 

Fields

fdefArgs :: [Id]

Argument names (in the same order as fsigArgTypes in the corresponding signature)

fdefGuard :: Expression

Condition under which this definition applies

fdefBody :: Expression

Body

data PSig Source

Procedure signature

Constructors

PSig 

Fields

psigName :: Id

Procedure name

psigTypeVars :: [Id]

Type variables

psigArgs :: [IdTypeWhere]

In-parameters

psigRets :: [IdTypeWhere]

Out-parameters

psigContracts :: [Contract]

Contracts

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

data PDef Source

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

Constructors

PDef 

Fields

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

Body

pdefPos :: SourcePos

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

Code generation

num :: Integer -> Pos BareExpressionSource

eneg :: Pos BareExpression -> Pos BareExpressionSource

enot :: Pos BareExpression -> Pos BareExpressionSource

(|+|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|-|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|*|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|/|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|%|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|!=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|<|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|<=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|>=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|&|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|||) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

(|<=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpressionSource

assume :: Pos BareExpression -> Pos BareStatementSource

Misc

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

mapFst :: (t -> t1) -> (t, t2) -> (t1, t2)Source

mapSnd :: (t -> t2) -> (t1, t) -> (t1, t2)Source

mapBoth :: (t -> t1) -> (t, t) -> (t1, t1)Source

changeState :: (s -> t) -> (t -> s -> s) -> State t a -> State s aSource

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

withLocalState :: (s -> t) -> State t a -> State s aSource

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