language-boogie (empty) → 0.1

raw patch · 18 files changed

+4245/−0 lines, 18 filesdep +HUnitdep +basedep +cmdargssetup-changed

Dependencies added: HUnit, base, cmdargs, containers, filepath, language-boogie, mtl, parsec, pretty, random, time, transformers

Files

• Boogaloo.hs +159/−0
• LICENSE +30/−0
• Language/Boogie/AST.hs +183/−0
• Language/Boogie/BasicBlocks.hs +119/−0
• Language/Boogie/DataFlow.hs +135/−0
• Language/Boogie/Interpreter.hs +846/−0
• Language/Boogie/Intervals.hs +138/−0
• Language/Boogie/NormalForm.hs +80/−0
• Language/Boogie/Parser.hs +510/−0
• Language/Boogie/Position.hs +61/−0
• Language/Boogie/PrettyPrinter.hs +324/−0
• Language/Boogie/Tester.hs +301/−0
• Language/Boogie/Tokens.hs +63/−0
• Language/Boogie/TypeChecker.hs +804/−0
• Language/Boogie/Util.hs +355/−0
• Setup.hs +2/−0
• Tests.hs +92/−0
• language-boogie.cabal +43/−0

@@ -0,0 +1,159 @@+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Main where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position
+import qualified Language.Boogie.Parser as Parser (program)
+import Language.Boogie.TypeChecker
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.Interpreter
+import Language.Boogie.Tester
+import System.Environment
+import System.Console.CmdArgs
+import System.Random
+import Data.Time.Calendar
+import Data.List
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.State
+import Control.Applicative
+import Text.PrettyPrint hiding (mode)
+import Text.ParserCombinators.Parsec (parse, parseFromFile)
+
+programName = "boogaloo"
+versionName = "0.1"
+releaseDate = fromGregorian 2012 10 25
+
+-- | Execute or test a Boogie program, according to command-line arguments
+main = do
+  res <- cmdArgsRun $ mode
+  case res of
+    Exec file entry -> executeFromFile file entry
+    args -> testFromFile (file args) (proc_ args) (testMethod args) (verbose args)
+
+{- Command line arguments -}
+
+data CommandLineArgs
+    = Exec { file :: String, entry :: String }
+    | Test { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), verbose :: Bool  }
+    | RTest { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), tc_count :: Int, seed :: Maybe Int, verbose :: Bool }
+      deriving (Data, Typeable, Show, Eq)
+
+execute = Exec {
+  entry = "Main"  &= help "Program entry point (must not have in- or out-parameters)" &= typ "PROCEDURE",
+  file  = ""      &= typFile &= argPos 0
+  } &= auto &= help "Execute program"
+      
+test_ = Test {
+  proc_   = []      &= help "Procedures to test" &= typ "PROCEDURE",
+  limits  = (-3, 3) &= help "Interval of input values to try for an integer variable" &= typ "NUM, NUM",
+  dlimits = (0, 2)  &= help dlimitsMsg &= typ "NUM, NUM" ,
+  file    = ""      &= typFile &= argPos 0,
+  verbose = False   &= help verboseMsg
+  } &= help "Test program exhaustively"
+  
+rtest = RTest {
+  proc_     = []        &= help "Procedures to test" &= typ "PROCEDURE",
+  limits    = (-32, 32) &= help "Interval of input values to draw from for an integer variable" &= typ "NUM, NUM",
+  dlimits   = (0, 2)    &= help dlimitsMsg &= typ "NUM, NUM",
+  tc_count  = 10        &= help "Number of test cases to generate per procedure implementation" &= name "n" &= typ "NUM",
+  seed      = Nothing   &= help "Seed for the random number generator" &= typ "NUM",
+  file      = ""        &= typFile &= argPos 0,
+  verbose = False       &= help verboseMsg
+  } &= help "Test program on random inputs"
+  
+dlimitsMsg = "Given a map with an integer domain, different range values will be tried for domain values in this interval"
+verboseMsg = "Output all executed test cases"
+    
+mode = cmdArgsMode $ modes [execute, test_, rtest] &= 
+  help "Boogie interpreter" &= 
+  program programName &= 
+  summary (programName ++ " v" ++ versionName ++ ", " ++ showGregorian releaseDate)
+  
+-- | Set up a test method depending on command-line arguments  
+testMethod :: CommandLineArgs -> Program -> Context -> [Id] -> IO [TestCase]
+testMethod (Test _ _ limits dlimits _ ) program context procNames = 
+  let settings = ExhaustiveSettings {
+      esIntRange = interval limits,
+      esIntMapDomainRange = interval dlimits,
+      esGenericTypeRange = defaultGenericTypeRange context,
+      esMapTypeRange = defaultMapTypeRange context
+    }
+  in return $ testProgram settings program context procNames
+testMethod (RTest _ _ limits dlimits tc_count seed _) program context procNames = do
+  defaultGen <- getStdGen
+  randomGen <- case seed of
+    Nothing -> getStdGen
+    Just s -> return $ mkStdGen s
+  let settings = RandomSettings {
+      rsRandomGen = randomGen,
+      rsCount = tc_count,
+      rsIntLimits = limits,
+      rsIntMapDomainRange = interval dlimits,
+      rsGenericTypeRange = defaultGenericTypeRange context,
+      rsMapTypeRange = defaultMapTypeRange context     
+    }  
+  return $ testProgram settings program context procNames
+    
+{- Interfacing internal modules -}
+
+-- | Execute procedure entryPoint from file
+-- | and output either errors or the final values of global variables
+executeFromFile :: String -> String -> IO ()
+executeFromFile file entryPoint = runOnFile printFinalState file
+  where
+    printFinalState p context = case M.lookup entryPoint (ctxProcedures context) of
+      Nothing -> print (text "Cannot find program entry point" <+> text entryPoint)
+      Just sig -> if not (goodEntryPoint sig)
+        then print (text "Program entry point" <+> text entryPoint <+> text "does not have the required signature" <+> doubleQuotes (sigDoc [] []))
+        else case executeProgram p context entryPoint of
+          Left err -> print err
+          Right env -> (print . varsDoc . envGlobals) env
+    goodEntryPoint sig = null (psigTypeVars sig) && null (psigArgTypes sig) && null (psigRetTypes sig)
+
+-- | Test procedures procNames from file with a testMethod
+-- | and output the test outcomes
+testFromFile :: String -> [String] -> (Program -> Context -> [String] -> IO [TestCase]) -> Bool -> IO ()
+testFromFile file procNames testMethod printAll = runOnFile printTestOutcomes file
+  where
+    printTestOutcomes p context = do
+      let (present, missing) = partition (`M.member` ctxProcedures context) procNames
+      when (not (null missing)) $ print (text "Cannot find procedures under test:" <+> commaSep (map text missing))
+      testResults <- testMethod p context present
+      print $ testSessionSummary testResults
+      when printAll $ putStr "\n" >> mapM_ print testResults
+
+-- | Parse file, type-check the resulting program, then execute command on the resulting program and type context
+runOnFile :: (Program -> Context -> IO ()) -> String -> IO ()      
+runOnFile command file = do 
+  parseResult <- parseFromFile Parser.program file
+  case parseResult of
+    Left parseErr -> print parseErr
+    Right p -> case checkProgram p of
+      Left typeErrs -> print (typeErrorsDoc typeErrs)
+      Right context -> command p context
+      
+{- Helpers for testing internal functions -}      
+      
+-- | Harness for testing various internal functions
+harness file = runOnFile printOutcome file
+  where
+    printOutcome p context = do
+      let env = execState (collectDefinitions p) emptyEnv { envTypeContext = context }
+      print $ envGlobals env
+      
+-- | Test that print . parse == print . parse . print .parse      
+testParser :: String -> IO ()      
+testParser file = do
+  result <- parseFromFile Parser.program file
+  case (result) of
+    Left err -> print err
+    Right p -> do
+      case parse Parser.program ('*' : file) (show p) of
+        Left err -> print err
+        Right p' -> if p == p'
+          then putStr ("Passed.\n")
+          else putStr ("Failed with different ASTs.\n")
+          

@@ -0,0 +1,30 @@+Copyright (c) 2012, Nadia Polikarpova
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Nadia Polikarpova nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,183 @@+-- | Abstract syntax tree for Boogie 2
+module Language.Boogie.AST where
+
+import Language.Boogie.Position
+import Data.Map (Map)
+
+{- Basic -}
+
+-- | Program: a list of top-level declarations
+newtype Program = Program [Decl]
+  deriving Eq
+
+{- Types -}
+
+-- | Type
+data Type = BoolType | IntType |
+  MapType [Id] [Type] Type |
+  Instance Id [Type]
+  deriving Eq -- syntactic equality
+
+-- | 'nullaryType' @id@ : type denoted by @id@ without arguments
+nullaryType id = Instance id []
+
+-- | Dummy type used during type checking to denote error
+noType = nullaryType "NoType"
+
+{- Expressions -}
+
+-- | Unary operators
+data UnOp = Neg | Not
+  deriving Eq
+
+-- | Binary operators  
+data BinOp = Plus | Minus | Times | Div | Mod | And | Or | Implies | Explies | Equiv | Eq | Neq | Lc | Ls | Leq | Gt | Geq
+  deriving Eq
+
+-- | Quantifiers
+data QOp = Forall | Exists | Lambda
+  deriving Eq
+  
+-- | Expression with a source position attached  
+type Expression = Pos BareExpression
+  
+-- | Expression
+data BareExpression = FF |                        -- ^ false
+  TT |                                            -- ^ true
+  Numeral Integer |                               -- ^ 'Numeral' @value@
+  Var Id |                                        -- ^ 'Var' @name@
+  Application Id [Expression] |                   -- ^ 'Application' @f args@
+  MapSelection Expression [Expression] |          -- ^ 'MapSelection' @map indexes@
+  MapUpdate Expression [Expression] Expression |  -- ^ 'MapUpdate' @map indexes rhs@
+  Old Expression |
+  IfExpr Expression Expression Expression |       -- ^ 'IfExpr' @cond eThen eElse@
+  Coercion Expression Type |
+  UnaryExpression UnOp Expression |
+  BinaryExpression BinOp Expression Expression |
+  Quantified QOp [Id] [IdType] Expression         -- ^ 'Quantified' @qop type_vars bound_vars expr@
+  deriving Eq -- syntactic equality
+  
+-- | 'mapSelectExpr' @m args@ : map selection expression with position of @m@ attached
+mapSelectExpr m args = attachPos (position m) (MapSelection m args)  
+  
+-- | Wildcard or expression  
+data WildcardExpression = Wildcard | Expr Expression
+  deriving Eq
+  
+{- Statements -}
+
+-- | Statement with a source position attached  
+type Statement = Pos BareStatement
+
+-- | Statement
+data BareStatement = Predicate SpecClause |      -- ^ Predicate statement (assume or assert)
+  Havoc [Id] |                                   -- ^ 'Havoc' @var_names@
+  Assign [(Id , [[Expression]])] [Expression] |  -- ^ 'Assign' @var_map_selects rhss@
+  Call [Id] Id [Expression] |                    -- ^ 'Call' @lhss proc_name args@
+  CallForall Id [WildcardExpression] |           -- ^ 'CallForall' @proc_name args@
+  If WildcardExpression Block (Maybe Block) |    -- ^ 'If' @wild_or_expr then_block else_block@
+  While WildcardExpression [SpecClause] Block |  -- ^ 'While' @wild_or_expr free_loop_inv loop_body@
+  Break (Maybe Id) |                             -- ^ 'Break' @label@
+  Return |
+  Goto [Id] |                                    -- ^ 'Goto' @labels@
+  Skip                                           -- ^ only used at the end of a block
+  deriving Eq -- syntactic equality
+
+-- | Statement labeled by multiple labels with a source position attached  
+type LStatement = Pos BareLStatement
+
+-- | Statement labeled by multiple labels
+type BareLStatement = ([Id], Statement)
+
+-- | Statement block
+type Block = [LStatement] 
+
+-- | Block consisting of a single non-labeled statement
+singletonBlock s = [attachPos (position s) ([], s)]
+
+-- | Procedure body: consists of local variable declarations and a statement block
+type Body = ([[IdTypeWhere]], Block)
+
+-- | Basic block is a list of statements labeled by a single label;
+-- the list contains no jump, if or while statements,
+-- except for the last statement, which can be a goto or return
+type BasicBlock = (Id, [Statement])
+
+-- | Procedure body transformed to basic blocks:
+-- consists of local variable declarations and a set of basic blocks
+-- (represented as a map from their labels to statement lists)
+type BasicBody = ([IdTypeWhere], Map Id [Statement])
+
+{- Specs -}
+
+-- | Types of specification clauses
+data SpecType = Inline | Precondition | Postcondition | LoopInvariant | Where
+  deriving Eq
+
+-- | Specification clause
+data SpecClause = SpecClause {
+  specType :: SpecType,   -- ^ Source of the clause
+  specFree :: Bool,       -- ^ Is it free (assumption) or checked (assertions)?
+  specExpr :: Expression  -- ^ Boolean expression
+  } deriving Eq
+
+-- | Procedure contract clause 
+data Contract = Requires Bool Expression |  -- ^ 'Requires' @e free@
+  Modifies Bool [Id] |                      -- ^ 'Modifies' @var_names free@
+  Ensures Bool Expression                   -- ^ 'Ensures' @e free@
+  deriving Eq
+
+{- Declarations -}
+
+-- | Top-level declaration with a source position attached  
+type Decl = Pos BareDecl
+
+-- | Top-level declaration
+data BareDecl = 
+  TypeDecl [NewType] |
+  ConstantDecl Bool [Id] Type ParentInfo Bool |                                -- ^ 'ConstantDecl' @unique names type orderSpec complete@
+  FunctionDecl Id [Id] [FArg] FArg (Maybe Expression) |                        -- ^ 'FunctionDecl' @name type_args formals ret body@
+  AxiomDecl Expression |
+  VarDecl [IdTypeWhere] |
+  ProcedureDecl Id [Id] [IdTypeWhere] [IdTypeWhere] [Contract] (Maybe Body) |  -- ^ 'ProcedureDecl' @name type_args formals rets contract body@
+  ImplementationDecl Id [Id] [IdType] [IdType] [Body]                          -- ^ 'ImplementationDecl' @name type_args formals rets body@
+  deriving Eq
+  
+{- Misc -}
+
+-- | Identifier
+type Id = String
+
+-- | Definition of a type
+data NewType = NewType {
+  tId :: Id,
+  tArgs :: [Id],
+  tValue :: Maybe Type
+  } deriving Eq
+
+-- | Name declaration (identifier, type)
+type IdType = (Id, Type)
+
+-- | Name declaration with a where clause
+data IdTypeWhere = IdTypeWhere { 
+  itwId :: Id, 
+  itwType :: Type, 
+  itwWhere :: Expression 
+  } deriving Eq
+  
+-- | Strip the where clause  
+noWhere itw = (itwId itw, itwType itw)  
+  
+-- | Formal argument of a function  
+type FArg = (Maybe Id, Type)
+
+-- | Argument name used for unnamed function arguments
+-- (does not matter, because it is never referred to from function's body)  
+dummyFArg = ""
+
+-- | Parent edge of a constant declaration (uniqueness, parent name)
+type ParentEdge = (Bool, Id)
+
+-- | Parent information in a constant declaration
+-- (Nothing means no information, while empty list means no parents)
+type ParentInfo = Maybe [ParentEdge]

@@ -0,0 +1,119 @@+-- | Basic block transformation for imperative Boogie code
+module Language.Boogie.BasicBlocks (toBasicBlocks, startLabel) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.State
+import Control.Applicative
+
+-- | Transform procedure body into a sequence of basic blocks.
+-- A basic block starts with a label and contains no jump, if or while statements,
+-- except for the last statement, which can be a goto or return.
+toBasicBlocks :: Block -> [BasicBlock]
+toBasicBlocks body = let 
+  tbs = evalState (concat <$> (mapM (transform M.empty) (map node body))) 0
+  -- By the properties of transform, tbs' is a sequence of basic blocks
+  tbs' = attach startLabel (tbs ++ [justBareStatement Return])  
+  -- Append a labeled statement to a sequence of basic blocks
+  -- (the first labeled statement cannot have empty label)
+  append :: [BasicBlock] -> BareLStatement -> [BasicBlock]
+  append bbs ([l], Pos _ Skip) = (l, []) : bbs
+  append bbs ([l], s) = (l, [s]) : bbs
+  append ((l, ss) : bbs) ([], s) = (l, ss ++ [s]) :  bbs  
+  in
+    -- First flatten control flow with transform, and then convert to basic blocks
+    reverse (foldl append [] tbs')
+
+-- | Label of the first block in a procedure
+startLabel = "00_start"    
+
+-- | Attach a label to the first statement (with an empty label) in a non-empty list of labeled statements    
+attach :: Id -> [BareLStatement] -> [BareLStatement]
+attach l (([], stmts) : lsts) = ([l], stmts) : lsts
+
+-- | LStatement with no label (no source position, generated)
+justBareStatement s = ([], gen s)
+
+-- | LStatement with no label (with a source position, derived from a source statement)
+justStatement pos s = ([], Pos pos s)
+
+-- | LStatement with no statement
+justLabel l = ([l], gen Skip)
+
+-- | Special label value that denoted the innermost loop (used for break) 
+innermost = "innermost"
+
+-- | genFreshLabel kind i: returns a label of kind with id i and the id for the next label
+genFreshLabel :: String -> Int -> (String, Int)
+genFreshLabel kind i = (show i ++ "_" ++ kind, i + 1)
+
+-- | transform m statement: transform statement into a sequence of basic blocks;
+-- m is a map from statement labels to labels of their exit points (used for break)
+transform :: Map Id Id -> BareLStatement -> State Int [BareLStatement]  
+transform m (l:lbs, Pos p Skip) = do
+  t <- transform m (lbs, Pos p Skip)
+  return $ (justBareStatement $ Goto [l]) : attach l t
+transform m (l:lbs, stmt) = do
+  lDone <- state $ genFreshLabel "done"
+  t <- transform (M.insert l lDone m) (lbs, stmt)
+  return $ [justBareStatement $ Goto [l]] ++ attach l t ++ [justBareStatement $ Goto [lDone], justLabel lDone]
+transform m ([], Pos p stmt) = case stmt of  
+  Goto lbs -> do
+    lUnreach <- state $ genFreshLabel "unreachable"
+    return $ [justStatement p (Goto lbs), justLabel lUnreach]
+  Break (Just l) -> do
+    lUnreach <- state $ genFreshLabel "unreachable"
+    return $ [justStatement p (Goto [m ! l]), justLabel lUnreach]
+  Break Nothing -> do
+    lUnreach <- state $ genFreshLabel "unreachable"
+    return $ [justStatement p (Goto [m ! innermost]), justLabel lUnreach]
+  Return -> do
+    lUnreach <- state $ genFreshLabel "unreachable"
+    return $ [justStatement p Return, justLabel lUnreach]
+  If cond thenBlock Nothing -> transform m (justStatement p (If cond thenBlock (Just [])))
+  If we thenBlock (Just elseBlock) -> do
+    lThen <- state $ genFreshLabel "then"
+    lElse <- state $ genFreshLabel "else"
+    lDone <- state $ genFreshLabel "done"
+    t1 <- transBlock m thenBlock
+    t2 <- transBlock m elseBlock
+    case we of
+      Wildcard -> return $ 
+        [justBareStatement $ Goto [lThen, lElse]] ++ 
+        attach lThen (t1 ++ [justBareStatement $ Goto [lDone]]) ++
+        attach lElse (t2 ++ [justBareStatement $ Goto [lDone]]) ++
+        [justLabel lDone]
+      Expr e -> return $
+        [justBareStatement $ Goto [lThen, lElse]] ++
+        [([lThen], assume e)] ++ t1 ++ [justBareStatement $ Goto [lDone]] ++
+        [([lElse], assume (enot e))] ++ t2 ++ [justBareStatement $ Goto [lDone]] ++
+        [justLabel lDone]      
+  While Wildcard invs body -> do
+    lHead <- state $ genFreshLabel "head"
+    lBody <- state $ genFreshLabel "body"
+    lDone <- state $ genFreshLabel "done"
+    t <- transBlock (M.insert innermost lDone m) body
+    return $
+      [justBareStatement $ Goto [lHead]] ++
+      attach lHead (map checkInvariant invs ++ [justBareStatement $ Goto [lBody, lDone]]) ++ 
+      attach lBody (t ++ [justBareStatement $ Goto [lHead]]) ++
+      [justLabel lDone]
+  While (Expr e) invs body -> do
+    lHead <- state $ genFreshLabel "head"
+    lBody <- state $ genFreshLabel "body"
+    lGDone <- state $ genFreshLabel "guarded_done"
+    lDone <- state $ genFreshLabel "done"
+    t <- transBlock (M.insert innermost lDone m) body
+    return $
+      [justBareStatement $ Goto [lHead]] ++
+      attach lHead (map checkInvariant invs ++ [justBareStatement $ Goto [lBody, lGDone]]) ++
+      [([lBody], assume e)] ++ t ++ [justBareStatement $ Goto [lHead]] ++
+      [([lGDone], assume (enot e))] ++ [justBareStatement $ Goto [lDone]] ++
+      [justLabel lDone]    
+  _ -> return [justStatement p stmt]  
+  where
+    transBlock m b = concat <$> mapM (transform m) (map node b)
+    checkInvariant inv = justStatement (position (specExpr inv)) (Predicate inv)

@@ -0,0 +1,135 @@+-- | Data-flow analysis on Boogie code
+module Language.Boogie.DataFlow (liveVariables, liveInputVariables) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position hiding (gen)
+import Language.Boogie.BasicBlocks
+import Data.List
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+
+{- Interface -}
+
+-- | 'liveInputVariables' @sig def@ : 
+-- Input parameters (in the order they appear in @sig@) and global names, 
+-- whose initial value might be read by the procedure implementation @def@
+liveInputVariables :: PSig -> PDef -> ([Id], [Id])
+liveInputVariables sig def = let
+  body = pdefBody def
+  liveVars = liveVariables (attachContractChecks sig def)
+  liveLocals = filter (`elem` liveVars) (map itwId (fst body))
+  liveIns = filter (`elem` liveVars) (pdefIns def)
+  liveOuts = filter (`elem` liveVars) (pdefOuts def)
+  liveGlobals = liveVars \\ (liveLocals ++ liveIns ++ liveOuts)
+  in (liveIns, liveGlobals)
+  
+-- | Identifiers whose initial value might be read in body
+liveVariables :: Map Id [Statement] -> [Id]
+liveVariables body = let
+    empty = M.map (const S.empty) body
+    insertExitBlock i = M.insert i (transition (body ! i) S.empty)
+    entry0 = S.foldr insertExitBlock empty (exitBlocks body)
+    changed0 = M.keysSet body <-> exitBlocks body
+    oldVariables = S.unions (map (\block -> S.unions (map genOld block)) (M.elems body))
+  in S.toList (oldVariables `S.union` (analyse body entry0 empty changed0 ! startLabel))
+
+{- Implementation -}
+
+-- | Analyse live variable in body, 
+-- starting from live variables at the entry to each block entry,
+-- live variables at the exit of each block exit,
+-- and the set of blocks whose exit set might have changed changed.
+analyse :: Map Id [Statement] -> Map Id (Set Id) -> Map Id (Set Id) -> Set Id -> Map Id (Set Id)
+analyse body entry exit changed = if S.null changed
+  then entry
+  else let 
+      (i, changed') = S.deleteFindMax changed
+      newExit = setUnions $ S.map (entry !) (successors body i)
+      newEntry = transition (body ! i) newExit
+      exit' = M.insert i newExit exit
+      entry' = M.insert i newEntry entry
+      changed'' = if entry ! i == newEntry then changed' else changed' <+> predecessors body i
+    in analyse body entry' exit' changed''
+
+(<+>) = (S.union)
+(<->) = (S.\\)
+-- | Union of a set of sets
+setUnions sets = S.foldl S.union S.empty sets
+
+-- | Variables that are live before a sequence of statements sts,
+-- if the final live variables are exit
+transition :: [Statement] -> Set Id -> Set Id
+transition sts exit = foldr transition1 exit sts
+  where
+    transition1 st exit = exit <-> kill st <+> gen st
+
+-- | Variables that are not live anymore as a result of st    
+kill :: Statement -> Set Id
+kill st = case node st of
+  Havoc ids     -> S.fromList ids
+  Assign lhss _ -> S.fromList (map fst lhss)
+  Call lhss _ _ -> S.fromList lhss
+  otherwise -> S.empty
+
+-- | Variables that become live as a result of st
+gen :: Statement -> Set Id
+gen st = genTwoState fst st
+
+-- | Variables whose pre-state is mentioned in st
+genOld :: Statement -> Set Id
+genOld st = genTwoState snd st
+  
+-- | Variables mentioned in st in either current state or old state
+genTwoState :: (([Id], [Id]) -> [Id]) -> Statement -> Set Id
+genTwoState select st = case node st of
+  Predicate (SpecClause _ _ e) -> (S.fromList . select . freeVarsTwoState) e
+  Assign lhss rhss -> let 
+    allSubscipts = concat $ concatMap snd lhss
+    subsciptedLhss = [fst lhs | lhs <- lhss, not (null (snd lhs))] -- Left-hand sides with a subscript are also read (consider desugaring)
+    in S.unions (map (S.fromList . select . freeVarsTwoState) (rhss ++ allSubscipts)) <+> S.fromList subsciptedLhss
+  Call _ _ args -> S.unions (map (S.fromList . select . freeVarsTwoState) args)
+  CallForall _ args -> S.unions (map (S.fromList . select . freeVarsTwoState') args)
+  otherwise -> S.empty
+  where 
+    freeVarsTwoState' Wildcard = ([], [])
+    freeVarsTwoState' (Expr e) = freeVarsTwoState e
+    
+-- | Blocks in body that end with a return statement
+exitBlocks :: Map Id [Statement] -> Set Id
+exitBlocks body = M.keysSet $ M.filter isExit body
+  where
+    isExit block = case node (last block) of
+      Return -> True
+      _ -> False
+      
+-- | Blocks in body that have an outgoing edge to label
+predecessors :: Map Id [Statement] -> Id -> Set Id
+predecessors body label = M.keysSet $ M.filter (goesTo label) body
+  where
+    goesTo label block = case node (last block) of
+      Goto lbs -> label `elem` lbs
+      _ -> False
+      
+-- | Blocks in body that have an incoming edge from label  
+successors :: Map Id [Statement] -> Id -> Set Id
+successors body label = case node (last (body ! label)) of
+  Goto lbs -> S.fromList lbs
+  _ -> S.empty
+  
+-- | Body of the implementation def of procedure sig with pre- and postcondition checks embedded;
+-- (used to extract live variables from contracts)
+attachContractChecks :: PSig -> PDef -> Map Id [Statement]
+attachContractChecks sig def = let
+  preChecks = map (attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
+  postChecks = map (attachPos (pdefPos def) . Predicate . subst sig) (psigEnsures sig)
+  subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
+  attachPreChecks = M.adjust (preChecks ++) startLabel (snd (pdefBody def))
+  attachPostChecks block = let jump = last block
+    in case node jump of
+      Return -> init block ++ postChecks ++ [jump]
+      _ -> block
+  in M.map attachPostChecks attachPreChecks  
+      

@@ -0,0 +1,846 @@+{-# LANGUAGE FlexibleContexts #-}
+
+-- | Interpreter for Boogie 2
+module Language.Boogie.Interpreter (
+  -- * Executing programs
+  executeProgram,
+  -- * State
+  Value (..),
+  Environment (..),
+  emptyEnv,
+  lookupFunction,
+  lookupProcedure,
+  modifyTypeContext,
+  setV,
+  setAll,
+  -- * Executions
+  Execution,
+  SafeExecution,
+  execSafely,
+  execUnsafely,
+  -- * Run-time failures
+  FailureSource (..),
+  InternalCode,
+  StackFrame (..),
+  StackTrace,
+  RuntimeFailure (..),  
+  FailureKind (..),
+  failureKind,
+  -- * Executing parts of programs
+  eval,
+  exec,
+  execProcedure,
+  collectDefinitions,
+  -- * Pretty-printing
+  valueDoc,
+  varsDoc,
+  functionsDoc,
+  runtimeFailureDoc
+  ) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Intervals
+import Language.Boogie.Position
+import Language.Boogie.Tokens (nonIdChar)
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.TypeChecker
+import Language.Boogie.NormalForm
+import Language.Boogie.BasicBlocks
+import Data.List
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.Error hiding (join)
+import Control.Applicative hiding (empty)
+import Control.Monad.State hiding (join)
+import Text.PrettyPrint
+
+{- Interface -}
+
+-- | 'executeProgram' @p tc entryPoint@ :
+-- Execute program @p@ in type context @tc@ starting from procedure @entryPoint@, 
+-- and return the final environment;
+-- requires that @entryPoint@ have no in- or out-parameters
+executeProgram :: Program -> Context -> Id -> Either RuntimeFailure Environment
+executeProgram p tc entryPoint = finalEnvironment
+  where
+    initEnvironment = emptyEnv { envTypeContext = tc }
+    finalEnvironment = case runState (runErrorT programExecution) initEnvironment of
+      (Left err, _) -> Left err
+      (_, env)      -> Right env            
+    programExecution = do
+      execUnsafely $ collectDefinitions p
+      execCall [] entryPoint [] noPos
+              
+{- State -}
+
+-- | Run-time value
+data Value = IntValue Integer |   -- ^ Integer value
+  BoolValue Bool |                -- ^ Boolean value
+  MapValue (Map [Value] Value) |  -- ^ Value of a map type
+  CustomValue Integer             -- ^ Value of a user-defined type (values with the same code are considered equal)
+  deriving (Eq, Ord)
+      
+-- | Default value of a type (used to initialize variables)  
+defaultValue :: Type -> Value
+defaultValue BoolType         = BoolValue False  
+defaultValue IntType          = IntValue 0
+defaultValue (MapType _ _ _)  = MapValue M.empty
+defaultValue (Instance _ _)   = CustomValue 0
+
+-- | Pretty-printed value
+valueDoc :: Value -> Doc
+valueDoc (IntValue n) = integer n
+valueDoc (BoolValue False) = text "false"
+valueDoc (BoolValue True) = text "true"
+valueDoc (MapValue m) = brackets (commaSep (map itemDoc (M.toList m)))
+  where itemDoc (keys, v) = commaSep (map valueDoc keys) <+> text "->" <+>  valueDoc v
+valueDoc (CustomValue n) = text "custom_" <> integer n
+
+instance Show Value where
+  show v = show (valueDoc v)
+
+-- | Execution state
+data Environment = Environment
+  {
+    envLocals :: Map Id Value,          -- ^ Local variable names to values
+    envGlobals :: Map Id Value,         -- ^ Global variable names to values
+    envOld :: Map Id Value,             -- ^ Global variable names to old values (in two-state contexts)
+    envConstants :: Map Id Expression,  -- ^ Constant names to expressions
+    envFunctions :: Map Id [FDef],      -- ^ Function names to definitions
+    envProcedures :: Map Id [PDef],     -- ^ Procedure names to definitions
+    envTypeContext :: Context           -- ^ Type context
+  }
+   
+-- | Empty environment   
+emptyEnv = Environment
+  {
+    envLocals = M.empty,
+    envGlobals = M.empty,
+    envOld = M.empty,
+    envConstants = M.empty,
+    envFunctions = M.empty,
+    envProcedures = M.empty,
+    envTypeContext = emptyContext
+  }
+  
+-- | 'lookupFunction' @id env@ : All definitions of function @id@ in @env@
+lookupFunction id env = case M.lookup id (envFunctions env) of
+  Nothing -> []
+  Just defs -> defs    
+  
+-- | 'lookupProcedure' @id env@ : All definitions of procedure @id@ in @env@  
+lookupProcedure id env = case M.lookup id (envProcedures env) of
+  Nothing -> []
+  Just defs -> defs  
+
+setGlobal id val env = env { envGlobals = M.insert id val (envGlobals env) }    
+setLocal id val env = env { envLocals = M.insert id val (envLocals env) }
+addConstantDef id def env = env { envConstants = M.insert id def (envConstants env) }
+addFunctionDefs id defs env = env { envFunctions = M.insert id (lookupFunction id env ++ defs) (envFunctions env) }
+addProcedureDef id def env = env { envProcedures = M.insert id (def : (lookupProcedure id env)) (envProcedures env) } 
+modifyTypeContext f env = env { envTypeContext = f (envTypeContext env) }
+
+-- | Pretty-printed mapping of variables to values
+varsDoc :: Map Id Value -> Doc
+varsDoc vars = vsep $ map varDoc (M.toList vars)
+  where varDoc (id, val) = text id <+> text "=" <+> valueDoc val
+  
+-- | Pretty-printed set of function definitions
+functionsDoc :: Map Id [FDef] -> Doc  
+functionsDoc funcs = vsep $ map funcDoc (M.toList funcs)
+  where 
+    funcDoc (id, defs) = vsep $ map (funcsDefDoc id) defs
+    funcsDefDoc id (FDef formals guard body) = exprDoc guard <+> text "->" <+> 
+      text id <> parens (commaSep (map text formals)) <+> text "=" <+> exprDoc body
+      
+{- Executions -}
+
+-- | Computations with 'Environment' as state, which can result in either @a@ or 'RuntimeFailure'
+type Execution a = ErrorT RuntimeFailure (State Environment) a
+
+-- | Computations with 'Environment' as state, which always result in @a@
+type SafeExecution a = State Environment a
+
+-- | 'execUnsafely' @computation@ : Execute a safe @computation@ in an unsafe environment
+execUnsafely :: SafeExecution a -> Execution a
+execUnsafely computation = ErrorT (Right <$> computation)
+
+-- | 'execSafely' @computation handler@ : Execute an unsafe @computation@ in a safe environment, handling errors that occur in @computation@ with @handler@
+execSafely :: Execution a -> (RuntimeFailure -> SafeExecution a) -> SafeExecution a
+execSafely computation handler = do
+  eres <- runErrorT computation
+  either handler return eres
+  
+-- | Computations that perform a cleanup at the end
+class Monad m => Finalizer m where
+  finally :: m a -> m () -> m a
+    
+instance (Monad m) => Finalizer (StateT s m) where
+  finally main cleanup = do
+    res <- main
+    cleanup
+    return res
+
+instance (Error e, Monad m) => Finalizer (ErrorT e m) where
+  finally main cleanup = do
+    res <- main `catchError` (\err -> cleanup >> throwError err)
+    cleanup
+    return res  
+          
+-- | 'setV' @id val@ : set value of variable @id@ to @val@;
+-- @id@ has to be declared in the current type context
+setV id val = do
+  tc <- gets envTypeContext
+  if M.member id (localScope tc)
+    then modify $ setLocal id val
+    else modify $ setGlobal id val      
+    
+-- | 'setAll' @ids vals@ : set values of variables @ids@ to @vals@;
+-- all @ids@ have to be declared in the current type context
+setAll ids vals = zipWithM_ setV ids vals
+
+-- | Run execution in the old environment
+old :: Execution a -> Execution a
+old execution = do
+  env <- get
+  put env { envGlobals = envOld env }
+  res <- execution
+  put env
+  return res
+
+-- | Save current values of global variables in the "old" environment, return the previous "old" environment
+saveOld :: Execution (Map Id Value)  
+saveOld = do
+  env <- get
+  put env { envOld = envGlobals env }
+  return $ envOld env
+
+-- | Set the "old" environment to olds  
+restoreOld :: Map Id Value -> Execution ()  
+restoreOld olds = do
+  env <- get
+  put env { envOld = olds }
+  
+-- | Enter local scope (apply localTC to the type context and assign actuals to formals),
+-- execute computation,
+-- then restore type context and local variables to their initial values
+executeLocally :: (MonadState Environment m, Finalizer m) => (Context -> Context) -> [Id] -> [Value] -> m a -> m a
+executeLocally localTC formals actuals computation = do
+  oldEnv <- get
+  modify $ modifyTypeContext localTC
+  setAll formals actuals
+  computation `finally` unwind oldEnv
+  where
+    -- | Restore type context and the values of local variables 
+    unwind oldEnv = do
+      env <- get
+      put env { envTypeContext = envTypeContext oldEnv, envLocals = envLocals oldEnv }
+              
+{- Nondeterminism -}  
+  
+-- | Generate a value of type t,
+-- such that when it is set, guard does not fail.
+-- Fail if cannot find such a value.
+-- (So far just returns the default value, but will be more elaborate in the future)
+generateValue :: Type -> (Value -> Execution ()) -> (Execution ()) -> Execution Value          
+generateValue t set guard = let newValue = defaultValue t in
+  do
+    set newValue 
+    guard
+    return newValue  
+  
+{- Runtime failures -}
+
+data FailureSource = 
+  SpecViolation SpecClause |    -- ^ Violation of user-defined specification
+  DivisionByZero |              -- ^ Division by zero  
+  UnsupportedConstruct String | -- ^ Language construct is not yet supported (should disappear in later versions)
+  InfiniteDomain Id Interval |  -- ^ Quantification over an infinite set
+  NoImplementation Id |         -- ^ Call to a procedure with no implementation
+  InternalFailure InternalCode  -- ^ Must be cought inside the interpreter and never reach the user
+  deriving Eq
+
+-- | Information about a procedure or function call  
+data StackFrame = StackFrame {
+  callPos :: SourcePos, -- ^ Source code position of the call
+  callName :: Id        -- ^ Name of procedure or function
+} deriving Eq
+
+type StackTrace = [StackFrame]
+
+-- | Failures that occur during execution
+data RuntimeFailure = RuntimeFailure {
+  rtfSource :: FailureSource,   -- ^ Source of the failure
+  rtfPos :: SourcePos,          -- ^ Location where the failure occurred
+  rtfEnv :: Environment,        -- ^ Environment at the time of failure
+  rtfTrace :: StackTrace        -- ^ Stack trace from the program entry point to the procedure where the failure occurred
+}
+
+-- | Throw a run-time failure
+throwRuntimeFailure source pos = do
+  env <- get
+  throwError (RuntimeFailure source pos env [])
+
+-- | Push frame on the stack trace of a runtime failure
+addStackFrame frame (RuntimeFailure source pos env trace) = throwError (RuntimeFailure source pos env (frame : trace))
+
+-- | Kinds of run-time failures
+data FailureKind = Error | -- ^ Error state reached (assertion violation)
+  Unreachable | -- ^ Unreachable state reached (assumption violation)
+  Nonexecutable -- ^ The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter
+  deriving Eq
+
+-- | Kind of a run-time failure
+failureKind :: RuntimeFailure -> FailureKind
+failureKind err = case rtfSource err of
+  SpecViolation (SpecClause _ True _) -> Unreachable
+  SpecViolation (SpecClause _ False _) -> Error
+  DivisionByZero -> Error
+  _ -> Nonexecutable
+  
+instance Error RuntimeFailure where
+  noMsg    = RuntimeFailure (UnsupportedConstruct "unknown") noPos emptyEnv []
+  strMsg s = RuntimeFailure (UnsupportedConstruct s) noPos emptyEnv []
+  
+-- | Pretty-printed run-time failure
+runtimeFailureDoc err = failureSourceDoc (rtfSource err) <+> posDoc (rtfPos err) $+$ 
+  text "with" <+> varsDoc revelantVars $+$
+  vsep (map stackFrameDoc (reverse (rtfTrace err)))
+  where
+    failureSourceDoc (SpecViolation (SpecClause specType isFree e)) = text (clauseName specType isFree) <+> doubleQuotes (exprDoc e) <+> defPosition specType e <+> text "violated"
+    failureSourceDoc (DivisionByZero) = text "Division by zero"
+    failureSourceDoc (InfiniteDomain var int) = text "Variable" <+> text var <+> text "quantified over an infinite domain" <+> text (show int)
+    failureSourceDoc (NoImplementation name) = text "Procedure" <+> text name <+> text "with no implementation called"
+    failureSourceDoc (UnsupportedConstruct s) = text "Unsupported construct" <+> text s
+    
+    clauseName Inline isFree = if isFree then "Assumption" else "Assertion"  
+    clauseName Precondition isFree = if isFree then "Free precondition" else "Precondition"  
+    clauseName Postcondition isFree = if isFree then "Free postcondition" else "Postcondition"  
+    clauseName LoopInvariant isFree = if isFree then "Free loop invariant" else "Loop invariant"  
+    clauseName Where True = "Where clause"  -- where clauses cannot be non-free  
+    
+    defPosition Inline _ = empty
+    defPosition LoopInvariant _ = empty
+    defPosition _ e = text "defined" <+> posDoc (position e)
+    
+    revelantVars = let env = rtfEnv err      
+      in M.filterWithKey (\k _ -> isRelevant k) (envLocals env `M.union` envGlobals env)
+      
+    isRelevant k = case rtfSource err of
+      SpecViolation (SpecClause _ _ expr) -> k `elem` freeVars expr
+      _ -> False
+    
+    stackFrameDoc f = text "in call to" <+> text (callName f) <+> posDoc (callPos f)
+    posDoc pos
+      | pos == noPos = text "from the environment"
+      | otherwise = text "at" <+> text (sourceName pos) <+> text "line" <+> int (sourceLine pos)
+
+instance Show RuntimeFailure where
+  show err = show (runtimeFailureDoc err)
+  
+-- | Internal error codes 
+data InternalCode = NotLinear
+  deriving Eq
+
+throwInternalFailure code = throwRuntimeFailure (InternalFailure code) noPos
+
+{- Expressions -}
+
+-- | Semantics of unary operators
+unOp :: UnOp -> Value -> Value
+unOp Neg (IntValue n)   = IntValue (-n)
+unOp Not (BoolValue b)  = BoolValue (not b)
+
+-- | Semi-strict semantics of binary operators:
+-- 'binOpLazy' @op lhs@ : returns the value of @lhs op@ if already defined, otherwise Nothing 
+binOpLazy :: BinOp -> Value -> Maybe Value
+binOpLazy And     (BoolValue False) = Just $ BoolValue False
+binOpLazy Or      (BoolValue True)  = Just $ BoolValue True
+binOpLazy Implies (BoolValue False) = Just $ BoolValue True
+binOpLazy Explies (BoolValue True)  = Just $ BoolValue True
+binOpLazy _ _                       = Nothing
+
+-- | Strict semantics of binary operators
+binOp :: SourcePos -> BinOp -> Value -> Value -> Execution Value 
+binOp pos Plus    (IntValue n1) (IntValue n2)   = return $ IntValue (n1 + n2)
+binOp pos Minus   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 - n2)
+binOp pos Times   (IntValue n1) (IntValue n2)   = return $ IntValue (n1 * n2)
+binOp pos Div     (IntValue n1) (IntValue n2)   = if n2 == 0 
+                                                then throwRuntimeFailure DivisionByZero pos
+                                                else return $ IntValue (fst (n1 `euclidean` n2))
+binOp pos Mod     (IntValue n1) (IntValue n2)   = if n2 == 0 
+                                                then throwRuntimeFailure DivisionByZero pos
+                                                else return $ IntValue (snd (n1 `euclidean` n2))
+binOp pos Leq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 <= n2)
+binOp pos Ls      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 < n2)
+binOp pos Geq     (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 >= n2)
+binOp pos Gt      (IntValue n1) (IntValue n2)   = return $ BoolValue (n1 > n2)
+binOp pos And     (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 && b2)
+binOp pos Or      (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 || b2)
+binOp pos Implies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 <= b2)
+binOp pos Explies (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 >= b2)
+binOp pos Equiv   (BoolValue b1) (BoolValue b2) = return $ BoolValue (b1 == b2)
+binOp pos Eq      v1 v2                         = return $ BoolValue (v1 == v2)
+binOp pos Neq     v1 v2                         = return $ BoolValue (v1 /= v2)
+binOp pos Lc      v1 v2                         = throwRuntimeFailure (UnsupportedConstruct "orders") pos
+
+-- | Euclidean division used by Boogie for integer division and modulo
+euclidean :: Integer -> Integer -> (Integer, Integer)
+a `euclidean` b =
+  case a `quotRem` b of
+    (q, r) | r >= 0    -> (q, r)
+           | b >  0    -> (q - 1, r + b)
+           | otherwise -> (q + 1, r - b)
+
+-- | Evaluate an expression;
+-- can have a side-effect of initializing variables that were not previously defined
+eval :: Expression -> Execution Value
+eval expr = case node expr of
+  TT -> return $ BoolValue True
+  FF -> return $ BoolValue False
+  Numeral n -> return $ IntValue n
+  Var id -> evalVar id (position expr)
+  Application id args -> evalApplication id args (position expr) Nothing
+  MapSelection m args -> evalMapSelection m args (position expr)
+  MapUpdate m args new -> evalMapUpdate m args new
+  Old e -> old $ eval e
+  IfExpr cond e1 e2 -> evalIf cond e1 e2
+  Coercion e t -> evalCoercion e t
+  UnaryExpression op e -> unOp op <$> eval e
+  BinaryExpression op e1 e2 -> evalBinary op e1 e2
+  Quantified Lambda _ _ _ -> throwRuntimeFailure (UnsupportedConstruct "lambda expressions") (position expr)
+  Quantified Forall tv vars e -> vnot <$> evalExists tv vars (enot e) (position expr)
+    where vnot (BoolValue b) = BoolValue (not b)
+  Quantified Exists tv vars e -> evalExists tv vars e (position expr)
+  
+evalVar id pos = do
+  tc <- gets envTypeContext
+  case M.lookup id (localScope tc) of
+    Just t -> lookup envLocals setLocal t
+    Nothing -> case M.lookup id (ctxGlobals tc) of
+      Just t -> lookup envGlobals setGlobal t
+      Nothing -> case M.lookup id (ctxConstants tc) of
+        Just t -> do
+          constants <- gets envConstants
+          case M.lookup id constants of
+            Just e -> eval e
+            Nothing -> return $ defaultValue t -- ToDo: cache constant value?
+        Nothing -> (error . show) (text "encountered unknown identifier during execution:" <+> text id) 
+  where
+    lookup getter setter t = do
+      vars <- gets getter
+      case M.lookup id vars of
+        Just val -> return val
+        Nothing -> generateValue t (modify . setter id) (checkWhere id pos)
+  
+evalApplication name args pos mRetType = do
+  defs <- gets (lookupFunction name)  
+  evalDefs defs
+  where
+    -- | If the guard of one of function definitions evaluates to true, apply that definition; otherwise return the default value
+    evalDefs :: [FDef] -> Execution Value
+    evalDefs [] = defaultValue . returnType <$> gets envTypeContext
+    evalDefs (FDef formals guard body : defs) = do
+      argsV <- mapM eval args
+      applicable <- evalLocally formals argsV guard `catchError` addStackFrame frame
+      case applicable of
+        BoolValue True -> evalLocally formals argsV body `catchError` addStackFrame frame 
+        BoolValue False -> evalDefs defs
+    evalLocally formals actuals expr = do
+      sig <- funSig name <$> gets envTypeContext
+      executeLocally (enterFunction sig formals args mRetType) formals actuals (eval expr)
+    returnType tc = case mRetType of
+      Nothing -> exprType tc (gen $ Application name args)
+      Just t -> t
+    frame = StackFrame pos name
+    
+evalMapSelection m args pos = do 
+  tc <- gets envTypeContext
+  let rangeType = exprType tc (gen $ MapSelection m args)
+  mV <- eval m
+  argsV <- mapM eval args
+  case mV of 
+    MapValue map -> case M.lookup argsV map of
+      Nothing -> 
+        case mapVariable tc (node m) of
+        Nothing -> return $ defaultValue rangeType -- The underlying map comes from a constant or function, nothing to check
+        Just v -> generateValue rangeType (\_ -> return ()) (checkWhere v pos) -- The underlying map comes from a variable: check the where clause
+        -- Decided not to cache map access so far, because it leads to strange effects when the map is passed as an argument and can take a lot of memory 
+        -- Just v -> generateValue rangeType (cache v map argsV) (checkWhere v pos) -- The underlying map comes from a variable: check the where clause and cache the value
+      Just v -> return v
+  where
+    mapVariable tc (Var v) = if M.member v (allVars tc)
+      then Just v
+      else Nothing
+    mapVariable tc (MapUpdate m _ _) = mapVariable tc (node m)
+    mapVariable tc _ = Nothing 
+    -- cache m map args val = setV m (MapValue (M.insert args val map))
+    
+evalMapUpdate m args new = do
+  mV <- eval m
+  argsV <- mapM eval args
+  newV <- eval new
+  case mV of 
+    MapValue map -> return $ MapValue (M.insert argsV newV map)
+  
+evalIf cond e1 e2 = do
+  v <- eval cond
+  case v of
+    BoolValue True -> eval e1    
+    BoolValue False -> eval e2    
+    
+evalCoercion (Pos pos (Application f args)) t = do
+  c <- gets envTypeContext
+  let t' = resolve c t
+  evalApplication f args pos (Just t') 
+evalCoercion e _ = eval e
+  
+evalBinary op e1 e2 = do
+  left <- eval e1
+  case binOpLazy op left of
+    Just result -> return result
+    Nothing -> do
+      right <- eval e2
+      binOp (position e1) op left right
+
+-- | Finite domain      
+type Domain = [Value]      
+
+evalExists :: [Id] -> [IdType] -> Expression -> SourcePos -> Execution Value      
+evalExists tv vars e pos = do
+  tc <- gets envTypeContext
+  case node $ normalize tc (attachPos pos $ Quantified Exists tv vars e) of
+    Quantified Exists tv' vars' e' -> evalExists' tv' vars' e'
+
+evalExists' :: [Id] -> [IdType] -> Expression -> Execution Value    
+evalExists' tv vars e = do
+  results <- executeLocally (enterQuantified tv vars) [] [] evalWithDomains
+  return $ BoolValue (any isTrue results)
+  where
+    evalWithDomains = do
+      doms <- domains e varNames
+      evalForEach varNames doms
+    -- | evalForEach vars domains: evaluate e for each combination of possible values of vars, drown from respective domains
+    evalForEach :: [Id] -> [Domain] -> Execution [Value]
+    evalForEach [] [] = replicate 1 <$> eval e
+    evalForEach (var : vars) (dom : doms) = concat <$> forM dom (fixOne vars doms var)
+    -- | Fix the value of var to val, then evaluate e for each combination of values for the rest of vars
+    fixOne :: [Id] -> [Domain] -> Id -> Value -> Execution [Value]
+    fixOne vars doms var val = do
+      setV var val
+      evalForEach vars doms
+    isTrue (BoolValue b) = b
+    varNames = map fst vars
+      
+{- Statements -}
+
+-- | Execute a basic statement
+-- (no jump, if or while statements allowed)
+exec :: Statement -> Execution ()
+exec stmt = case node stmt of
+  Predicate specClause -> execPredicate specClause (position stmt)
+  Havoc ids -> execHavoc ids (position stmt)
+  Assign lhss rhss -> execAssign lhss rhss
+  Call lhss name args -> execCall lhss name args (position stmt)
+  CallForall name args -> return () -- ToDo: assume (forall args :: pre ==> post)?
+  
+execPredicate specClause pos = do
+  b <- eval $ specExpr specClause
+  case b of 
+    BoolValue True -> return ()
+    BoolValue False -> throwRuntimeFailure (SpecViolation specClause) pos
+    
+execHavoc ids pos = do
+  tc <- gets envTypeContext
+  mapM_ (havoc tc) ids 
+  where
+    havoc tc id = generateValue (exprType tc . gen . Var $ id) (setV id) (checkWhere id pos) 
+    
+execAssign lhss rhss = do
+  rVals <- mapM eval rhss'
+  setAll lhss' rVals
+  where
+    lhss' = map fst (zipWith simplifyLeft lhss rhss)
+    rhss' = map snd (zipWith simplifyLeft lhss rhss)
+    simplifyLeft (id, []) rhs = (id, rhs)
+    simplifyLeft (id, argss) rhs = (id, mapUpdate (gen $ Var id) argss rhs)
+    mapUpdate e [args] rhs = gen $ MapUpdate e args rhs
+    mapUpdate e (args1 : argss) rhs = gen $ MapUpdate e args1 (mapUpdate (gen $ MapSelection e args1) argss rhs)
+    
+execCall lhss name args pos = do
+  tc <- gets envTypeContext
+  defs <- gets (lookupProcedure name)
+  case defs of
+    [] -> throwRuntimeFailure (NoImplementation name) pos
+    def : _ -> do
+      let lhssExpr = map (attachPos (ctxPos tc) . Var) lhss
+      retsV <- execProcedure (procSig name tc) def args lhssExpr `catchError` addStackFrame frame
+      setAll lhss retsV
+  where
+    frame = StackFrame pos name
+    
+-- | Execute program consisting of blocks starting from the block labeled label.
+-- Return the location of the exit point.
+execBlock :: Map Id [Statement] -> Id -> Execution SourcePos
+execBlock blocks label = let
+  block = blocks ! label
+  statements = init block
+  in do
+    mapM exec statements
+    case last block of
+      Pos pos Return -> return pos
+      Pos _ (Goto lbs) -> tryOneOf blocks lbs
+  
+-- | tryOneOf blocks labels: try executing blocks starting with each of labels,
+-- until we find one that does not result in an assumption violation      
+tryOneOf :: Map Id [Statement] -> [Id] -> Execution SourcePos        
+tryOneOf blocks (l : lbs) = execBlock blocks l `catchError` retry
+  where
+    retry err 
+      | failureKind err == Unreachable && not (null lbs) = tryOneOf blocks lbs
+      | otherwise = throwError err
+  
+-- | 'execProcedure' @sig def args lhss@ :
+-- Execute definition @def@ of procedure @sig@ with actual arguments @args@ and call left-hand sides @lhss@
+execProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Execution [Value]
+execProcedure sig def args lhss = let 
+  ins = pdefIns def
+  outs = pdefOuts def
+  blocks = snd (pdefBody def)
+  exitPoint pos = if pos == noPos 
+    then pdefPos def  -- Fall off the procedure body: take the procedure definition location
+    else pos          -- A return statement inside the body
+  execBody = do
+    checkPreconditions sig def
+    olds <- saveOld
+    pos <- exitPoint <$> execBlock blocks startLabel
+    checkPostonditions sig def pos
+    restoreOld olds
+    mapM (eval . attachPos (pdefPos def) . Var) outs
+  in do
+    argsV <- mapM eval args
+    executeLocally (enterProcedure sig def args lhss) ins argsV execBody
+    
+{- Specs -}
+
+-- | Assert preconditions of definition def of procedure sig
+checkPreconditions sig def = mapM_ (exec . attachPos (pdefPos def) . Predicate . subst sig) (psigRequires sig)
+  where 
+    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
+
+-- | Assert postconditions of definition def of procedure sig at exitPoint    
+checkPostonditions sig def exitPoint = mapM_ (exec . attachPos exitPoint . Predicate . subst sig) (psigEnsures sig)
+  where 
+    subst sig (SpecClause t f e) = SpecClause t f (paramSubst sig def e)
+
+-- | Assume where clause of variable at a program location pos
+-- (pos will be reported as the location of the failure instead of the location of the variable definition).
+checkWhere id pos = do
+  whereClauses <- ctxWhere <$> gets envTypeContext
+  case M.lookup id whereClauses of
+    Nothing -> return ()
+    Just w -> (exec . attachPos pos . Predicate . SpecClause Where True) w
+
+{- Preprocessing -}
+
+-- | Collect constant, function and procedure definitions from the program
+collectDefinitions :: Program -> SafeExecution ()
+collectDefinitions (Program decls) = mapM_ processDecl decls
+  where
+    processDecl (Pos _ (FunctionDecl name _ args _ (Just body))) = processFunctionBody name args body
+    processDecl (Pos pos (ProcedureDecl name _ args rets _ (Just body))) = processProcedureBody name pos (map noWhere args) (map noWhere rets) body
+    processDecl (Pos pos (ImplementationDecl name _ args rets bodies)) = mapM_ (processProcedureBody name pos args rets) bodies
+    processDecl (Pos _ (AxiomDecl expr)) = processAxiom expr
+    processDecl _ = return ()
+  
+processFunctionBody name args body = let
+  formals = map (formalName . fst) args
+  guard = gen TT
+  in
+    modify $ addFunctionDefs name [FDef formals guard body]
+  where
+    formalName Nothing = dummyFArg 
+    formalName (Just n) = n    
+
+processProcedureBody name pos args rets body = do
+  sig <- procSig name <$> gets envTypeContext
+  modify $ addProcedureDef name (PDef argNames retNames (paramsRenamed sig) (flatten body) pos) 
+  where
+    argNames = map fst args
+    retNames = map fst rets
+    flatten (locals, statements) = (concat locals, M.fromList (toBasicBlocks statements))
+    paramsRenamed sig = map itwId (psigParams sig) /= (argNames ++ retNames)     
+
+processAxiom expr = do
+  extractConstantDefs expr
+  extractFunctionDefs expr []
+  
+{- Constant and function definitions -}
+
+-- | Extract constant definitions from a boolean expression bExpr
+extractConstantDefs :: Expression -> SafeExecution ()
+extractConstantDefs bExpr = case node bExpr of  
+  BinaryExpression Eq (Pos _ (Var c)) rhs -> modify $ addConstantDef c rhs -- c == rhs: remember rhs as a definition for c
+  _ -> return ()
+
+-- | Extract function definitions from a boolean expression bExpr, using guards extracted from the exclosing expression.
+-- bExpr of the form "(forall x :: P(x, c) ==> f(x, c) == rhs(x, c) && B) && A",
+-- with zero or more bound variables x and zero or more constants c,
+-- produces a definition "f(x, x') = rhs(x, x')" with a guard "P(x) && x' == c"
+extractFunctionDefs :: Expression -> [Expression] -> SafeExecution ()
+extractFunctionDefs bExpr guards = extractFunctionDefs' (node bExpr) guards
+
+extractFunctionDefs' (BinaryExpression Eq (Pos _ (Application f args)) rhs) outerGuards = do
+  c <- gets envTypeContext
+  -- Only possible if each argument is either a variables or does not involve variables and there are no extra variables in rhs:
+  if all (simple c) args && closedRhs c
+    then do    
+      let (formals, guards) = unzip (extractArgs c)
+      let allGuards = concat guards ++ outerGuards
+      let guard = if null allGuards then gen TT else foldl1 (|&|) allGuards
+      modify $ addFunctionDefs f [FDef formals guard rhs]
+    else return ()
+  where
+    simple _ (Pos p (Var _)) = True
+    simple c e = null $ freeVars e `intersect` M.keys (ctxIns c)
+    closedRhs c = null $ (freeVars rhs \\ concatMap freeVars args) `intersect` M.keys (ctxIns c)
+    extractArgs c = zipWith (extractArg c) args [0..]
+    -- | Formal argument name and guards extracted from an actual argument at position i
+    extractArg :: Context -> Expression -> Integer -> (String, [Expression])
+    extractArg c (Pos p e) i = let 
+      x = freshArgName i 
+      xExpr = attachPos p $ Var x
+      in 
+        case e of
+          Var arg -> if arg `M.member` ctxIns c 
+            then (arg, []) -- Bound variable of the enclosing quantifier: use variable name as formal, no additional guards
+            else (x, [xExpr |=| Pos p e]) -- Constant: use fresh variable as formal (will only appear in the guard), add equality guard
+          _ -> (x, [xExpr |=| Pos p e])
+    freshArgName i = f ++ (nonIdChar : show i)
+extractFunctionDefs' (BinaryExpression Implies cond bExpr) outerGuards = extractFunctionDefs bExpr (cond : outerGuards)
+extractFunctionDefs' (BinaryExpression And bExpr1 bExpr2) outerGuards = do
+  extractFunctionDefs bExpr1 outerGuards
+  extractFunctionDefs bExpr2 outerGuards
+extractFunctionDefs' (Quantified Forall tv vars bExpr) outerGuards = executeLocally (enterQuantified tv vars) [] [] (extractFunctionDefs bExpr outerGuards)
+extractFunctionDefs' _ _ = return ()
+   
+{- Quantification -}
+
+-- | Sets of interval constraints on integer variables
+type Constraints = Map Id Interval
+            
+-- | The set of domains for each variable in vars, outside which boolean expression boolExpr is always false.
+-- Fails if any of the domains are infinite or cannot be found.
+domains :: Expression -> [Id] -> Execution [Domain]
+domains boolExpr vars = do
+  initC <- foldM initConstraints M.empty vars
+  finalC <- inferConstraints boolExpr initC 
+  forM vars (domain finalC)
+  where
+    initConstraints c var = do
+      tc <- gets envTypeContext
+      case M.lookup var (allVars tc) of
+        Just BoolType -> return c
+        Just IntType -> return $ M.insert var top c
+        _ -> throwRuntimeFailure (UnsupportedConstruct "quantification over a map or user-defined type") (position boolExpr)
+    domain c var = do
+      tc <- gets envTypeContext
+      case M.lookup var (allVars tc) of
+        Just BoolType -> return $ map BoolValue [True, False]
+        Just IntType -> do
+          case c ! var of
+            int | isBottom int -> return []
+            Interval (Finite l) (Finite u) -> return $ map IntValue [l..u]
+            int -> throwRuntimeFailure (InfiniteDomain var int) (position boolExpr)
+
+-- | Starting from initial constraints, refine them with the information from boolExpr,
+-- until fixpoint is reached or the domain for one of the variables is empty.
+-- This function terminates because the interval for each variable can only become smaller with each iteration.
+inferConstraints :: Expression -> Constraints -> Execution Constraints
+inferConstraints boolExpr constraints = do
+  constraints' <- foldM refineVar constraints (M.keys constraints)
+  if bot `elem` M.elems constraints'
+    then return $ M.map (const bot) constraints'  -- if boolExpr does not have a satisfying assignment to one variable, then it has none to all variables
+    else if constraints == constraints'
+      then return constraints'                    -- if a fixpoint is reached, return it
+      else inferConstraints boolExpr constraints' -- otherwise do another iteration
+  where
+    refineVar :: Constraints -> Id -> Execution Constraints
+    refineVar c id = do
+      int <- inferInterval boolExpr c id
+      return $ M.insert id (meet (c ! id) int) c 
+
+-- | Infer an interval for variable x, outside which boolean expression booExpr is always false, 
+-- assuming all other quantified variables satisfy constraints;
+-- boolExpr has to be in negation-prenex normal form.
+inferInterval :: Expression -> Constraints -> Id -> Execution Interval
+inferInterval boolExpr constraints x = (case node boolExpr of
+  FF -> return bot
+  BinaryExpression And be1 be2 -> liftM2 meet (inferInterval be1 constraints x) (inferInterval be2 constraints x)
+  BinaryExpression Or be1 be2 -> liftM2 join (inferInterval be1 constraints x) (inferInterval be2 constraints x)
+  BinaryExpression Eq ae1 ae2 -> do
+    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
+    if 0 <: a && 0 <: b
+      then return top
+      else return $ -b // a
+  BinaryExpression Leq ae1 ae2 -> do
+    (a, b) <- toLinearForm (ae1 |-| ae2) constraints x
+    if isBottom a || isBottom b
+      then return bot
+      else if 0 <: a && not (isBottom (meet b nonPositives))
+        then return top
+        else return $ join (lessEqual (-b // meet a positives)) (greaterEqual (-b // meet a negatives))
+  BinaryExpression Ls ae1 ae2 -> inferInterval (ae1 |<=| (ae2 |-| num 1)) constraints x
+  BinaryExpression Geq ae1 ae2 -> inferInterval (ae2 |<=| ae1) constraints x
+  BinaryExpression Gt ae1 ae2 -> inferInterval (ae2 |<=| (ae1 |-| num 1)) constraints x
+  -- Quantifier can only occur here if it is alternating with the enclosing one, hence no domain can be inferred 
+  _ -> return top
+  ) `catchError` handleNotLinear
+  where      
+    lessEqual int | isBottom int = bot
+                  | otherwise = Interval NegInf (upper int)
+    greaterEqual int  | isBottom int = bot
+                      | otherwise = Interval (lower int) Inf
+    handleNotLinear err = case rtfSource err of
+      InternalFailure NotLinear -> return top
+      _ -> throwError err                      
+
+-- | Linear form (A, B) represents a set of expressions a*x + b, where a in A and b in B
+type LinearForm = (Interval, Interval)
+
+-- | If possible, convert arithmetic expression aExpr into a linear form over variable x,
+-- assuming all other quantified variables satisfy constraints.
+toLinearForm :: Expression -> Constraints -> Id -> Execution LinearForm
+toLinearForm aExpr constraints x = case node aExpr of
+  Numeral n -> return (0, fromInteger n)
+  Var y -> if x == y
+    then return (1, 0)
+    else case M.lookup y constraints of
+      Just int -> return (0, int)
+      Nothing -> const aExpr
+  Application name args -> if null $ M.keys constraints `intersect` freeVars aExpr
+    then const aExpr
+    else throwInternalFailure NotLinear
+  MapSelection m args -> if null $ M.keys constraints `intersect` freeVars aExpr
+    then const aExpr
+    else throwInternalFailure NotLinear
+  Old e -> old $ toLinearForm e constraints x
+  UnaryExpression Neg e -> do
+    (a, b) <- toLinearForm e constraints x
+    return (-a, -b)
+  BinaryExpression op e1 e2 -> do
+    left <- toLinearForm e1 constraints x
+    right <- toLinearForm e2 constraints x 
+    combineBinOp op left right
+  where
+    const e = do
+      v <- eval e
+      case v of
+        IntValue n -> return (0, fromInteger n)
+    combineBinOp Plus   (a1, b1) (a2, b2) = return (a1 + a2, b1 + b2)
+    combineBinOp Minus  (a1, b1) (a2, b2) = return (a1 - a2, b1 - b2)
+    combineBinOp Times  (a, b)   (0, k)   = return (k * a, k * b)
+    combineBinOp Times  (0, k)   (a, b)   = return (k * a, k * b)
+    combineBinOp _ _ _ = throwInternalFailure NotLinear                      
+  

@@ -0,0 +1,138 @@+{-# LANGUAGE PatternGuards #-}
+
+-- | Lattice of integer intervals
+module Language.Boogie.Intervals where
+
+import Data.Ratio
+import Data.Maybe
+
+-- | Lattice type class 
+class Eq a => Lattice a where
+  top   :: a              -- ^ Top
+  bot   :: a              -- ^ Bottom
+  (<:)  :: a -> a -> Bool -- ^ Partial order
+  join  :: a -> a -> a    -- ^ Least upper bound
+  meet  :: a -> a -> a    -- ^ Greatest lower bound
+  
+  x <: y = meet x y == x
+
+-- | Integers extended with infinity
+data Extended = NegInf | Finite Integer | Inf
+  deriving Eq
+  
+instance Show Extended where
+  show NegInf = "-Infinity"
+  show (Finite i) = show i
+  show Inf = "Infinity"
+  
+instance Num Extended where
+  Inf + NegInf = error ("Cannot add " ++ show Inf ++ " and " ++ show NegInf)
+  NegInf + Inf = error ("Cannot add " ++ show NegInf ++ " and " ++ show Inf)
+  Inf + _ = Inf
+  NegInf + _ = NegInf
+  Finite _ + Inf = Inf
+  Finite _ + NegInf = NegInf
+  Finite i + Finite j = Finite (i + j)
+  
+  Finite 0 * _ = Finite 0
+  _ * Finite 0 = Finite 0
+  e1 * e2 | signum (e1) == -1 && signum (e2) == -1 = negate e1 * negate e2
+  e1 * e2 | signum (e1) == -1 = negate $ negate e1 * e2
+  e1 * e2 | signum (e2) == -1 = negate $ e1 * negate e2
+  Inf * _ = Inf
+  _ * Inf = Inf
+  Finite i * Finite j = Finite (i * j)
+  
+  negate Inf = NegInf
+  negate NegInf = Inf
+  negate (Finite i) = Finite (-i)
+  
+  abs Inf = Inf
+  abs NegInf = Inf
+  abs (Finite i) = Finite (abs i)
+  
+  signum Inf = 1
+  signum NegInf = -1
+  signum (Finite i) = Finite (signum i)
+  
+  fromInteger i = Finite i
+
+-- | 'extDiv' @r a b@ : result of dividing @a@ by @b@, rounded with @r@ in the finite case;
+-- dividing infinty by infinity yields 'Nothing'.
+extDiv :: (Ratio Integer -> Integer) -> Extended -> Extended -> Maybe Extended  
+extDiv r (Finite i) (Finite j) = Just $ Finite (r (i % j))
+extDiv _ Inf (Finite j) = Just $ signum (Finite j) * Inf
+extDiv _ NegInf (Finite j) = Just $ signum (Finite j) * NegInf
+extDiv _ (Finite i) Inf = Just $ 0
+extDiv _ (Finite i) NegInf = Just $ 0
+extDiv _ _ _ = Nothing  
+
+instance Ord Extended where
+  NegInf <= b = True
+  b <= NegInf = False
+  b <= Inf = True
+  Inf <= b = False
+  Finite x <= Finite y = x <= y
+ 
+-- | Integer intervals
+data Interval = Interval {
+  lower :: Extended,
+  upper :: Extended
+}
+
+-- | Is interval empty?
+isBottom (Interval l u) = l > u
+
+-- | Are both bounds of the interval finite?
+isBounded (Interval (Finite l) (Finite u)) = True
+isBounded _ = False
+
+-- | All positive integers
+positives = Interval 1 Inf
+-- | All negative integers
+negatives = Interval NegInf (-1)
+-- | All positive integers and 0
+nonNegatives = Interval 0 Inf
+-- | All netaive integers and 0
+nonPositives = Interval NegInf 0
+
+-- | Apply function to all pairs of bounds coming from two different intervals
+mapBounds f (Interval l1 u1) (Interval l2 u2) = [f b1 b2 | b1 <- [l1, u1], b2 <- [l2, u2]]
+
+instance Show Interval where
+  show int | isBottom int = "[]"
+  show (Interval l u)     = "[" ++ show l ++ ".." ++ show u ++ "]"
+
+instance Eq Interval where
+  int1 == int2 | isBottom int1, isBottom int2 = True
+  Interval l1 u1 == Interval l2 u2            = l1 == l2 && u1 == u2
+  
+instance Lattice Interval where  
+  top = Interval NegInf Inf
+  bot = Interval Inf NegInf
+  
+  join int1 int2 | isBottom int1 = int2
+  join int1 int2 | isBottom int2 = int1
+  join (Interval l1 u1) (Interval l2 u2) = Interval (min l1 l2) (max u1 u2)
+
+  meet int1 int2 | isBottom int1 = int1
+  meet int1 int2 | isBottom int2 = int2
+  meet (Interval l1 u1) (Interval l2 u2) = Interval (max l1 l2) (min u1 u2)
+  
+instance Num Interval where
+  int1 + int2 | isBottom int1 || isBottom int2 = bot
+  Interval l1 u1 + Interval l2 u2 = Interval (l1 + l2) (u1 + u2)
+  
+  int1 * int2 | isBottom int1 || isBottom int2 = bot
+              | otherwise = Interval (minimum (mapBounds (*) int1 int2)) (maximum (mapBounds (*) int1 int2))
+  
+  negate (Interval l u) = Interval (-u) (-l)  
+  abs int = int
+  signum _ = 1
+  fromInteger n = Interval (Finite n) (Finite n)
+
+-- | Division on integer intervals
+(//) int1 int2 | isBottom int1 || isBottom int2 = bot
+               | 0 <: int2 = join (int1 // meet int2 negatives) (int1 // meet int2 positives)
+               | otherwise = Interval (minimum (catMaybes (mapBounds (extDiv ceiling) int1 int2))) (maximum (catMaybes (mapBounds (extDiv floor) int1 int2)))
+  

@@ -0,0 +1,80 @@+-- | Various normal forms of Boolean expressions
+module Language.Boogie.NormalForm where
+
+import Language.Boogie.AST
+import Language.Boogie.Position
+import Language.Boogie.Util
+import Language.Boogie.TypeChecker
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+
+-- | Negation normal form of a Boolean expression:
+-- no negation above boolean connectives, quantifiers or relational operators;
+-- no boolean connectives except @&&@ and @||@
+negationNF :: Context -> Expression -> Expression
+negationNF c boolExpr = case node boolExpr of
+  UnaryExpression Not e -> case node e of
+    UnaryExpression Not e' -> negationNF c e'
+    BinaryExpression And e1 e2 -> negationNF c (enot e1) ||| negationNF c (enot e2)
+    BinaryExpression Or e1 e2 -> negationNF c (enot e1) |&| negationNF c (enot e2)
+    BinaryExpression Implies e1 e2 -> negationNF c e1 |&| negationNF c (enot e2)
+    BinaryExpression Equiv e1 e2 -> (negationNF c e1 |&| negationNF c (enot e2)) |&| (negationNF c (enot e1) |&| negationNF c e2)
+    BinaryExpression Eq e1 e2 -> case exprType c e1 of
+      BoolType -> negationNF c (enot (e1 |<=>| e2))
+      _ -> e1 |!=| e2
+    BinaryExpression Neq e1 e2 -> case exprType c e1 of
+      BoolType -> negationNF c (e1 |<=>| e2)
+      _ -> e1 |=| e2
+    BinaryExpression Leq ae1 ae2 -> ae1 |>| ae2
+    BinaryExpression Ls ae1 ae2 -> ae1 |>=| ae2
+    BinaryExpression Geq ae1 ae2 -> ae1 |<| ae2
+    BinaryExpression Gt ae1 ae2 -> ae1 |<=| ae2
+    Quantified Forall tv vars e' -> attachPos (position e) $ Quantified Exists tv vars (negationNF (enterQuantified tv vars c) (enot e'))
+    Quantified Exists tv vars e' -> attachPos (position e) $ Quantified Forall tv vars (negationNF (enterQuantified tv vars c) (enot e'))
+    _ -> boolExpr
+  BinaryExpression Implies e1 e2 -> negationNF c (enot e1) ||| negationNF c e2
+  BinaryExpression Equiv e1 e2 -> (negationNF c (enot e1) ||| negationNF c e2) |&| (negationNF c e1 ||| negationNF c (enot e2))
+  BinaryExpression Eq e1 e2 -> case exprType c e1 of
+    BoolType -> negationNF c (e1 |<=>| e2)
+    _ -> boolExpr
+  BinaryExpression Neq e1 e2 -> case exprType c e1 of
+    BoolType -> negationNF c (enot (e1 |<=>| e2))
+    _ -> boolExpr
+  BinaryExpression op e1 e2 | op == And || op == Or -> inheritPos2 (BinaryExpression op) (negationNF c e1) (negationNF c e2)    
+  Quantified qop tv vars e -> attachPos (position boolExpr) $ Quantified qop tv vars (negationNF (enterQuantified tv vars c) e)
+  _ -> boolExpr
+
+-- | Prenex normal form of a Boolean expression:
+-- all quantifiers are pushed to the outside and any two quantifiers of the same kind in a row are glued together.
+-- Requires expression to be in the negation normal form.  
+prenexNF :: Expression -> Expression
+prenexNF boolExpr = (glue . rawPrenex) boolExpr
+  where
+    -- | Push all quantifiers to the front
+    rawPrenex boolExpr = case node boolExpr of
+      -- We only have to consider && and || because boolExpr is in negation normal form
+      BinaryExpression op e1 e2 | op == And || op == Or -> merge (++ "1") (++ "2") op (rawPrenex e1) (rawPrenex e2)
+      _ -> boolExpr
+    merge r1 r2 op e1 e2 = attachPos (position e1) (merge' r1 r2 op e1 e2)
+    merge' r1 r2 op (Pos _ (Quantified qop tv vars e)) e2 = case renameBound r1 (Quantified qop tv vars e) of
+      Quantified qop tv' vars' e' -> Quantified qop tv' vars' (merge r1 r2 op e' e2)
+    merge' r1 r2 op e1 (Pos _ (Quantified qop tv vars e)) = case renameBound r2 (Quantified qop tv vars e) of
+      Quantified qop tv' vars' e' -> Quantified qop tv' vars' (merge r1 r2 op e1 e')
+    merge' _ _ op e1 e2 = BinaryExpression op e1 e2
+    -- | Rename all bound variables and type variables in a quantified expression with a renaming function r
+    renameBound r (Quantified qop tv vars e) = Quantified qop (map r tv) (map (renameVar r tv) vars) (exprSubst (varBinding r (map fst vars)) e)
+    varBinding r ids = M.fromList $ zip ids (map (Var . r) ids)
+    typeBinding r tv = M.fromList $ zip tv (map (nullaryType . r) tv)
+    renameVar r tv (id, t) = (r id, typeSubst (typeBinding r tv) t)
+    -- | Glue together any two quantifiers of the same kind in a row
+    glue boolExpr = attachPos (position boolExpr) (glue' (node boolExpr))
+    glue' boolExpr = case boolExpr of
+      Quantified qop tv vars e -> case node e of
+        Quantified qop' tv' vars' e' | qop == qop' -> glue' (Quantified qop (tv ++ tv') (vars ++ vars') e')
+                                     | otherwise -> Quantified qop tv vars (glue e)
+        _ -> boolExpr
+      _ -> boolExpr
+
+-- | Negation and prenex normal form of a Boolean expression
+normalize :: Context -> Expression -> Expression      
+normalize c boolExpr = prenexNF $ negationNF c boolExpr

@@ -0,0 +1,510 @@+-- | Parsec-based parser for Boogie 2
+module Language.Boogie.Parser (
+  program,
+  type_,
+  expression,
+  statement,
+  decl
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position
+import Language.Boogie.Tokens
+import Language.Boogie.PrettyPrinter hiding (option, optionMaybe, commaSep, angles)
+import Data.List
+import Text.ParserCombinators.Parsec hiding (token, label)
+import qualified Text.ParserCombinators.Parsec.Token as P
+import Text.ParserCombinators.Parsec.Expr
+import Control.Monad
+import Control.Applicative ((<$>), (<*>), (<*), (*>))
+
+{- Interface -}
+
+-- | Program parser
+program :: Parser Program
+program = do 
+  whiteSpace
+  p <- many decl
+  eof
+  return $ Program p
+
+{- Lexical analysis -}
+
+opNames :: [String]
+opNames = map snd unOpTokens ++ (map snd binOpTokens \\ keywords) ++ otherOps
+
+opStart :: [Char]
+opStart = nub (map head opNames)
+
+opLetter :: [Char]
+opLetter = nub (concatMap tail opNames)
+
+boogieDef :: P.LanguageDef st
+boogieDef = P.LanguageDef 
+  commentStart
+  commentEnd
+  commentLine
+  False
+  (letter <|> oneOf identifierChars)
+  (alphaNum <|> oneOf identifierChars)
+  (oneOf opStart)
+  (oneOf opLetter)
+  keywords
+  opNames
+  True
+  
+lexer :: P.TokenParser ()
+lexer = P.makeTokenParser boogieDef    
+      
+identifier = P.identifier lexer
+reserved = P.reserved lexer
+reservedOp = P.reservedOp lexer
+charLiteral = P.charLiteral lexer
+stringLiteral = P.stringLiteral lexer
+natural = P.natural lexer
+integer = P.integer lexer
+symbol = P.symbol lexer
+whiteSpace = P.whiteSpace lexer
+angles = P.angles lexer
+brackets = P.brackets lexer
+parens = P.parens lexer
+braces = P.braces lexer
+semi = P.semi lexer
+comma = P.comma lexer
+commaSep = P.commaSep lexer
+commaSep1 = P.commaSep1 lexer
+
+{- Types -}
+
+typeAtom :: Parser Type
+typeAtom = choice [
+  reserved "int" >> return IntType,
+  reserved "bool" >> return BoolType,
+  -- bit vector
+  parens type_
+  ]
+       
+typeArgs :: Parser [Id]
+typeArgs = try (angles (commaSep1 identifier)) <|> return []
+       
+mapType :: Parser Type
+mapType = do
+  args <- typeArgs
+  domains <- brackets (commaSep1 type_)
+  range <- type_
+  return $ MapType args domains range
+  
+typeCtorArgs :: Parser [Type]
+typeCtorArgs = choice [
+  do 
+    x <- typeAtom
+    xs <- option [] typeCtorArgs
+    return $ x : xs,
+  do
+    x <- identifier
+    xs <- option [] typeCtorArgs
+    return $ Instance x [] : xs,
+  do
+    x <- mapType
+    return [x]
+  ]
+
+-- | Type parser  
+type_ :: Parser Type
+type_ = choice [
+  typeAtom, 
+  mapType,  
+  do
+    id <- identifier
+    args <- option [] typeCtorArgs
+    return $ Instance id args
+  ] <?> "type"
+
+{- Expressions -}
+
+qop :: Parser QOp
+qop = (reserved "forall" >> return Forall) <|> (reserved "exists" >> return Exists) <|> (reserved "lambda" >> return Lambda)
+  
+atom :: Parser BareExpression
+atom = choice [
+  reserved "false" >> return FF,
+  reserved "true" >> return TT,
+  Numeral <$> natural,
+  varOrCall,
+  old,
+  ifThenElse,
+  node <$> try (parens expression),
+  parens quantified
+  ]
+  where
+    varOrCall = do
+      id <- identifier
+      (parens (commaSep expression) >>= (return . Application id)) <|> (return $ Var id)
+    old = do
+      reserved "old"
+      e <- parens expression
+      return $ Old e
+    ifThenElse = do
+      reserved "if"
+      cond <- expression
+      reserved "then"
+      thenExpr <- expression
+      reserved "else"
+      elseExpr <- expression
+      return $ IfExpr cond thenExpr elseExpr
+    quantified = do
+      op <- qop
+      args <- typeArgs
+      vars <- case args of
+        [] -> commaSep1 idsType
+        _ -> commaSep idsType      
+      reservedOp "::" 
+      case op of
+        Lambda -> return []
+        _ -> many trigAttr      
+      e <- expression
+      return $ Quantified op args (ungroup vars) e
+
+arrayExpression :: Parser Expression
+arrayExpression = do
+  e <- attachPosBefore atom
+  mapOps <- many (brackets (mapOp))
+  return $ foldr (.) id (reverse mapOps) e
+  where
+    mapOp = do
+      args <- commaSep1 expression
+      option (inheritPos ((flip MapSelection) args)) (do 
+        reservedOp ":="
+        e <- expression
+        return $ inheritPos (flip ((flip MapUpdate) args) e))
+        
+coercionExpression :: Parser Expression
+coercionExpression = do
+  e <- arrayExpression
+  coercedTos <- many coercedTo
+  return $ foldr (.) id (reverse coercedTos) e
+  where
+    coercedTo = do
+      reservedOp ":"
+      t <- type_
+      return $ inheritPos ((flip Coercion) t)
+    
+-- | Expression parser    
+expression :: Parser Expression  
+expression = buildExpressionParser table coercionExpression <?> "expression"
+
+table = [[unOp Neg, unOp Not],
+     [binOp Times AssocLeft, binOp Div AssocLeft, binOp Mod AssocLeft],
+     [binOp Plus AssocLeft, binOp Minus AssocLeft],
+     --[binOp Concat AssocLeft],
+     [binOp Eq AssocNone, binOp Neq AssocNone, binOp Ls AssocNone, binOp Leq AssocNone, binOp Gt AssocNone, binOp Geq AssocNone, binOp Lc AssocNone],
+     [binOp And AssocLeft], -- ToDo: && and || on the same level but do not interassociate
+     [binOp Or AssocLeft],
+     [binOp Implies AssocRight, binOp Explies AssocLeft], -- Mixing is prevented by different associativities
+     [binOp Equiv AssocRight]]
+  where
+    binOp op assoc = Infix (reservedOp (opName op binOpTokens) >> return (\e1 e2 -> attachPos (position e1) (BinaryExpression op e1 e2))) assoc
+    unOp op = Prefix (do
+      pos <- getPosition
+      reservedOp (opName op unOpTokens)
+      return (\e -> attachPos pos (UnaryExpression op e)))
+    
+wildcardExpression :: Parser WildcardExpression
+wildcardExpression = (expression >>= return . Expr) <|> (reservedOp "*" >> return Wildcard)
+    
+{- Statements -}
+
+lhs :: Parser (Id, [[Expression]])
+lhs = do
+  id <- identifier
+  selects <- many (brackets (commaSep1 expression))
+  return (id, selects)
+
+assign :: Parser BareStatement
+assign = do
+  lefts <- commaSep1 lhs
+  reservedOp ":="
+  rights <- commaSep1 expression
+  semi
+  return $ Assign lefts rights
+  
+call :: Parser BareStatement  
+call = do
+  reserved "call"
+  lefts <- option [] (try lhss)
+  id <- identifier
+  args <- parens (commaSep expression)
+  semi
+  return $ Call lefts id args
+  where
+    lhss = do
+      ids <- commaSep1 identifier
+      reservedOp ":="
+      return ids
+  
+callForall :: Parser BareStatement  
+callForall = do
+  reserved "call"
+  reserved "forall"
+  id <- identifier
+  args <- parens (commaSep wildcardExpression)
+  semi
+  return $ CallForall id args
+  
+ifStatement :: Parser BareStatement
+ifStatement = do
+  reserved "if"
+  cond <- parens wildcardExpression
+  thenBlock <- block
+  elseBlock <- optionMaybe (reserved "else" >> (block <|> elseIf))
+  return $ If cond thenBlock elseBlock
+  where
+    elseIf = do
+      i <- attachPosBefore ifStatement
+      return $ singletonBlock i
+  
+whileStatement :: Parser BareStatement
+whileStatement = do
+  reserved "while"
+  cond <- parens wildcardExpression
+  invs <- many loopInvariant
+  body <- block
+  return $ While cond invs body
+  where
+    loopInvariant = do
+      free <- hasKeyword "free"
+      reserved "invariant"
+      e <- expression
+      semi
+      return (SpecClause LoopInvariant free e)    
+
+-- | Statement parser      
+statement :: Parser Statement
+statement = attachPosBefore (choice [
+  do { reserved "assert"; many attribute; e <- expression; semi; return $ Predicate (SpecClause Inline False e) },
+  do { reserved "assume"; many attribute; e <- expression; semi; return $ Predicate (SpecClause Inline True e) },
+  do { reserved "havoc"; ids <- commaSep1 identifier; semi; return $ Havoc ids },
+  assign,
+  try call,
+  callForall,
+  ifStatement,
+  whileStatement,
+  do { reserved "break"; id <- optionMaybe identifier; semi; return $ Break id },
+  do { reserved "return"; semi; return Return },
+  do { reserved "goto"; ids <- commaSep1 identifier; semi; return $ Goto ids }
+  ] <?> "statement")
+  
+label :: Parser Id
+label = do
+  id <- identifier
+  reservedOp ":"
+  return id 
+  <?> "label"
+  
+lStatement :: Parser LStatement
+lStatement = attachPosBefore $ do
+  lbs <- many (try label)
+  s <- statement
+  return (lbs, s)
+
+statementList :: Parser Block
+statementList = do
+  lstatements <- many (try lStatement)
+  pos1 <- getPosition
+  lempty <- many (try label)
+  pos2 <- getPosition
+  return $ if null lempty
+    then lstatements 
+    else lstatements ++ [attachPos pos1 (lempty, attachPos pos2 Skip)]
+
+block :: Parser Block
+block = braces statementList
+    
+{- Declarations -}
+
+newType :: Parser NewType
+newType = do
+  name <- identifier
+  args <- many identifier
+  value <- optionMaybe (reservedOp "=" >> type_ )
+  return $ NewType name args value
+
+typeDecl :: Parser BareDecl
+typeDecl = do
+  reserved "type"
+  many attribute
+  ts <- commaSep newType
+  semi
+  return $ TypeDecl ts
+
+parentEdge :: Parser ParentEdge
+parentEdge = do
+  unique <- hasKeyword "unique"
+  id <- identifier
+  return (unique, id)
+
+constantDecl :: Parser BareDecl
+constantDecl = do 
+  reserved "const"
+  many attribute
+  unique <- hasKeyword "unique"
+  ids <- idsType
+  orderSpec <- optionMaybe (reserved "extends" >> commaSep parentEdge)
+  complete <- hasKeyword "complete"
+  semi
+  return $ ConstantDecl unique (fst ids) (snd ids) orderSpec complete
+  
+functionDecl :: Parser BareDecl
+functionDecl = do
+  reserved "function"
+  many attribute
+  name <- identifier
+  tArgs <- typeArgs
+  args <- parens (option [] (try namedArgs <|> unnamedArgs))  
+  ret <- returns <|> returnType
+  body <- (semi >> return Nothing) <|> (Just <$> braces expression)
+  return $ FunctionDecl name tArgs args ret body
+  where
+    unnamedArgs = map (\t -> (Nothing, t))                  <$> commaSep1 type_
+    namedArgs =   map (\(id, t) -> (Just id, t)) . ungroup  <$> commaSep1 idsType
+    returns = do
+      reserved "returns"
+      parens fArg
+    fArg = do
+      name <- optionMaybe (try (identifier <* reservedOp ":"))
+      t <- type_
+      return (name, t)      
+    returnType = do
+      reservedOp ":"
+      t <- type_
+      return (Nothing, t)
+
+axiomDecl :: Parser BareDecl
+axiomDecl = do
+  reserved "axiom"
+  many attribute
+  e <- expression
+  semi
+  return $ AxiomDecl e
+
+varList :: Parser [IdTypeWhere]
+varList = do
+  reserved "var"
+  many attribute
+  vars <- commaSep1 idsTypeWhere
+  semi
+  return $ ungroupWhere vars
+  
+varDecl :: Parser BareDecl
+varDecl = VarDecl <$> varList
+    
+body :: Parser Body
+body = braces (do
+  locals <- many varList
+  statements <- statementList
+  return (locals, statements))
+  
+procDecl :: Parser BareDecl
+procDecl = do
+  reserved "procedure"
+  many attribute
+  name <- identifier
+  tArgs <- typeArgs
+  args <- parens (commaSep idsTypeWhere)
+  rets <- option [] (reserved "returns" >> parens (commaSep idsTypeWhere))
+  noBody name tArgs args rets <|> withBody name tArgs args rets
+  where 
+    noBody name tArgs args rets = do 
+      semi
+      specs <- many spec
+      return (ProcedureDecl name tArgs (ungroupWhere args) (ungroupWhere rets) specs Nothing)
+    withBody name tArgs args rets = do
+      specs <- many spec
+      b <- body
+      return (ProcedureDecl name tArgs (ungroupWhere args) (ungroupWhere rets) specs (Just b))
+
+implDecl :: Parser BareDecl
+implDecl = do
+  reserved "implementation"
+  many attribute
+  name <- identifier
+  tArgs <- typeArgs
+  args <- parens (commaSep idsType)
+  rets <- option [] (reserved "returns" >> parens (commaSep idsType))
+  bs <- many body
+  return $ ImplementationDecl name tArgs (ungroup args) (ungroup rets) bs
+  
+-- | Top-level declaration parser  
+decl :: Parser Decl
+decl = attachPosBefore (choice [
+  typeDecl,
+  constantDecl,
+  functionDecl, 
+  axiomDecl, 
+  varDecl, 
+  procDecl, 
+  implDecl
+  ] <?> "declaration")
+  
+{- Contracts -}
+
+spec :: Parser Contract
+spec = do
+  free <- hasKeyword "free"
+  choice [
+    do
+      reserved "requires"
+      e <- expression
+      semi
+      return $ Requires free e,
+    do
+      reserved "modifies"
+      ids <- commaSep identifier
+      semi
+      return $ Modifies free ids,
+    do
+      reserved "ensures"
+      e <- expression
+      semi
+      return $ Ensures free e]
+
+{- Misc -}
+
+hasKeyword :: String -> Parser Bool
+hasKeyword s = option False (reserved s >> return True)
+
+idsType :: Parser ([Id], Type)
+idsType = do
+  ids <- commaSep1 identifier
+  reservedOp ":"
+  t <- type_
+  return (ids, t)
+
+ungroup :: [([Id], Type)] -> [(IdType)]
+ungroup = concatMap (\x -> zip (fst x) (repeat (snd x)))
+
+idsTypeWhere :: Parser ([Id], Type, Expression)
+idsTypeWhere = do
+  ids <- idsType
+  pos <- getPosition
+  e <- option (attachPos pos TT) (reserved "where" >> expression)
+  return ((fst ids), (snd ids), e)
+
+ungroupWhere :: [([Id], Type, Expression)] -> [IdTypeWhere]
+ungroupWhere = concatMap ungroupWhereOne
+  where ungroupWhereOne (ids, t, e) = zipWith3 IdTypeWhere ids (repeat t) (repeat e)
+
+trigAttr :: Parser ()
+trigAttr = (try trigger) <|> attribute <?> "attribute or trigger"
+
+trigger :: Parser ()
+trigger = void (braces (commaSep1 expression)) <?> "trigger"
+
+attribute :: Parser ()
+attribute = void (braces (do
+  reservedOp ":"
+  identifier
+  commaSep1 (void expression <|> void stringLiteral)
+  )) <?> "attribute"
+  

@@ -0,0 +1,61 @@+-- | Utility for attaching source code positions to AST nodes
+module Language.Boogie.Position 
+    (Pos (..)
+    ,SourcePos
+
+    ,sourceLine
+    ,sourceColumn
+    ,sourceName
+
+    ,noPos
+    ,attachPos
+    ,gen
+    ,attachPosBefore
+    ,inheritPos
+    ,inheritPos2
+
+    ) where
+
+import Control.Monad
+import Text.ParserCombinators.Parsec
+import Text.Parsec.Pos
+
+-- | Anything with a source position attached 
+data Pos a = Pos {
+  position :: SourcePos,
+  node :: a
+}
+
+instance Eq a => Eq (Pos a) where
+    (==) p1 p2 = node p1 == node p2
+
+instance Show a => Show (Pos a) where
+    show p = show (node p)
+
+instance Functor Pos where
+    fmap f (Pos s a) = Pos s (f a)
+    
+-- | Attach position to a node    
+attachPos :: SourcePos -> a -> Pos a
+attachPos = Pos
+
+-- | Dummy source position
+noPos = (initialPos "<no file name>")
+
+-- | Attach dummy position to a node
+gen = attachPos noPos
+
+attachPosM :: Monad m => m SourcePos -> m a -> m (Pos a)
+attachPosM = liftM2 attachPos
+
+-- | 'attachPosBefore' @p@ : parser that behaves like @p@, but also attaches the source position before the first token it parsed to the result
+attachPosBefore :: Parser a -> Parser (Pos a)
+attachPosBefore = attachPosM getPosition
+
+-- | 'inheritPos' @f a@ : apply @f@ to @a@ and attach @a@'s position to the result
+inheritPos :: (Pos a -> b) -> Pos a -> Pos b
+inheritPos f a = attachPos (position a) (f a)
+
+-- | 'inheritPos2' @f a b@ : apply @f@ to @a@ and @b@ and attach @a@'s position to the result
+inheritPos2 :: (Pos a -> Pos b -> c) -> Pos a -> Pos b -> Pos c
+inheritPos2 f a b = attachPos (position a) (f a b)

@@ -0,0 +1,324 @@+-- | Pretty printer for Boogie 2
+module Language.Boogie.PrettyPrinter (
+  -- * Pretty-printing programs
+  programDoc,
+  renderWithTabs,
+  typeDoc,
+  exprDoc,
+  statementDoc,
+  declDoc,
+  -- * Utility
+  newline,
+  vsep,
+  commaSep,
+  angles,
+  spaces,  
+  option,
+  optionMaybe,
+  unOpDoc,
+  binOpDoc,
+  sigDoc
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Position
+import Language.Boogie.Tokens
+import Data.Maybe
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Text.PrettyPrint
+  
+{- Interface -}
+
+-- | Pretty-printed program
+programDoc :: Program -> Doc
+programDoc (Program decls) = (vsep . punctuate newline . map declDoc) decls
+
+instance Show Program where show p = show (programDoc p)
+
+-- | Render document with tabs instead of spaces
+renderWithTabs = fullRender (mode style) (lineLength style) (ribbonsPerLine style) spacesToTabs ""
+  where
+    spacesToTabs :: TextDetails -> String -> String
+    spacesToTabs (Chr c) s  = c:s
+    spacesToTabs (Str s1) s2 = if s1 == replicate (length s1) ' ' && length s1 > 1 
+      then replicate (length s1 `div` defaultIndent) '\t' ++ s2 
+      else s1 ++ s2
+      
+{- Tokens -}
+
+-- | Pretty-printed unary operator
+unOpDoc op = text (opName op unOpTokens)
+-- | Pretty-printed binary operator
+binOpDoc op = text (opName op binOpTokens)
+-- | Pretty-printed quantifier
+qOpDoc op = text (opName op qOpTokens)
+
+{- Types -}
+
+-- | Pretty-printed type
+typeDoc :: Type -> Doc
+typeDoc BoolType = text "bool"
+typeDoc IntType = text "int"
+typeDoc (MapType fv domains range) = typeArgsDoc fv <> 
+  brackets (commaSep (map typeDoc domains)) <+>
+  typeDoc range
+typeDoc (Instance id args) = text id <+> hsep (map typeDoc args)
+
+instance Show Type where show t = show (typeDoc t)
+
+-- | Pretty-printed function or procedure signature
+sigDoc :: [Type] -> [Type] -> Doc
+sigDoc argTypes retTypes = parens(commaSep (map typeDoc argTypes)) <+> 
+  text "returns" <+> 
+  parens(commaSep (map typeDoc retTypes))
+  
+{- Expressions -}
+
+-- | Binding power of an expression
+power :: BareExpression -> Int
+power TT = 10
+power FF = 10
+power (Numeral _) = 10
+power (Var _) = 10
+power (Application _ _) = 10
+power (Old _) = 10
+power (IfExpr _ _ _) = 10
+power (Quantified _ _ _ _) = 10
+power (MapSelection _ _) = 9
+power (MapUpdate _ _ _) = 9
+power (Coercion _ _) = 8
+power (UnaryExpression _ _) = 7
+power (BinaryExpression op _ _) 
+  | op `elem` [Times, Div, Mod] = 6 
+  | op `elem` [Plus, Minus] = 5
+  | op `elem` [Eq, Neq, Ls, Leq, Gt, Geq, Lc] = 3
+  | op `elem` [And, Or] = 2
+  | op `elem` [Implies, Explies] = 1
+  | op `elem` [Equiv] = 0
+
+-- | Pretty-printed expression  
+exprDoc :: Expression -> Doc
+exprDoc e = exprDocAt (-1) e
+
+-- | 'exprDocAt' @n expr@ : print @expr@ in a context with binding power @n@
+exprDocAt :: Int -> Expression -> Doc
+exprDocAt n (Pos _ e) = condParens (n' <= n) (
+  case e of
+    FF -> text "false"
+    TT -> text "true"
+    Numeral n -> integer n
+    Var id -> text id
+    Application id args -> text id <> parens (commaSep (map exprDoc args))
+    MapSelection m args -> exprDocAt n' m <> brackets (commaSep (map exprDoc args))
+    MapUpdate m args val -> exprDocAt n' m <> brackets (commaSep (map exprDoc args) <+> text ":=" <+> exprDoc val)
+    Old e -> text "old" <+> parens (exprDoc e)
+    IfExpr cond e1 e2 -> text "if" <+> exprDoc cond <+> text "then" <+> exprDoc e1 <+> text "else" <+> exprDoc e2
+    Coercion e t -> exprDocAt n' e <+> text ":" <+> typeDoc t
+    UnaryExpression unOp e -> unOpDoc unOp <> exprDocAt n' e
+    BinaryExpression binOp e1 e2 -> exprDocAt n' e1 <+> binOpDoc binOp <+> exprDocAt n' e2
+    Quantified qOp fv vars e -> parens (qOpDoc qOp <+> typeArgsDoc fv <+> commaSep (map idTypeDoc vars) <+> text "::" <+> exprDoc e)
+  )
+  where
+    n' = power e
+    
+instance Show BareExpression where show e = show (exprDoc (gen e))      
+
+{- Statements -}
+
+-- | Pretty-printed statement
+statementDoc :: Statement -> Doc
+statementDoc (Pos _ s) = case s of
+  Predicate (SpecClause _ isAssume e) -> (if isAssume then text "assume" else text "assert") <+> exprDoc e <> semi
+  Havoc vars -> text "havoc" <+> commaSep (map text vars) <> semi
+  Assign lhss rhss -> commaSep (map lhsDoc lhss) <+> 
+    text ":=" <+> commaSep (map exprDoc rhss) <> semi
+  Call lhss name args -> text "call" <+>
+    commaSep (map text lhss) <+>
+    option (not (null lhss)) (text ":=") <+> 
+    text name <> 
+    parens (commaSep (map exprDoc args)) <> 
+    semi
+  CallForall name args -> text "call forall" <+> 
+    text name <> 
+    parens (commaSep (map wildcardDoc args)) <> 
+    semi
+  If cond thenBlock elseBlock -> text "if" <+> parens (wildcardDoc cond) <+> 
+    bracedBlockDoc thenBlock <+>
+    optionMaybe elseBlock elseDoc
+  While cond invs b -> text "while" <+> parens (wildcardDoc cond) $+$
+    nestDef (vsep (map specClauseDoc invs)) $+$
+    bracedBlockDoc b
+  Break ml -> text "break" <+> optionMaybe ml text <> semi
+  Return -> text "return" <> semi
+  Goto ids -> text "goto" <+> commaSep (map text ids) <> semi
+  Skip -> empty
+  where
+    lhsDoc (id, selects) = text id <> hcat (map (\sel -> brackets (commaSep (map exprDoc sel))) selects)
+    wildcardDoc Wildcard = text "*"
+    wildcardDoc (Expr e) = exprDoc e
+    elseDoc b = text "else" <+> bracedBlockDoc b
+    
+instance Show BareStatement where show s = show (statementDoc (gen s))   
+
+{- Blocks -}
+
+blockDoc block = vsep (map lStatementDoc block)
+  where
+    lStatementDoc (Pos _ (lbs, s)) = hsep (map labelDoc lbs) <+> statementDoc s
+    
+bracedBlockDoc block = 
+  lbrace $+$
+  nestDef (blockDoc block) $+$
+  rbrace
+    
+bodyDoc (vars, block) =
+  lbrace $+$
+  nestDef (vsep (map varDeclDoc vars) $+$ blockDoc block) $+$
+  rbrace
+  
+transformedBlockDoc block = vsep (map basicBlockDoc block)
+  where
+    basicBlockDoc (l, stmts) = labelDoc l $+$ 
+      nestDef (vsep (map statementDoc stmts))
+
+labelDoc l = text l <> text ":"
+
+{- Specs -}     
+
+specTypeDoc Precondition = text "precondition"
+specTypeDoc Postcondition = text "postcondition"
+specTypeDoc LoopInvariant = text "invariant"
+
+specClauseDoc (SpecClause t free e) = option free (text "free") <+> specTypeDoc t <+> exprDoc e <> semi
+
+{- Declarations -}
+
+-- | Pretty-printed top-level declaration
+declDoc :: Decl -> Doc
+declDoc (Pos pos d) = case d of
+  TypeDecl ts -> typeDeclDoc ts
+  ConstantDecl unique names t orderSpec complete -> constantDoc unique names t orderSpec complete
+  FunctionDecl name fv args ret mb -> functionDoc name fv args ret mb
+  AxiomDecl e -> text "axiom" <+> exprDoc e <> semi
+  VarDecl vars -> varDeclDoc vars
+  ProcedureDecl name fv args rets specs mb -> procedureDoc name fv args rets specs mb
+  ImplementationDecl name fv args rets bodies -> implementationDoc name fv args rets bodies
+  
+instance Show BareDecl where show d = show (declDoc (gen d))  
+  
+typeDeclDoc ts = 
+  text "type" <+> 
+  commaSep (map newTypeDoc ts) <> 
+  semi
+  where
+    newTypeDoc (NewType id args mVal) = text id <+> hsep (map text args) <+> optionMaybe mVal (\t -> text "=" <+> typeDoc t)
+    
+constantDoc unique names t orderSpec complete =
+  text "const" <+>
+  option unique (text "unique") <+>
+  commaSep (map text names) <>
+  text ":" <+> typeDoc t <+>
+  optionMaybe orderSpec orderSpecDoc <+>
+  option complete (text "complete") <> 
+  semi
+  where
+    orderSpecDoc parents = text "extends" <+> commaSep (map parentDoc parents)
+    parentDoc (u, id) = option u (text "unique") <+> text id
+    
+functionDoc name fv args ret mb =
+  text "function" <+>
+  text name <>
+  typeArgsDoc fv <>
+  parens (commaSep (map fArgDoc args)) <+>
+  text "returns" <+>
+  parens (fArgDoc ret) <>
+  option (isNothing mb) semi $+$
+  optionMaybe mb (braces . spaces . exprDoc)
+  where
+    fArgDoc (Nothing, t) = typeDoc t
+    fArgDoc (Just id, t) = idTypeDoc (id, t) 
+    
+varDeclDoc vars =
+  text "var" <+>
+  commaSep (map idTypeWhereDoc vars) <>
+  semi
+      
+procedureDoc name fv args rets specs mb =
+  text "procedure" <+>
+  text name <>
+  typeArgsDoc fv <>
+  parens (commaSep (map idTypeWhereDoc args)) <+>
+  text "returns" <+>
+  parens (commaSep (map idTypeWhereDoc rets)) <>
+  option (isNothing mb) semi $+$
+  nestDef (vsep (map specDoc specs)) $+$
+  optionMaybe mb bodyDoc
+  where
+    specDoc (Requires free e) = option free (text "free") <+>
+      text "requires" <+>
+      exprDoc e <>
+      semi
+    specDoc (Ensures free e) = option free (text "free") <+>
+      text "ensures" <+>
+      exprDoc e <>
+      semi
+    specDoc (Modifies free ids) = option free (text "free") <+>
+      text "modifies" <+>
+      commaSep (map text ids) <>
+      semi
+    
+implementationDoc name fv args rets bodies =
+  text "implementation" <+>
+  text name <>
+  typeArgsDoc fv <>
+  parens (commaSep (map idTypeDoc args)) <+>
+  text "returns" <+>
+  parens (commaSep (map idTypeDoc rets)) $+$
+  vsep (map bodyDoc bodies)
+  
+{- Misc -}
+  
+defaultIndent = 4
+nestDef = nest defaultIndent
+
+-- | New line
+newline = char '\n'
+-- | Separate by new lines
+vsep = foldr ($+$) empty
+-- | Separate by commas
+commaSep = hsep . punctuate comma
+-- | Enclose in \< \>
+angles d = langle <> d <> rangle
+  where
+    langle = char '<'
+    rangle = char '>'
+-- | Enclose in spaces    
+spaces d = space <> d <> space
+
+-- | Conditionally produce a doc
+option b doc = if b then doc else empty
+
+-- | Convert a 'Just' value to doc
+optionMaybe mVal toDoc = case mVal of
+  Nothing -> empty
+  Just val -> toDoc val
+  
+-- | Conditionally enclose in parentheses  
+condParens b doc = if b then parens doc else doc
+    
+-- | Pretty-printed type arguments     
+typeArgsDoc tv = option (not (null tv)) (angles (commaSep (map text tv)))
+
+-- | Pretty-printed name declaration
+idTypeDoc (id, t) = text id <> text ":" <+> typeDoc t
+
+-- | Pretty-printed name declaration with a where clause
+idTypeWhereDoc (IdTypeWhere id t w) = idTypeDoc (id, t) <+> case w of
+  (Pos _ TT) -> empty
+  e -> text "where" <+> exprDoc e
+  
+instance Eq Doc where
+  d1 == d2 = show d1 == show d2
+  
+  

@@ -0,0 +1,301 @@+-- | Automated specification-based tester
+module Language.Boogie.Tester (
+  -- * Running tests
+  testProgram,
+  testSessionSummary,
+  -- * Configurng test sessions
+  TestSettings (..),
+  defaultGenericTypeRange,
+  defaultMapTypeRange,
+  ExhaustiveSettings (..),
+  RandomSettings (..),
+  -- * Testing results
+  Outcome (..),
+  outcomeDoc,
+  TestCase (..),
+  testCaseDoc,
+  Summary (..),
+  summaryDoc
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position
+import Language.Boogie.TypeChecker
+import Language.Boogie.Tokens
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.Interpreter
+import Language.Boogie.DataFlow
+import System.Random
+import Data.Maybe
+import Data.List
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.Error
+import Control.Applicative
+import Control.Monad.State
+import Text.PrettyPrint
+
+{- Interface -}
+    
+-- | 'testProgram' @settings p tc procNames@ : 
+-- Test all implementations of all procedures @procNames@ from program @p@ in type context @tc@;
+-- requires that all @procNames@ exist in @tc@
+testProgram :: TestSettings s => s -> Program -> Context -> [Id] -> [TestCase]
+testProgram settings p tc procNames = evalState testExecution (settings, initEnvironment)
+  where
+    initEnvironment = emptyEnv { envTypeContext = tc }
+    testExecution = do
+      changeState snd (mapSnd . const) $ collectDefinitions p
+      concat <$> forM procNames testProcedure
+    -- | Test all implementations of procedure name
+    testProcedure name = do
+      sig <- gets (procSig name . envTypeContext . snd) 
+      defs <- gets (lookupProcedure name . snd)
+      concat <$> forM defs (testImplementation sig)
+      
+-- | Summary of a set of test cases   
+testSessionSummary :: [TestCase] -> Summary
+testSessionSummary tcs = let 
+  passing = [ x | x@(TestCase _ _ _ _ Pass)         <- tcs ]
+  failing = [ x | x@(TestCase _ _ _ _ (Fail _))     <- tcs ]
+  invalid = [ x | x@(TestCase _ _ _ _ (Invalid _))  <- tcs ]
+  in Summary {
+    sPassCount = length passing,
+    sFailCount = length failing,
+    sInvalidCount = length invalid,  
+    sUniqueFailures = nubBy equivalent failing
+  }
+            
+{- Testing session parameters -}
+
+-- | Test session parameters
+class TestSettings s where
+  -- | How should input values for an integer variable be generated?
+  generateIntInput :: State s [Integer]
+  -- | How should input values for a boolean variable be generated?
+  generateBoolInput :: State s [Bool]
+  -- | How should input values for several variables be combined?
+  combineInputs :: (a -> State s [b]) -> [a] -> State s [[b]]
+  -- | Settings for generating map domains (always exhaustive)
+  mapDomainSettings :: s -> ExhaustiveSettings
+  -- | Range of instances for a type parameter of a generic procedure under test 
+  genericTypeRange :: s -> [Type]
+  -- | Range of instances for a type parameter of a polymorphic map
+  mapTypeRange :: s -> [Type]
+  
+-- | Default range for instantiating procedure type parameters:
+-- using a single type bool is enough unless the program contains a function or a map that allows differentiating between types at runtime
+defaultGenericTypeRange _ = [BoolType]
+
+-- | Default range for instantiating polymorphic maps:
+-- all nullary type constructors
+defaultMapTypeRange context = [BoolType, IntType] ++ [Instance name [] | name <- M.keys (M.filter (== 0) (ctxTypeConstructors context))]  
+  
+-- | Settings for exhaustive testing  
+data ExhaustiveSettings = ExhaustiveSettings {
+  esIntRange :: [Integer],            -- ^ Input range for an integer variable
+  esIntMapDomainRange :: [Integer],   -- ^ Input range for an integer map domain
+  esGenericTypeRange :: [Type],       -- ^ Range of instances for a type parameter of a generic procedure under test 
+  esMapTypeRange :: [Type]            -- ^ Range of instances for a type parameter of a polymorphic map
+}
+
+instance TestSettings ExhaustiveSettings where
+  -- | Return all integers within limits  
+  generateIntInput = gets esIntRange
+  -- | Return both booleans
+  generateBoolInput = return [False, True]      
+  -- | Use all combinations of inputs for each variable   
+  combineInputs genOne args = sequence <$> mapM genOne args
+  mapDomainSettings s = s { esIntRange = esIntMapDomainRange s }  
+  genericTypeRange = esGenericTypeRange
+  mapTypeRange = esMapTypeRange
+  
+-- | Settings for random testing  
+data RandomSettings = RandomSettings {
+  rsRandomGen :: StdGen,              -- ^ Random number generator
+  rsCount :: Int,                     -- ^ Number of test cases to be generated (currently per type in 'rsGenericTypeRange', if the procedure under test is generic)
+  rsIntLimits :: (Integer, Integer),  -- ^ Lower and upper bound for integer inputs
+  rsIntMapDomainRange :: [Integer],   -- ^ Input range for an integer map domain
+  rsGenericTypeRange :: [Type],       -- ^ Range of instances for a type parameter of a generic procedure under test 
+  rsMapTypeRange :: [Type]            -- ^ Range of instances for a type parameter of a polymorphic map
+}
+
+setRandomGen gen rs = rs { rsRandomGen = gen }
+
+instance TestSettings RandomSettings where
+  -- | Generate rsCount random values within limits
+  generateIntInput = do
+    randomGen <- gets rsRandomGen
+    limits <- gets rsIntLimits
+    n <- gets rsCount
+    changeState rsRandomGen setRandomGen $ replicateM n (state (randomR limits))
+    
+  -- | Generate rsCount random values within limits  
+  generateBoolInput = do
+    randomGen <- gets rsRandomGen
+    n <- gets rsCount
+    changeState rsRandomGen setRandomGen $ replicateM n (state random)    
+  
+  -- | Generate rsCount random tuples of values
+  combineInputs genOne args = transpose <$> mapM genOne args
+  
+  -- | Integer map domains are intervals [0..rsIntMapDomainSize s - 1]  
+  mapDomainSettings s = ExhaustiveSettings { 
+    esIntRange = rsIntMapDomainRange s,
+    esIntMapDomainRange = rsIntMapDomainRange s,
+    esGenericTypeRange = rsGenericTypeRange s,
+    esMapTypeRange = rsMapTypeRange s
+    }  
+      
+  genericTypeRange = rsGenericTypeRange
+  mapTypeRange = rsMapTypeRange
+
+-- | Executions that have access to testing session parameters
+type TestSession s a = State (s, Environment) a
+        
+{- Reporting results -}
+
+instance Eq RuntimeFailure where
+  -- Runtime errors are considered equivalent if the same property failed at the same program location 
+  f == f'   =  rtfSource f == rtfSource f' && rtfPos f == rtfPos f' 
+
+-- | Outcome of a test case        
+data Outcome = Pass | Fail RuntimeFailure | Invalid RuntimeFailure
+  deriving Eq
+
+-- | Pretty-printed outcome  
+outcomeDoc :: Outcome -> Doc
+outcomeDoc Pass = text "passed"
+outcomeDoc (Fail err) = text "failed: " <+> runtimeFailureDoc err
+outcomeDoc (Invalid err) = text "invalid: " <+> runtimeFailureDoc err
+
+instance Show Outcome where show o = show (outcomeDoc o)
+
+-- | Description of a test case
+data TestCase = TestCase {
+  tcProcedure :: Id,      -- ^ Procedure under test
+  tcLiveIns :: [Id],      -- ^ Input parameters for which an input value was generated
+  tcLiveGlobals :: [Id],  -- ^ Global variables for which an input value was generated
+  tcInput :: [Value],     -- ^ Values for in-parameters
+  tcOutcome :: Outcome    -- ^ Outcome
+} deriving Eq
+
+-- | Pretty-printed test case
+testCaseDoc :: TestCase -> Doc
+testCaseDoc (TestCase procName liveIns liveGlobals input outcome) = text procName <> 
+  parens (commaSep (zipWith argDoc (liveIns ++ (map ("var " ++) liveGlobals)) input)) <+>
+  outcomeDoc outcome
+  where
+    argDoc name val = text name <+> text "=" <+> valueDoc val
+
+instance Show TestCase where show tc = show (testCaseDoc tc)
+
+-- | Test cases are considered equivalent from a user perspective
+-- | if they are testing the same procedure and result in the same outcome
+equivalent tc1 tc2 = tcProcedure tc1 == tcProcedure tc2 && tcOutcome tc1 == tcOutcome tc2      
+
+-- | Test session summary
+data Summary = Summary {
+  sPassCount :: Int,            -- ^ Number of passing test cases
+  sFailCount :: Int,            -- ^ Number of failing test cases
+  sInvalidCount :: Int,         -- ^ Number of invalid test cases
+  sUniqueFailures :: [TestCase] -- ^ Unique failing test cases
+}
+
+totalCount s = sPassCount s + sFailCount s + sInvalidCount s
+
+-- | Pretty-printed test session summary
+summaryDoc :: Summary -> Doc
+summaryDoc summary = 
+  text "Test cases:" <+> int (totalCount summary) $+$
+  text "Passed:" <+> int (sPassCount summary) $+$
+  text "Invalid:" <+> int (sInvalidCount summary) $+$
+  text "Failed:" <+> int (sFailCount summary) <+> parens (int (length (sUniqueFailures summary)) <+> text "unique") $+$
+  vsep (map testCaseDoc (sUniqueFailures summary))
+  
+instance Show Summary where show s = show (summaryDoc s)  
+    
+{- Test execution -}
+
+-- | Test implementation def of procedure sig on all inputs prescribed by the testing strategy
+testImplementation :: TestSettings s => PSig -> PDef -> TestSession s [TestCase] 
+testImplementation sig def = do
+  let paramTypes = map itwType (psigParams sig)
+  tc <- gets (envTypeContext . snd)
+  typeRange <- gets (genericTypeRange . fst)
+  -- all types the procedure signature should be instantiated with:
+  let typeInputs = generateInputTypes typeRange tc { ctxTypeVars = psigTypeVars sig } paramTypes  
+  concat <$> mapM typeTestCase typeInputs
+  where
+    -- | Execute procedure instantiated with typeInputs on all value inputs
+    typeTestCase :: TestSettings s => [Type] -> TestSession s [TestCase]
+    typeTestCase typeInputs = do
+      -- fresh name for a parameter at position index; to be used as actual parameter
+      let localName index = [nonIdChar] ++ show index
+      let localNames = map localName [0..length (psigParams sig) - 1]
+      -- declare local variables localNames with appropriate types:
+      modify $ mapSnd (modifyTypeContext (`setLocals` (M.fromList $ zip localNames typeInputs)))
+      tc <- gets (envTypeContext . snd)
+      
+      -- names of actual in- and out-parameters
+      let (inParams, outParams) = splitAt (length (psigArgs sig)) localNames      
+      
+      -- names of input variables (variables for which input values are generated);
+      -- input variables can be either in-parameters or global variables 
+      let (liveIns, liveGlobals) = liveInputVariables sig def
+      let livePositions = map (fromJust . (`elemIndex` pdefIns def)) liveIns 
+      let liveActualIns = map localName livePositions
+      let liveGlobalVars = filter (`M.member` ctxGlobals tc) liveGlobals
+      let inputVars = liveActualIns ++ liveGlobalVars
+            
+      -- types of input variables
+      let inTypes = map (typeInputs !!) livePositions ++ map (ctxGlobals tc !) liveGlobalVars      
+      
+      let execTestCase input = changeState snd (mapSnd . const) $ testCase inParams outParams inputVars input
+      let reportTestCase input = TestCase (psigName sig) liveIns liveGlobalVars input <$> execTestCase input
+      -- all inputs the procedure should be tested on:
+      let genInputs = combineInputs (generateInputValue tc) inTypes
+      inputs <- changeState fst (mapFst . const) genInputs 
+      mapM reportTestCase inputs
+    -- | Assign inputVals to inputVars, and execute procedure with actual in-parameter variables inParams and actual out-parameter variables outParams;
+    -- | inputVars contain some inParams and some globals variables
+    testCase :: [Id] -> [Id] -> [Id] -> [Value] -> SafeExecution Outcome
+    testCase inParams outParams inputVars inputVals = do
+      setAll inputVars inputVals
+      let inExpr = map (gen . Var) inParams
+      let outExpr = map (gen . Var) outParams
+      execSafely (execProcedure (assumePreconditions sig) def inExpr outExpr >> return Pass) failureReport
+    -- | Test case outcome in case of a runtime error err
+    failureReport err = if failureKind err == Unreachable || failureKind err == Nonexecutable
+      then return $ Invalid err
+      else return $ Fail err
+            
+{- Input generation -}
+    
+-- | generateInputValue c t: generate all values of type t in context c          
+generateInputValue :: TestSettings s => Context -> Type -> State s [Value]
+generateInputValue _ BoolType = map BoolValue <$> generateBoolInput
+generateInputValue _ IntType = map IntValue <$> generateIntInput
+generateInputValue c (MapType tv domains range) = do
+  typeRange <- gets mapTypeRange
+  let polyTypes = generateInputTypes typeRange c { ctxTypeVars = tv } (range : domains)
+  -- A polymorphic map is a union of monomorphic maps with all possible instantiations for type variables:
+  maps <- combineInputs monomorphicMap polyTypes
+  return $ map (MapValue . M.unions) maps
+  where
+    monomorphicMap (range : domains) = do 
+      -- Domain is always generated deterministically: 
+      args <- withLocalState mapDomainSettings (combineInputs (generateInputValue c) domains)
+      rets <- combineInputs (generateInputValue c) (replicate (length args) range)
+      return $ map (\r -> M.fromList (zip args r)) rets
+generateInputValue _ (Instance _ _) = map CustomValue <$> generateIntInput
+
+-- | All instantiations of types ts in context c, with a range of instances for a single type variables range 
+generateInputTypes :: [Type] -> Context -> [Type] -> [[Type]]
+generateInputTypes range c ts = do
+  let freeVars = filter (\x -> any (x `isFreeIn`) ts) (ctxTypeVars c)
+  actuals <- replicateM (length freeVars) range
+  let binding = M.fromList (zip freeVars actuals)
+  return $ map (typeSubst binding) ts
+  

@@ -0,0 +1,63 @@+-- | Tokens used in Boogie 2
+module Language.Boogie.Tokens where
+
+import Language.Boogie.AST
+import Data.Maybe
+
+-- | Keywords
+keywords :: [String]
+keywords = ["assert", "assume", "axiom", "bool", "break", "call", "complete", "const",
+    "else", "div", "ensures", "exists", "extends", "false", "forall", "free", "function",
+    "goto", "havoc", "if", "implementation", "int", "invariant", "lambda", "mod", "modifies",
+    "old", "procedure", "requires", "return", "returns", "then", "true", "type", "unique",
+    "var", "where", "while"]
+
+-- | 'opName' @op table@ : lookup operator name in @table@
+opName op table = fromJust (lookup op table)
+    
+-- | Names of unary operators    
+unOpTokens :: [(UnOp, String)]
+unOpTokens = [(Neg, "-"),
+              (Not, "!")]
+             
+-- | Names of binary operators             
+binOpTokens :: [(BinOp, String)]
+binOpTokens = [(Plus,    "+"),
+               (Minus,   "-"),
+               (Times,   "*"),
+               (Div,     "div"),
+               (Mod,     "mod"),
+               (And,     "&&"),
+               (Or,      "||"),
+               (Implies, "==>"),
+               (Explies, "<=="),
+               (Equiv,   "<==>"),
+               (Eq,      "=="),
+               (Neq,     "!="),
+               (Lc,      "<:"),
+               (Ls,      "<"),
+               (Leq,     "<="),
+               (Gt,      ">"),
+               (Geq,     ">=")]
+    
+-- | Names of quantifiers    
+qOpTokens :: [(QOp, String)]
+qOpTokens = [ (Forall, "forall"),
+              (Exists, "exists"),
+              (Lambda, "lambda") ]         
+         
+-- | Other operators         
+otherOps :: [String]
+otherOps = [":", ";", "::", ":=", "="] 
+
+-- | Characters allowed in identifiers (in addition to letters and digits)
+identifierChars = "_.$#\'`~^\\?"
+-- | Start of a multi-line comment
+commentStart = "/*"
+-- | End of a multi-line comment
+commentEnd = "*/"
+-- | Start of a single-line comment
+commentLine = "//"
+
+-- | A character that is not allowed in identifiers (used for generating unique names)
+nonIdChar = '*'         

@@ -0,0 +1,804 @@+-- | Type checker for Boogie 2
+module Language.Boogie.TypeChecker (
+  -- * Checking programs
+  checkProgram,
+  exprType,
+  resolve,
+  TypeError (..),
+  typeErrorsDoc,
+  Checked,  
+  -- * Typechecking context
+  Context (..),
+  emptyContext,
+  typeNames,
+  globalScope,
+  localScope,
+  mutableVars,
+  allVars,
+  allNames,
+  funProcNames,
+  funSig,
+  procSig,
+  setGlobals,
+  setIns,
+  setLocals,
+  setConstants,
+  enterFunction,
+  enterProcedure,
+  enterQuantified
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Util
+import Language.Boogie.Position
+import Language.Boogie.PrettyPrinter
+import Data.List
+import Data.Maybe
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import Control.Monad.Error
+import Control.Monad.Trans.Error hiding (throwError)
+import Control.Applicative
+import Text.PrettyPrint
+
+{- Interface -}
+
+-- | 'checkProgram' @p@ : Check program @p@ and return the type information in the global part of the context
+checkProgram :: Program -> Checked Context
+checkProgram (Program decls) = do
+  pass1  <- foldAccum collectTypes emptyContext decls                            -- collect type names from type declarations
+  _pass2 <- mapAccum_ (checkTypeSynonyms pass1) decls                            -- check values of type synonyms
+  _pass3 <- mapAccum_ (checkCycles pass1 decls) (M.keys (ctxTypeSynonyms pass1)) -- check that type synonyms do not form a cycle 
+  pass4  <- foldAccum checkSignatures pass1 decls                                -- check variable, constant, function and procedure signatures
+  pass5  <- foldAccum checkBodies pass4 decls                                    -- check axioms, function and procedure bodies, constant parent info
+  return pass5
+  
+-- | 'exprType' @c expr@ :
+-- Type of @expr@ in context @c@;
+-- fails if expr contains type errors.    
+exprType :: Context -> Expression -> Type
+exprType c expr = case checkExpression c expr of
+  Left _ -> (error . show) (text "encountered ill-typed expression during execution:" <+> exprDoc expr)
+  Right t -> t
+  
+-- | 'enterFunction' @sig formals actuals mRetType c@ :
+-- Local context of function @sig@ with formal arguments @formals@ and actual arguments @actuals@
+-- in a context where the return type is exprected to be @mRetType@ (if known)
+enterFunction :: FSig -> [Id] -> [Expression] -> Maybe Type -> Context -> Context 
+enterFunction sig formals actuals mRetType c = c 
+  {
+    ctxTypeVars = [],
+    ctxIns = M.fromList (zip formals argTypes),
+    ctxLocals = M.empty,
+    ctxModifies = [],
+    ctxTwoState = False,
+    ctxInLoop = False
+  }
+  where 
+    inst = case fInstance c sig actuals mRetType of
+      Left _ -> (error . show) (text "encountered ill-typed function application during execution:" <+> 
+        text (fsigName sig) <+> parens (commaSep (map text formals)) <+>
+        text "to actual arguments" <+> parens (commaSep (map exprDoc actuals)))
+      Right u -> typeSubst u
+    argTypes = map inst (fsigArgTypes sig)
+
+-- | 'enterProcedure' @sig def actuals lhss c@ :
+-- Local context of procedure @sig@ with definition @def@ and actual arguments @actuals@
+-- in a call with left-hand sides @lhss@
+enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> Context 
+enterProcedure sig def actuals lhss c = c 
+  {
+    ctxTypeVars = [],
+    ctxIns = M.fromList $ zip ins inTypes,
+    ctxLocals = M.union (M.fromList $ zip localNames localTypes) (M.fromList $ zip outs outTypes),
+    ctxWhere = foldl addWhere (ctxWhere c) (zip (ins ++ outs ++ localNames) (paramWhere ++ localWhere)), 
+    ctxModifies = psigModifies sig,
+    ctxTwoState = True,
+    ctxInLoop = False
+  }
+  where
+    ins = pdefIns def
+    outs = pdefOuts def
+    locals = fst (pdefBody def)
+    inst = case pInstance c sig actuals lhss of
+      Left _ -> (error . show) (text "encountered ill-typed procedure call during execution:" <+> 
+        text (psigName sig) <+> text "with actual arguments" <+> parens (commaSep (map exprDoc actuals)) <+>
+        text "and left-hand sides" <+> parens (commaSep (map exprDoc lhss)))
+      Right u -> typeSubst u
+    inTypes = map inst (psigArgTypes sig)
+    outTypes = map inst (psigRetTypes sig)
+    localTypes = map (inst . itwType) locals
+    localNames = map itwId locals
+    addWhere m (id, w) = M.insert id w m
+    localWhere = map itwWhere locals
+    paramWhere = map (paramSubst sig def . itwWhere) (psigArgs sig ++ psigRets sig)
+   
+-- | Local context of a quantified expression   
+enterQuantified :: [Id] -> [IdType] -> Context -> Context 
+enterQuantified tv vars c = c' 
+  {
+    ctxIns = foldl addIn (ctxIns c) vars
+  }
+  where
+    c' = c { ctxTypeVars = tv }
+    addIn ins (id, t) = M.insert id (resolve c' t) ins
+
+{- Errors -}
+
+-- | Type error with a source position and a pretty-printed message
+data TypeError = TypeError SourcePos Doc
+
+instance ErrorList TypeError where
+  listMsg s = [TypeError noPos (text s)]
+
+-- | Pretty-printed type error  
+typeErrorDoc (TypeError pos msgDoc) = text "Type error in" <+> text (show pos) $+$ msgDoc  
+  
+-- | Pretty-printed list of type errors
+typeErrorsDoc errs = (vsep . punctuate newline . map typeErrorDoc) errs
+  
+-- | Result of type checking: either 'a' or a type error
+type Checked a = Either [TypeError] a
+
+-- | Throw a single type error
+throwTypeError pos msgDoc = throwError [TypeError pos msgDoc]
+
+-- | Error accumulator: used to store intermediate type checking results, when errors should be accumulated rather than reported immediately
+data ErrorAccum a = ErrorAccum [TypeError] a
+
+instance Monad ErrorAccum where
+  return x                = ErrorAccum [] x
+  ErrorAccum errs x >>= f = case (f x) of
+    ErrorAccum es v -> ErrorAccum (errs ++ es) v
+
+-- | Transform a type checking result and default value into an error accumlator
+accum :: Checked a -> a -> ErrorAccum a
+accum cx y = case cx of
+  Left e -> ErrorAccum e y
+  Right x -> ErrorAccum [] x    
+  
+-- | Transform an error accumulator back into a rgeular type checking result  
+report :: ErrorAccum a -> Checked a
+report (ErrorAccum [] x) = Right x
+report (ErrorAccum es _) = Left es  
+
+-- | 'foldAccum' @f c nodes@ :
+-- Apply type checking @f@ to all @nodes@ in the initial context @c@,
+-- accumulating errors from all @nodes@ and reporting them at the end;
+-- in case of success the modified context is passed on and in case of failure the context is unchanged
+foldAccum :: (a -> b -> Checked a) -> a -> [b] -> Checked a
+foldAccum f c nodes = report $ foldM (acc f) c nodes
+  where
+    acc f x y = accum (f x y) x
+    
+-- | 'mapAccum' @f def nodes@ :
+-- Apply type checking @f@ to all @nodes@,
+-- accumulating errors from all @nodes@ and reporting them at the end
+mapAccum :: (b -> Checked c) -> c -> [b] -> Checked [c]
+mapAccum f def nodes = report $ mapM (acc f) nodes  
+  where
+    acc f x  = accum (f x) def
+   
+-- | 'mapAccumA_' @f nodes@ :
+-- Apply type checking @f@ to all @nodes@ throwing away the result,
+-- accumulating errors from all @nodes@
+mapAccumA_ :: (a -> Checked ()) -> [a] -> ErrorAccum ()
+mapAccumA_ f nodes = mapM_ (acc f) nodes  
+  where
+    acc f x  = accum (f x) ()
+    
+-- | Same as 'mapAccumA_', but reporting the error at the end
+mapAccum_ :: (a -> Checked ()) -> [a] -> Checked ()
+mapAccum_ f nodes = report $ mapAccumA_ f nodes  
+
+-- | 'zipWithAccum_' @f xs ys@ :
+-- Apply type checking @f@ to all @xs@ and @ys@ throwing away the result,
+-- accumulating errors from all nodes and reporting them at the end
+zipWithAccum_ :: (a -> b -> Checked ()) -> [a] -> [b] -> Checked ()
+zipWithAccum_ f xs ys = report $ zipWithM_ (acc f) xs ys  
+  where
+    acc f x y  = accum (f x y) ()
+  
+{- Context -}
+
+-- | Typechecking context
+data Context = Context
+  {
+    -- Global context:
+    ctxTypeConstructors :: Map Id Int,      -- ^ type constructor arity
+    ctxTypeSynonyms :: Map Id ([Id], Type), -- ^ type synonym values
+    ctxGlobals :: Map Id Type,              -- ^ global variable types (type synonyms resolved)
+    ctxConstants :: Map Id Type,            -- ^ constant types (type synonyms resolved)
+    ctxFunctions :: Map Id FSig,            -- ^ function signatures (type synonyms resolved)
+    ctxProcedures :: Map Id PSig,           -- ^ procedure signatures (type synonyms resolved)
+    ctxWhere :: Map Id Expression,          -- ^ where clauses of variables (global and local)
+    
+    -- Local context:
+    ctxTypeVars :: [Id],                    -- ^ free type variables
+    ctxIns :: Map Id Type,                  -- ^ input parameter types
+    ctxLocals :: Map Id Type,               -- ^ local variable types
+    ctxModifies :: [Id],                    -- ^ variables in the modifies clause of the enclosing procedure
+    ctxLabels :: [Id],                      -- ^ all labels of the enclosing procedure body
+    ctxEncLabels :: [Id],                   -- ^ labels of all enclosing statements
+    ctxTwoState :: Bool,                    -- ^ is the context two-state? (procedure body or postcondition)
+    ctxInLoop :: Bool,                      -- ^ is context inside a loop body?
+    ctxPos :: SourcePos                     -- ^ position in the source code
+  }
+
+-- | Empty context  
+emptyContext = Context {
+    ctxTypeConstructors = M.empty,
+    ctxTypeSynonyms     = M.empty,
+    ctxGlobals          = M.empty,
+    ctxConstants        = M.empty,
+    ctxFunctions        = M.empty,
+    ctxProcedures       = M.empty,
+    ctxWhere            = M.empty,
+    ctxTypeVars         = [],
+    ctxIns              = M.empty,
+    ctxLocals           = M.empty,
+    ctxModifies         = [],
+    ctxLabels           = [],
+    ctxEncLabels        = [],
+    ctxTwoState         = False,
+    ctxInLoop           = False,
+    ctxPos              = noPos
+  }
+
+setGlobals ctx g    = ctx { ctxGlobals = g }
+setIns ctx i        = ctx { ctxIns = i }
+setLocals ctx l     = ctx { ctxLocals = l }
+setConstants ctx c  = ctx { ctxConstants = c }
+
+-- | Type constructors and synonyms
+typeNames c = M.keys (ctxTypeConstructors c) ++ M.keys (ctxTypeSynonyms c)
+-- | Global variables and constants
+globalScope c = M.union (ctxGlobals c) (ctxConstants c)
+-- | Input parameters and local variables
+localScope c = M.union (ctxIns c) (ctxLocals c)
+-- | All variables that can be assigned to (local variables and global variables)
+mutableVars c = M.union (ctxGlobals c) (ctxLocals c)
+-- | All variables that can have where clauses (everything except constants)
+allVars c = M.union (localScope c) (ctxGlobals c)
+-- | All variables and constants (local-scope preferred)
+allNames c = M.union (localScope c) (globalScope c)
+-- | Names of functions and procedures
+funProcNames c = M.keys (ctxFunctions c) ++ M.keys (ctxProcedures c)
+-- | Function signature by name
+funSig name c = ctxFunctions c ! name
+-- | Procedure signature by name
+procSig name c = ctxProcedures c ! name    
+  
+{- Types -}
+  
+-- | Check that a type variable is fresh and add it to context  
+checkTypeVar :: Context -> Id -> Checked Context
+checkTypeVar c v
+  | v `elem` typeNames c = throwTypeError (ctxPos c) (text v <+> text "already used as a type constructor or synonym")
+  | v `elem` ctxTypeVars c = throwTypeError (ctxPos c) (text "Multiple decalartions of type variable" <+> text v)
+  | otherwise = return c { ctxTypeVars = v : ctxTypeVars c }
+
+-- | 'checkType' @c t@ : check that @t@ is a correct type in context @c@ (i.e. that all type names exist and have correct number of arguments)
+checkType :: Context -> Type -> Checked ()
+checkType c (MapType tv domains range) = do
+  c' <- foldAccum checkTypeVar c tv
+  mapAccum_ (checkType c') (domains ++ [range])
+checkType c (Instance name args)
+  | name `elem` ctxTypeVars c && null args = return ()
+  | M.member name (ctxTypeConstructors c) = if n == length args 
+    then mapAccum_ (checkType c) args
+    else throwTypeError (ctxPos c) (text "Wrong number of arguments" <+> int (length args) <+> text "given to the type constructor" <+> text name <+> 
+      parens (text "expected" <+> int n))
+  | M.member name (ctxTypeSynonyms c) = if length formals == length args
+    then mapAccum_ (checkType c) args
+    else throwTypeError (ctxPos c) (text "Wrong number of arguments " <+> int (length args) <+> text "given to the type synonym" <+> text name <+> 
+      parens (text "expected" <+> int (length formals)))
+  | otherwise = throwTypeError (ctxPos c) (text "Not in scope: type constructor or synonym" <+> text name)
+    where 
+      n = ctxTypeConstructors c ! name
+      formals = fst (ctxTypeSynonyms c ! name)
+checkType _ _ = return ()
+
+-- | 'resolve' @c t@ : type @t@ with all type synonyms resolved according to binding in @c@
+resolve :: Context -> Type -> Type
+resolve c (MapType tv domains range) = MapType tv (map (resolve c') domains) (resolve c' range)
+  where c' = c { ctxTypeVars = ctxTypeVars c ++ tv }
+resolve c (Instance name args) 
+  | name `elem` ctxTypeVars c = Instance name args
+  | otherwise = case M.lookup name (ctxTypeSynonyms c) of
+    Nothing -> Instance name (map (resolve c) args)
+    Just (formals, t) -> resolve c (typeSubst (M.fromList (zip formals args)) t)
+resolve _ t = t
+
+-- | 'fInstance' @c sig actuals mRetType@ :
+-- Instantiation of type variables in a function signature @sig@ given the actual arguments @actuals@ in a context @c@
+-- and possibly a return type @mRetType@ (if known from the context)
+fInstance :: Context -> FSig -> [Expression] -> Maybe Type -> Checked TypeBinding
+fInstance c sig actuals mRetType = case mRetType of
+    Nothing -> if not (null retOnlyTVs) 
+      then throwTypeError (ctxPos c) (text "Cannot infer type arguments from the context:" <+> commaSep (map text retOnlyTVs) <+> text "(insert a coercion)")
+      else do
+        actualTypes <- mapAccum (checkExpression c) noType actuals
+        case oneSidedUnifier (fsigTypeVars sig) (fsigArgTypes sig) (ctxTypeVars c) actualTypes of
+          Nothing -> throwTypeError (ctxPos c) (text "Could not match formal argument types" <+> 
+            doubleQuotes (commaSep (map typeDoc (fsigArgTypes sig))) <+>
+            text "against actual argument types" <+> 
+            doubleQuotes (commaSep (map typeDoc actualTypes)) <+>
+            text "in the call to" <+> text (fsigName sig))
+          Just u -> return u
+    Just retType -> do
+      actualTypes <- mapAccum (checkExpression c) noType actuals
+      case oneSidedUnifier (fsigTypeVars sig) (fsigRetType sig : fsigArgTypes sig) (ctxTypeVars c) (retType : actualTypes) of
+        Nothing -> throwTypeError (ctxPos c) (text "Could not match function signature" <+> 
+          doubleQuotes (sigDoc (fsigArgTypes sig) [fsigRetType sig]) <+>
+          text "against actual types" <+> 
+          doubleQuotes (sigDoc actualTypes [retType]) <+>
+          text "in the call to" <+> text (fsigName sig))
+        Just u -> return u
+  where
+    tvs = fsigTypeVars sig
+    retOnlyTVs = filter (not . freeInArgs) tvs
+    freeInArgs tv = any (tv `isFreeIn`) (fsigArgTypes sig)
+      
+-- | 'pInstance' @c sig actuals lhss@ : 
+-- Instantiation of type variables in a procedure @sig@ given the actual arguments @actuals@ and call left-hand sides @lhss@, in a context @c@
+pInstance :: Context -> PSig -> [Expression] -> [Expression] -> Checked TypeBinding
+pInstance c sig actuals lhss = do
+  actualTypes <- mapAccum (checkExpression c) noType actuals
+  lhssTypes <- mapAccum (checkExpression c) noType lhss
+  case oneSidedUnifier (psigTypeVars sig) (psigArgTypes sig ++ psigRetTypes sig) (ctxTypeVars c) (actualTypes ++ lhssTypes) of
+    Nothing -> throwTypeError (ctxPos c) (text "Could not match procedure signature" <+> 
+      doubleQuotes (sigDoc (psigArgTypes sig) (psigRetTypes sig)) <+>
+      text "against actual types" <+> 
+      doubleQuotes (sigDoc actualTypes lhssTypes) <+>
+      text "in the call to" <+> text (psigName sig))
+    Just u -> return u    
+  
+{- Expressions -}
+
+-- | 'checkExpression' @c expr@ :
+-- Check that @expr@ is a valid expression in context @c@ and return its type
+-- (requires all types in the context be valid and type synonyms be resolved)
+checkExpression :: Context -> Expression -> Checked Type
+checkExpression c (Pos pos e) = case e of
+  TT -> return BoolType
+  FF -> return BoolType
+  Numeral n -> return IntType
+  Var id -> case M.lookup id (allNames c) of
+    Nothing -> throwTypeError pos (text "Not in scope: variable or constant" <+> text id)
+    Just t -> return t
+  Application id args -> checkApplication cPos id args Nothing
+  MapSelection m args -> checkMapSelection cPos m args
+  MapUpdate m args val -> checkMapUpdate cPos m args val
+  Old e1 -> if ctxTwoState c
+    then checkExpression c { ctxLocals = M.empty } e1
+    else throwTypeError pos (text "Old expression in a single state context")
+  IfExpr cond e1 e2 -> checkIfExpression cPos cond e1 e2
+  Coercion e t -> checkCoercion cPos e t
+  UnaryExpression op e1 -> checkUnaryExpression cPos op e1
+  BinaryExpression op e1 e2 -> checkBinaryExpression cPos op e1 e2
+  Quantified qop tv vars e -> checkQuantified cPos qop tv vars e
+  where
+    cPos = c { ctxPos = pos }
+
+-- @mRetType@ stores function return type if known from the context (currently: if used inside a coercion);
+-- it is a temporary workaround for generic return types of functions    
+checkApplication :: Context -> Id -> [Expression] -> Maybe Type -> Checked Type
+checkApplication c id args mRetType = case M.lookup id (ctxFunctions c) of
+  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: function" <+> text id)
+  Just sig -> do
+    u <- fInstance c sig args mRetType
+    return $ typeSubst u (fsigRetType sig)
+    
+checkMapSelection :: Context -> Expression -> [Expression] -> Checked Type
+checkMapSelection c m args = do
+  mType <- checkExpression c m
+  case mType of
+    MapType tv domainTypes rangeType -> do
+      actualTypes <- mapAccum (checkExpression c) noType args
+      case oneSidedUnifier tv domainTypes (ctxTypeVars c) actualTypes of
+        Nothing -> throwTypeError (ctxPos c) (text "Could not match map domain types" <+> doubleQuotes (commaSep (map typeDoc domainTypes)) <+>
+          text "against map selection types" <+> doubleQuotes (commaSep (map typeDoc actualTypes)) <+>
+          text "for the map" <+> exprDoc m)
+        Just u -> return (typeSubst u rangeType)
+    t -> throwTypeError (ctxPos c) (text "Map selection applied to a non-map" <+> exprDoc m <+> text "of type" <+> doubleQuotes (typeDoc t))
+  
+checkMapUpdate :: Context -> Expression -> [Expression] -> Expression -> Checked Type
+checkMapUpdate c m args val = do 
+  t <- checkMapSelection c m args
+  actualT <- checkExpression c val
+  if t <==> actualT 
+    then checkExpression c m 
+    else throwTypeError (ctxPos c) (text "Update value type" <+> doubleQuotes (typeDoc actualT) <+> text "different from map range type" <+> doubleQuotes (typeDoc t))
+    
+checkIfExpression :: Context -> Expression -> Expression -> Expression -> Checked Type    
+checkIfExpression c cond e1 e2 = do
+  compareType c "if-expression condition" BoolType cond
+  t <- checkExpression c e1
+  compareType c "else-part of the if-expression" t e2
+  return t
+  
+checkCoercion :: Context -> Expression -> Type -> Checked Type
+checkCoercion c e t = do
+  checkType c t
+  let t' = resolve c t
+  case node e of
+    Application id args -> checkApplication cPos id args (Just t')
+    _ -> compareType c "coerced expression" t' e >> return t'
+  where cPos = c { ctxPos = position e }
+    
+checkUnaryExpression :: Context -> UnOp -> Expression -> Checked Type
+checkUnaryExpression c op e
+  | op == Neg = matchType IntType IntType
+  | op == Not = matchType BoolType BoolType
+  where 
+    matchType t ret = do
+      t' <- checkExpression c e
+      if t' <==> t then return ret else throwTypeError (ctxPos c) (errorMsg t' op)
+    errorMsg t op = text "Invalid argument type" <+> doubleQuotes (typeDoc t) <+> text "to unary operator" <+> unOpDoc op
+  
+checkBinaryExpression :: Context -> BinOp -> Expression -> Expression -> Checked Type
+checkBinaryExpression c op e1 e2
+  | elem op [Plus, Minus, Times, Div, Mod] = matchTypes (\t1 t2 -> t1 <==> IntType && t2 <==> IntType) IntType
+  | elem op [And, Or, Implies, Explies, Equiv] = matchTypes (\t1 t2 -> t1 <==> BoolType && t2 <==> BoolType) BoolType
+  | elem op [Ls, Leq, Gt, Geq] = matchTypes (\t1 t2 -> t1 <==> IntType && t2 <==> IntType) BoolType
+  | elem op [Eq, Neq] = matchTypes (\t1 t2 -> isJust (unifier (ctxTypeVars c) [t1] [t2])) BoolType
+  | op == Lc = matchTypes (<==>) BoolType
+  where 
+    matchTypes pred ret = do
+      t1 <- checkExpression c e1
+      t2 <- checkExpression c e2
+      if pred t1 t2 then return ret else throwTypeError (ctxPos c) (errorMsg t1 t2 op)
+    errorMsg t1 t2 op = text "Invalid argument types" <+> doubleQuotes (typeDoc t1) <+> text "and" <+> doubleQuotes (typeDoc t2) <+> text "to binary operator" <+> binOpDoc op
+    
+checkQuantified :: Context -> QOp -> [Id] -> [IdType] -> Expression -> Checked Type
+checkQuantified c Lambda tv vars e = do
+  c' <- foldAccum checkTypeVar c tv
+  quantifiedScope <- foldAccum (checkIdType localScope ctxIns setIns) c' vars
+  if not (null missingTV)
+    then throwTypeError (ctxPos c) (text "Type variable(s) must occur among the types of lambda parameters:" <+> commaSep (map text missingTV)) 
+    else do
+      rangeType <- checkExpression quantifiedScope e
+      return $ MapType tv varTypes rangeType
+  where
+    varTypes = map snd vars
+    missingTV = filter (not . freeInVars) tv    
+    freeInVars v = any (v `isFreeIn`) varTypes      
+checkQuantified c qop tv vars e = do
+  c' <- foldAccum checkTypeVar c tv
+  quantifiedScope <- foldAccum (checkIdType localScope ctxIns setIns) c' vars
+  compareType quantifiedScope "quantified expression" BoolType e
+  return BoolType
+    
+{- Statements -}
+
+-- | 'checkStatement' @c st@ :
+-- Check that @st@ is a valid statement in context @c@
+checkStatement :: Context -> Statement -> Checked ()
+checkStatement c (Pos pos s) = case s of
+  Predicate (SpecClause _ _ e) -> compareType cPos "predicate" BoolType e
+  Havoc vars -> checkLefts cPos (nub vars) (length (nub vars))
+  Assign lhss rhss -> checkAssign cPos lhss rhss
+  Call lhss name args -> checkCall cPos lhss name args
+  CallForall name args -> checkCallForall cPos name args
+  If cond thenBlock elseBlock -> checkIf cPos cond thenBlock elseBlock
+  While cond invs b -> checkWhile cPos cond invs b
+  Goto ids -> checkGoto cPos ids
+  Break Nothing -> checkSimpleBreak cPos
+  Break (Just l) -> checkLabelBreak cPos l
+  _ -> return ()
+  where
+    cPos = c { ctxPos = pos }
+
+checkAssign :: Context -> [(Id , [[Expression]])] -> [Expression] -> Checked ()
+checkAssign c lhss rhss = do
+  checkLefts c (map fst lhss) (length rhss)
+  rTypes <- mapAccum (checkExpression c) noType rhss
+  zipWithAccum_ (compareType c "assignment left-hand side") rTypes (map selectExpr lhss) 
+  where
+    selectExpr (id, selects) = foldl mapSelectExpr (attachPos (ctxPos c) (Var id)) selects
+        
+checkCall :: Context -> [Id] -> Id -> [Expression] -> Checked ()
+checkCall c lhss name args = case M.lookup name (ctxProcedures c) of
+  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
+  Just sig -> let illegalModifies = psigModifies sig \\ ctxModifies c in
+    if not (null illegalModifies) 
+    then throwTypeError (ctxPos c) (text "Call modifies a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text illegalModifies))
+    else do
+      checkLefts c lhss (length $ psigRetTypes sig)
+      let lhssExpr = map (attachPos (ctxPos c) . Var) lhss
+      pInstance c sig args lhssExpr >> return ()      
+        
+checkCallForall :: Context -> Id -> [WildcardExpression] -> Checked ()
+checkCallForall c name args = case M.lookup name (ctxProcedures c) of
+  Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
+  Just sig -> if not (null (psigModifies sig)) 
+    then throwTypeError (ctxPos c) (text "Call forall to a procedure with a non-empty modifies clause")
+    else pInstance c sig { psigArgs = concrete (psigArgs sig) } concreteArgs [] >> return ()
+  where
+    concreteArgs = [e | (Expr e) <- args]
+    concrete at = [at !! i | i <- [0..length args - 1], isConcrete (args !! i)]
+    isConcrete Wildcard = False
+    isConcrete (Expr _) = True
+    
+checkIf :: Context -> WildcardExpression -> Block -> (Maybe Block) -> Checked ()
+checkIf c cond thenBlock elseBlock = report $ do
+  case cond of
+    Wildcard -> return ()
+    Expr e -> accum (compareType c "branching condition" BoolType e) ()
+  accum (checkBlock c thenBlock) ()
+  case elseBlock of
+    Nothing -> return ()
+    Just b -> accum (checkBlock c b) ()
+    
+checkWhile :: Context -> WildcardExpression -> [SpecClause] -> Block -> Checked ()
+checkWhile c cond invs body = report $ do
+  case cond of  
+    Wildcard -> return ()
+    Expr e -> accum (compareType c "loop condition" BoolType e) ()
+  mapAccumA_ (compareType c "loop invariant" BoolType) (map specExpr invs)
+  accum (checkBlock c {ctxInLoop = True} body) ()
+
+checkGoto :: Context -> [Id] -> Checked ()  
+checkGoto c ids = if not (null unknownLabels)
+  then throwTypeError (ctxPos c) (text "Not in scope: label(s)" <+> commaSep (map text unknownLabels))
+  else return ()
+  where
+    unknownLabels = ids \\ ctxLabels c 
+    
+checkSimpleBreak :: Context -> Checked ()
+checkSimpleBreak c = if not (ctxInLoop c)
+  then throwTypeError (ctxPos c) (text "Break statement outside a loop")
+  else return ()
+  
+checkLabelBreak :: Context -> Id -> Checked ()
+checkLabelBreak c l = if not (l `elem` ctxEncLabels c)
+  then throwTypeError (ctxPos c) (text "Break label" <+> text l <+> text "does not label an enclosing statement")
+  else return ()
+  
+{- Blocks -}
+
+-- | 'collectLabels' @c block@ : 
+-- Check that all labels in @block@ and nested blocks are unique and add them to the context
+collectLabels :: Context -> Block -> Checked Context
+collectLabels c block = foldAccum checkLStatement c block
+  where
+    checkLStatement c (Pos pos (ls, (Pos _ st))) = do
+      c' <- foldM (addLabel pos) c ls
+      case st of
+        If _ thenBlock mElseBlock -> do 
+          c'' <- collectLabels c' thenBlock
+          case mElseBlock of
+            Nothing -> return c''
+            Just elseBlock -> collectLabels c'' elseBlock
+        While _ _ bodyBlock -> collectLabels c' bodyBlock
+        _ -> return c'
+    addLabel pos c l = if l `elem` ctxLabels c 
+      then throwTypeError pos (text "Multiple occurrences of label" <+> text l <+> text "in a procedure body")
+      else return c {ctxLabels = l : ctxLabels c}
+
+-- | Check every statement in a block
+checkBlock :: Context -> Block -> Checked ()    
+checkBlock c block = mapAccum_ (checkLStatement c) block
+  where
+    checkLStatement c (Pos _ (ls, st)) = checkStatement c { ctxEncLabels = ctxEncLabels c ++ ls} st
+    
+{- Declarations -}
+
+-- | Collect type names from type declarations
+collectTypes :: Context -> Decl -> Checked Context
+collectTypes c (Pos pos d) = case d of
+  TypeDecl ts -> foldM checkTypeDecl c { ctxPos = pos } ts
+  otherwise -> return c  
+
+-- | Check uniqueness of type constructors and synonyms, and them in the context  
+checkTypeDecl :: Context -> NewType -> Checked Context 
+checkTypeDecl c (NewType name formals value)
+  | name `elem` (typeNames c) = throwTypeError (ctxPos c) (text "Multiple declarations of type constructor or synonym" <+> text name) 
+  | otherwise = case value of
+    Nothing -> return c { ctxTypeConstructors = M.insert name (length formals) (ctxTypeConstructors c) }
+    Just t -> return c { ctxTypeSynonyms = M.insert name (formals, t) (ctxTypeSynonyms c) }
+
+-- | Check that type arguments of type synonyms are fresh and values are valid types
+checkTypeSynonyms :: Context -> Decl -> Checked ()
+checkTypeSynonyms c (Pos pos d) = case d of
+  TypeDecl ts -> mapAccum_ (checkNewType c { ctxPos = pos }) ts
+  otherwise -> return ()
+  where
+    checkNewType c (NewType name formals (Just t)) = do
+      c' <- foldAccum checkTypeVar c formals 
+      checkType c' t
+    checkNewType _ _ = return ()
+
+-- | Check if type synonym declarations have cyclic dependences (program is passed for the purpose of error reporting)
+checkCycles :: Context -> [Decl] -> Id -> Checked ()
+checkCycles c decls id = checkCyclesWith c id (value id)
+  where
+    checkCyclesWith c id t = case t of
+      Instance name args -> do
+        if M.member name (ctxTypeSynonyms c)
+          then if id == name 
+            then throwTypeError firstPos (text "Cycle in the definition of type synonym" <+> text id) 
+            else checkCyclesWith c id (value name)
+          else return ()
+        mapAccum_ (checkCyclesWith c id) args
+      MapType _ domains range -> mapAccum_ (checkCyclesWith c id) (range:domains)
+      _ -> return ()
+    value name = snd (ctxTypeSynonyms c ! name)
+    firstPos = head [pos | Pos pos (TypeDecl ts) <- decls, id `elem` map tId ts]
+
+-- | Check variable, constant, function and procedures and add them to context
+checkSignatures :: Context -> Decl -> Checked Context
+checkSignatures c (Pos pos d) = case d of
+  VarDecl vars -> foldAccum (checkIdType globalScope ctxGlobals setGlobals) cPos (map noWhere vars)
+  ConstantDecl _ ids t _ _ -> foldAccum (checkIdType globalScope ctxConstants setConstants) cPos (zip ids (repeat t))
+  FunctionDecl name tv args ret _ -> checkFunctionSignature cPos name tv args ret
+  ProcedureDecl name tv args rets specs _ -> checkProcSignature cPos name tv args rets specs
+  otherwise -> return c
+  where
+    cPos = c { ctxPos = pos }
+
+-- | 'checkIdType' @scope get set c idType@ : 
+-- Check that declaration @idType@ is fresh in @scope@, and if so add it to @get c@ using @set c@
+checkIdType :: (Context -> Map Id Type) -> (Context -> Map Id Type) -> (Context -> Map Id Type -> Context) -> Context -> IdType -> Checked Context
+checkIdType scope get set c (i, t)   
+  | M.member i (scope c) = throwTypeError (ctxPos c) (text "Multiple declarations of variable or constant" <+> text i)
+  | otherwise = checkType c t >> return (c `set` M.insert i (resolve c t) (get c))
+
+-- | Check uniqueness of function name, types of formals and add function to context
+checkFunctionSignature :: Context -> Id -> [Id] -> [FArg] -> FArg -> Checked Context
+checkFunctionSignature c name tv args ret
+  | name `elem` funProcNames c = throwTypeError (ctxPos c) (text "Multiple declarations of function or procedure" <+> text name)
+  | otherwise = do
+    c' <- foldAccum checkTypeVar c tv
+    foldAccum checkFArg c' params
+    if not (null missingTV) 
+      then throwTypeError (ctxPos c) (text "Type variable(s) must occur in function arguments or return type:" <+> commaSep (map text missingTV))
+      else return $ addFSig c name (FSig name tv argTypes retType) 
+    where
+      params = args ++ [ret]
+      checkFArg c (Just id, t) = checkIdType ctxIns ctxIns setIns c (id, t)
+      checkFArg c (Nothing, t) = checkType c t >> return c
+      missingTV = filter (not . freeInParams) tv
+      freeInParams v = any (v `isFreeIn`) (map snd params)
+      addFSig c name sig = c { ctxFunctions = M.insert name sig (ctxFunctions c) }
+      argTypes = map (resolve c . snd) args
+      retType = (resolve c . snd) ret
+      
+-- | Check uniqueness of procedure name, types of formals and add procedure to context      
+checkProcSignature :: Context -> Id -> [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> Checked Context
+checkProcSignature c name tv args rets specs
+  | name `elem` funProcNames c = throwTypeError (ctxPos c) (text "Multiple declarations of function or procedure" <+> text name)
+  | otherwise = do
+    c' <- foldAccum checkTypeVar c tv
+    foldAccum checkPArg c' params
+    if not (null missingTV) 
+      then throwTypeError (ctxPos c) (text "Type variable(s) must occur in procedure in- our out-parameters:" <+> commaSep (map text missingTV))
+      else return $ addPSig c name (PSig name tv (map resolveType args) (map resolveType rets) specs)
+    where
+      params = args ++ rets
+      checkPArg c arg = checkIdType ctxIns ctxIns setIns c (noWhere arg)
+      missingTV = filter (not . freeInParams) tv
+      freeInParams v = any (v `isFreeIn`) (map itwType params)
+      addPSig c name sig = c { ctxProcedures = M.insert name sig (ctxProcedures c) }
+      resolveType (IdTypeWhere id t w) = IdTypeWhere id (resolve c t) w
+
+-- | Check axioms, function and procedure bodies      
+checkBodies :: Context -> Decl -> Checked Context
+checkBodies c (Pos pos d) = case d of
+  VarDecl vars -> foldAccum checkWhere cPos vars
+  ConstantDecl _ ids t (Just edges) _ -> checkParentInfo cPos ids t (map snd edges) >> return c
+  FunctionDecl name tv args ret (Just body) -> checkFunction cPos name tv args body >> return c
+  AxiomDecl e -> checkAxiom cPos e >> return c
+  ProcedureDecl name tv args rets specs mb -> checkProcedure cPos tv args rets specs mb >> return c
+  ImplementationDecl name tv args rets bodies -> checkImplementation cPos name tv args rets bodies >> return c
+  otherwise -> return c
+  where
+    cPos = c { ctxPos = pos }  
+  
+-- | Check that where-part is a valid boolean expression
+checkWhere :: Context -> IdTypeWhere -> Checked Context
+checkWhere c var = do
+  compareType c "where clause" BoolType (itwWhere var)
+  return c { ctxWhere = M.insert (itwId var) (itwWhere var) (ctxWhere c) }
+
+-- | Check that identifiers in parents are distinct constants of a proper type and do not occur among ids
+checkParentInfo :: Context -> [Id] -> Type -> [Id] -> Checked ()
+checkParentInfo c ids t parents = if length parents /= length (nub parents)
+  then throwTypeError (ctxPos c) (text "Parent list contains duplicates:" <+> commaSep (map text parents))
+  else mapAccum_ checkParent parents
+  where
+    checkParent p = case M.lookup p (ctxConstants c) of
+      Nothing -> throwTypeError (ctxPos c) (text "Not in scope: constant" <+> text p)
+      Just t' -> if not (t <==> t')
+        then throwTypeError (ctxPos c) (text "Parent type" <+> doubleQuotes (typeDoc t') <+> text "is different from constant type" <+> doubleQuotes (typeDoc t))
+        else if p `elem` ids
+          then throwTypeError (ctxPos c) (text "Constant" <+> text p <+> text "is decalred to be its own parent")
+          else return ()    
+
+-- | Check that axiom is a valid boolean expression    
+checkAxiom :: Context -> Expression -> Checked ()
+checkAxiom c e = compareType c {ctxGlobals = M.empty } "axiom" BoolType e
+  
+-- | Check that function body is a valid expression of the same type as the function return type
+checkFunction :: Context -> Id -> [Id] -> [FArg] -> Expression -> Checked ()
+checkFunction c name tv args body = do 
+  functionScope <- foldAccum addFArg c { ctxTypeVars = tv } args
+  compareType functionScope { ctxGlobals = M.empty } "function body" retType body
+  where 
+    addFArg c (Just id, t) = checkIdType ctxIns ctxIns setIns c (id, t)
+    addFArg c  _ = return c
+    sig = funSig name c
+    retType = fsigRetType sig
+        
+-- | Check where-parts of procedure arguments and statements in its body
+checkProcedure :: Context -> [Id] -> [IdTypeWhere] -> [IdTypeWhere] -> [Contract] -> (Maybe Body) -> Checked ()
+checkProcedure c tv args rets specs mb = do 
+  cArgs <- foldAccum (checkIdType localScope ctxIns setIns) c { ctxTypeVars = tv } (map noWhere args)
+  _ <- foldAccum checkWhere cArgs args
+  mapAccum_ (compareType cArgs "precondition" BoolType . specExpr) (preconditions specs)
+  cRets <- foldAccum (checkIdType localScope ctxLocals setLocals) cArgs (map noWhere rets)
+  _ <- foldAccum checkWhere cRets rets
+  mapAccum_ (compareType cRets {ctxTwoState = True} "postcondition" BoolType . specExpr) (postconditions specs)
+  if not (null invalidModifies)
+    then throwTypeError (ctxPos c) (text "Identifier in a modifies clause does not denote a global variable:" <+> commaSep (map text invalidModifies))
+    else case mb of
+      Nothing -> return ()
+      Just body -> checkBody cRets { ctxModifies = modifies specs, ctxTwoState = True } body
+  where invalidModifies = modifies specs \\ M.keys (ctxGlobals c)
+  
+-- | Check procedure body  
+checkBody :: Context -> Body -> Checked ()
+checkBody c body = do
+  bodyScope <- foldAccum (checkIdType localScope ctxLocals setLocals) c (map noWhere (concat (fst body)))
+  _ <- foldAccum checkWhere bodyScope (concat (fst body))
+  bodyScope' <- collectLabels bodyScope (snd body)
+  checkBlock bodyScope' (snd body)
+
+-- | Check that implementation corresponds to a known procedure and matches its signature, then check all bodies
+checkImplementation :: Context -> Id -> [Id] -> [IdType] -> [IdType] -> [Body] -> Checked ()  
+checkImplementation c name tv args rets bodies = case M.lookup name (ctxProcedures c) of
+    Nothing -> throwTypeError (ctxPos c) (text "Not in scope: procedure" <+> text name)
+    Just sig -> case boundUnifier [] (psigTypeVars sig) (psigArgTypes sig ++ psigRetTypes sig) tv (argTypes ++ retTypes) of
+      Nothing -> throwTypeError (ctxPos c) (text "Could not match procedure signature" <+> 
+        doubleQuotes (sigDoc (psigArgTypes sig) (psigRetTypes sig)) <+>
+        text "against implementation signature" <+>
+        doubleQuotes (sigDoc argTypes retTypes) <+>
+        text "in the implementation of" <+> text name)
+      Just _ -> do
+        cArgs <- foldAccum (checkIdType localScope ctxIns setIns) c { ctxTypeVars = tv } args
+        cRets <- foldAccum (checkIdType localScope ctxLocals setLocals) cArgs rets
+        mapAccum_ (checkBody cRets { ctxModifies = (psigModifies sig), ctxTwoState = True }) bodies
+  where
+    argTypes = map (resolve c . snd) args
+    retTypes = map (resolve c . snd) rets        
+    
+{- Misc -}
+
+-- | 'compareType' @c msg t e@
+-- Check that @e@ is a valid expression in context @c@ and its type is @t@;
+-- in case of type error use @msg@ as a description for @e@
+-- (requires type synonyms in t be resolved)
+compareType :: Context -> String -> Type -> Expression -> Checked ()
+compareType c msg t e = do
+  t' <- checkExpression c e
+  if t <==> t' 
+    then return ()
+    else throwTypeError (ctxPos c) (text "Type of" <+> text msg <+> doubleQuotes (typeDoc t') <+> text "is different from" <+> doubleQuotes (typeDoc t))
+    
+-- 'checkLefts' @c ids n@ : 
+-- Check that there are @n@ @ids@, all @ids@ are unique and denote mutable variables
+checkLefts :: Context -> [Id] -> Int -> Checked ()
+checkLefts c vars n = if length vars /= n 
+  then throwTypeError (ctxPos c) (text "Expected" <+> int n <+> text "left-hand sides and got" <+> int (length vars))
+  else if vars /= nub vars
+    then throwTypeError (ctxPos c) (text "Variable occurs more than once among left-handes of a parallel assignment")
+    else if not (null immutableLhss)
+      then throwTypeError (ctxPos c) (text "Assignment to immutable variable(s):" <+> commaSep (map text immutableLhss))
+      else if not (null invalidGlobals)
+        then throwTypeError (ctxPos c) (text "Assignment to a global variable that is not in the enclosing procedure's modifies clause:" <+> commaSep (map text invalidGlobals))
+        else return ()      
+  where 
+    immutableLhss = vars \\ M.keys (mutableVars c)
+    invalidGlobals = (vars \\ M.keys (ctxLocals c)) \\ ctxModifies c
+  

@@ -0,0 +1,355 @@+-- | Various properties and transformations of Boogie program elements
+module Language.Boogie.Util ( 
+  -- * Types
+  TypeBinding,
+  typeSubst,
+  isFreeIn,
+  unifier,
+  oneSidedUnifier,
+  boundUnifier,
+  (<==>),
+  -- * Expressions
+  freeVarsTwoState,
+  freeVars,
+  freeOldVars,
+  VarBinding,
+  exprSubst,
+  paramSubst,
+  -- * Specs
+  preconditions,
+  postconditions,
+  modifies,
+  assumePreconditions,
+  -- * Funstions and procedures
+  FSig (..),
+  FDef (..),
+  PSig (..),
+  psigParams,
+  psigArgTypes,
+  psigRetTypes,
+  psigModifies,
+  psigRequires,
+  psigEnsures,
+  PDef (..),
+  -- * Code generation
+  num, eneg, enot,
+  (|+|), (|-|), (|*|), (|/|), (|%|), (|=|), (|!=|), (|<|), (|<=|), (|>|), (|>=|), (|&|), (|||), (|=>|), (|<=>|),
+  assume,
+  -- * Misc
+  interval,
+  fromRight,
+  mapFst,
+  mapSnd,
+  mapBoth,
+  changeState,
+  withLocalState
+) where
+
+import Language.Boogie.AST
+import Language.Boogie.Position
+import Language.Boogie.Tokens
+import Data.Maybe
+import Data.List
+import Data.Map (Map)
+import qualified Data.Map as M
+import Control.Applicative
+import Control.Monad.State
+
+{- Types -}
+
+-- | Mapping from type variables to types
+type TypeBinding = Map Id Type
+
+-- | '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
+typeSubst :: TypeBinding -> Type -> Type
+typeSubst _ BoolType = BoolType
+typeSubst _ IntType = IntType
+typeSubst binding (Instance id []) = case M.lookup id binding of
+  Just t -> t
+  Nothing -> Instance id []
+typeSubst binding (Instance id args) = Instance id (map (typeSubst binding) args)
+typeSubst binding (MapType bv domains range) = MapType bv (map (typeSubst removeBound) domains) (typeSubst removeBound range)
+  where removeBound = deleteAll bv binding
+  
+-- | 'fromTVNames' @tvs tvs'@ : type binding that replaces type variables @tvs@ with type variables @tvs'@
+fromTVNames :: [Id] -> [Id] -> TypeBinding
+fromTVNames tvs tvs' = M.fromList (zip tvs (map nullaryType tvs'))
+  
+-- | @x@ `isFreeIn` @t@ : does @x@ occur as a free type variable in @t@?
+-- @x@ must not be a name of a type constructor
+isFreeIn :: Id -> Type -> Bool
+x `isFreeIn` (Instance y []) = x == y
+x `isFreeIn` (Instance y args) = any (x `isFreeIn`) args
+x `isFreeIn` (MapType bv domains range) = x `notElem` bv && any (x `isFreeIn`) (range:domains)
+_ `isFreeIn` _ = False
+  
+-- | 'unifier' @fv xs ys@ : most general unifier of @xs@ and @ys@ with shared free type variables @fv@
+unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding
+unifier _ [] [] = Just M.empty
+unifier fv (IntType:xs) (IntType:ys) = unifier fv xs ys
+unifier fv (BoolType:xs) (BoolType:ys) = unifier fv xs ys
+unifier fv ((Instance id1 args1):xs) ((Instance id2 args2):ys) | id1 == id2 = unifier fv (args1 ++ xs) (args2 ++ ys)
+unifier fv ((Instance id []):xs) (y:ys) | id `elem` fv = 
+  if id `isFreeIn` y then Nothing 
+  else M.insert id y <$> unifier fv (update xs) (update ys)
+    where update = map (typeSubst (M.singleton id y))
+unifier fv (x:xs) ((Instance id []):ys) | id `elem` fv = 
+  if id `isFreeIn` x then Nothing 
+  else M.insert id x <$> unifier fv (update xs) (update ys)
+    where update = map (typeSubst (M.singleton id x))
+unifier fv ((MapType bv1 domains1 range1):xs) ((MapType bv2 domains2 range2):ys) =
+  case boundUnifier fv bv1 (range1:domains1) bv2 (range2:domains2) of
+    Nothing -> Nothing
+    Just u -> M.union u <$> (unifier fv (update u xs) (update u ys))
+  where
+    update u = map (typeSubst u)
+unifier _ _ _ = Nothing
+
+-- | 'removeClashesWith' @tvs tvs'@ :
+-- New names for type variables @tvs@ that are disjoint from @tvs'@
+-- (if @tvs@ does not have duplicates, then result also does not have duplicates)
+removeClashesWith :: [Id] -> [Id] -> [Id]
+removeClashesWith tvs tvs' = map freshName tvs
+  where
+    -- new name for tv that does not coincide with any tvs'
+    freshName tv = if tv `elem` tvs' then replicate (level + 1) nonIdChar ++ tv else tv
+    -- maximum number of nonIdChar characters at the beginning of a tvs'; by prepending (level + 1) nonIdChar charactes to tv we make is different from all tvs'
+    level = maximum [fromJust (findIndex (\c -> c /= nonIdChar) id) | id <- tvs']
+
+-- | '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@
+oneSidedUnifier :: [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding    
+oneSidedUnifier fv xs tv ys = M.map old <$> unifier fv xs (map new ys)
+  where
+    freshTV = tv `removeClashesWith` fv
+    new = typeSubst (fromTVNames tv freshTV)
+    old = typeSubst (fromTVNames freshTV tv)
+
+-- | '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
+boundUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
+boundUnifier fv bv1 xs bv2 ys = if length bv1 /= length bv2 || length xs /= length ys 
+  then Nothing
+  else case unifier (fv ++ bv1) xs (map withFreshBV ys) of
+    Nothing -> Nothing
+    Just u -> if all isFreshBV (M.elems (bound u)) && not (any hasFreshBV (M.elems (free u)))
+      then Just (free u)
+      else Nothing
+    where
+      freshBV = bv2 `removeClashesWith` bv1
+      withFreshBV = typeSubst (fromTVNames bv2 freshBV)
+      -- does a type correspond to one of the fresh bound variables of m2?
+      isFreshBV (Instance id []) = id `elem` freshBV
+      isFreshBV _ = False
+      -- does type t contain any fresh bound variables of m2?
+      hasFreshBV t = any (`isFreeIn` t) freshBV
+      -- binding restricted to free variables
+      free = deleteAll bv1
+      -- binding restricted to bound variables
+      bound = deleteAll (fv \\ bv1)
+      
+-- | Semantic equivalence on types
+-- (equality up to renaming of bound type variables)
+t1 <==> t2 = isJust (unifier [] [t1] [t2])       
+  
+{- Expressions -}
+
+-- | Free variables in an expression, referred to in current state and old state
+freeVarsTwoState :: Expression -> ([Id], [Id])
+freeVarsTwoState e = freeVarsTwoState' (node e)
+
+freeVarsTwoState' FF = ([], [])
+freeVarsTwoState' TT = ([], [])
+freeVarsTwoState' (Numeral _) = ([], [])
+freeVarsTwoState' (Var x) = ([x], [])
+freeVarsTwoState' (Application name args) = mapBoth (nub . concat) (unzip (map freeVarsTwoState args))
+freeVarsTwoState' (MapSelection m args) =  mapBoth (nub . concat) (unzip (map freeVarsTwoState (m : args)))
+freeVarsTwoState' (MapUpdate m args val) =  mapBoth (nub . concat) (unzip (map freeVarsTwoState (val : m : args)))
+freeVarsTwoState' (Old e) = let (state, old) = freeVarsTwoState e in ([], state ++ old)
+freeVarsTwoState' (IfExpr cond e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState cond, freeVarsTwoState e1, freeVarsTwoState e2])
+freeVarsTwoState' (Coercion e _) = freeVarsTwoState e
+freeVarsTwoState' (UnaryExpression _ e) = freeVarsTwoState e
+freeVarsTwoState' (BinaryExpression _ e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState e1, freeVarsTwoState e2])
+freeVarsTwoState' (Quantified _ _ boundVars e) = let (state, old) = freeVarsTwoState e in (state \\ map fst boundVars, old)
+
+-- | Free variables in an expression, in current state
+freeVars = fst . freeVarsTwoState
+-- | Free variables in an expression, in old state
+freeOldVars = snd . freeVarsTwoState
+
+-- | Mapping from variables to expressions
+type VarBinding = Map Id BareExpression
+
+-- | '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
+exprSubst :: VarBinding -> Expression -> Expression
+exprSubst binding (Pos pos e) = attachPos pos $ exprSubst' binding e
+
+exprSubst' binding (Var id) = case M.lookup id binding of
+  Nothing -> Var id
+  Just e -> e
+exprSubst' binding (Application id args) = Application id (map (exprSubst binding) args)
+exprSubst' binding (MapSelection m args) = MapSelection (exprSubst binding m) (map (exprSubst binding) args)
+exprSubst' binding (MapUpdate m args val) = MapUpdate (exprSubst binding m) (map (exprSubst binding) args) (exprSubst binding val)
+exprSubst' binding (Old e) = Old (exprSubst binding e)
+exprSubst' binding (IfExpr cond e1 e2) = IfExpr (exprSubst binding cond) (exprSubst binding e1) (exprSubst binding e2)
+exprSubst' binding (Coercion e t) = Coercion (exprSubst binding e) t
+exprSubst' binding (UnaryExpression op e) = UnaryExpression op (exprSubst binding e)
+exprSubst' binding (BinaryExpression op e1 e2) = BinaryExpression op (exprSubst binding e1) (exprSubst binding e2)
+exprSubst' binding (Quantified qop tv boundVars e) = Quantified qop tv boundVars (exprSubst binding' e)
+  where binding' = deleteAll (map fst boundVars) binding
+exprSubst' _ e = e
+
+-- | 'paramBinding' @sig def@ :
+-- Binding of parameter names from procedure signature @sig@ to their equivalents from procedure definition @def@
+paramBinding :: PSig -> PDef -> VarBinding
+paramBinding sig def = M.fromList $ zip (sigIns ++ sigOuts) (defIns ++ defOuts)
+  where
+    sigIns = map itwId $ psigArgs sig
+    sigOuts = map itwId $ psigRets sig
+    defIns = map Var $ pdefIns def
+    defOuts = map Var $ pdefOuts def
+  
+-- | 'paramSubst' @sig def@ :
+-- Substitute parameter names from @sig@ in an expression with their equivalents from @def@
+paramSubst :: PSig -> PDef -> Expression -> Expression  
+paramSubst sig def = if not (pdefParamsRenamed def) 
+  then id 
+  else exprSubst (paramBinding sig def)   
+
+{- Specs -}
+
+-- | 'preconditions' @specs@ : all precondition clauses in @specs@  
+preconditions :: [Contract] -> [SpecClause]
+preconditions specs = catMaybes (map extractPre specs)
+  where 
+    extractPre (Requires f e) = Just (SpecClause Precondition f e)
+    extractPre _ = Nothing
+
+-- | 'postconditions' @specs@ : all postcondition clauses in @specs@     
+postconditions :: [Contract] -> [SpecClause]
+postconditions specs = catMaybes (map extractPost specs)
+  where 
+    extractPost (Ensures f e) = Just (SpecClause Postcondition f e)
+    extractPost _ = Nothing
+   
+-- | 'modifies' @specs@ : all modifies clauses in @specs@   
+modifies :: [Contract] -> [Id]
+modifies specs = (nub . concat . catMaybes) (map extractMod specs)
+  where
+    extractMod (Modifies _ ids) = Just ids
+    extractMod _ = Nothing
+  
+-- | Make all preconditions in contracts free  
+assumePreconditions :: PSig -> PSig
+assumePreconditions sig = sig { psigContracts = map assumePrecondition (psigContracts sig) }
+  where
+    assumePrecondition (Requires _ e) = Requires True e
+    assumePrecondition c = c
+
+{- Functions and procedures -}
+
+-- | Function signature
+data FSig = FSig {
+    fsigName :: Id,         -- ^ Function name
+    fsigTypeVars :: [Id],   -- ^ Type variables
+    fsigArgTypes :: [Type], -- ^ Argument types
+    fsigRetType :: Type     -- ^ Return type
+  }
+  
+-- | Function definition
+data FDef = FDef {
+    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 
+  }
+ 
+-- | Procedure signature 
+data PSig = PSig {
+    psigName :: Id,               -- ^ Procedure name
+    psigTypeVars :: [Id],         -- ^ Type variables
+    psigArgs :: [IdTypeWhere],    -- ^ In-parameters
+    psigRets :: [IdTypeWhere],    -- ^ Out-parameters
+    psigContracts :: [Contract]   -- ^ Contracts
+  }
+  
+-- | All parameters of a procedure signature 
+psigParams sig = psigArgs sig ++ psigRets sig
+-- | Types of in-parameters of a procedure signature
+psigArgTypes = (map itwType) . psigArgs
+-- | Types of out-parameters of a procedure signature
+psigRetTypes = (map itwType) . psigRets
+-- | Modifies clauses of a procedure signature
+psigModifies = modifies . psigContracts
+-- | Preconditions of a procedure signature
+psigRequires = preconditions . psigContracts
+-- | Postconditions of a procedure signature
+psigEnsures = postconditions . psigContracts    
+  
+-- | Procedure definition;
+-- a single procedure might have multiple definitions (one per body)
+data PDef = PDef { 
+    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 i = gen $ Numeral i
+eneg e = inheritPos (UnaryExpression Neg) e
+enot e = inheritPos (UnaryExpression Not) e
+e1 |+|    e2 = inheritPos2 (BinaryExpression Plus) e1 e2
+e1 |-|    e2 = inheritPos2 (BinaryExpression Minus) e1 e2
+e1 |*|    e2 = inheritPos2 (BinaryExpression Times) e1 e2
+e1 |/|    e2 = inheritPos2 (BinaryExpression Div) e1 e2
+e1 |%|    e2 = inheritPos2 (BinaryExpression Mod) e1 e2
+e1 |=|    e2 = inheritPos2 (BinaryExpression Eq) e1 e2
+e1 |!=|   e2 = inheritPos2 (BinaryExpression Neq) e1 e2
+e1 |<|    e2 = inheritPos2 (BinaryExpression Ls) e1 e2
+e1 |<=|   e2 = inheritPos2 (BinaryExpression Leq) e1 e2
+e1 |>|    e2 = inheritPos2 (BinaryExpression Gt) e1 e2
+e1 |>=|   e2 = inheritPos2 (BinaryExpression Geq) e1 e2
+e1 |&|    e2 = inheritPos2 (BinaryExpression And) e1 e2
+e1 |||    e2 = inheritPos2 (BinaryExpression Or) e1 e2
+e1 |=>|   e2 = inheritPos2 (BinaryExpression Implies) e1 e2
+e1 |<=>|  e2 = inheritPos2 (BinaryExpression Equiv) e1 e2
+assume e = attachPos (position e) (Predicate (SpecClause Inline True e))
+  
+{- Misc -}
+
+-- | 'interval' @(lo, hi)@ : Interval from @lo@ to @hi@
+interval (lo, hi) = [lo..hi]
+
+-- | Extract the element out of a 'Right' and throw an error if its argument is 'Left'
+fromRight :: Either a b -> b
+fromRight (Right x) = x
+
+-- | 'deleteAll' @keys m@ : map @m@ with @keys@ removed from its domain
+deleteAll :: Ord k => [k] -> Map k a -> Map k a
+deleteAll keys m = foldr M.delete m keys
+
+mapFst f (x, y) = (f x, y)
+mapSnd f (x, y) = (x, f y)
+mapBoth f (x, y) = (f x, f y)
+
+-- | Execute a computation with state of type @t@ inside a computation with state of type @s@
+changeState :: (s -> t) -> (t -> s -> s) -> State t a -> State s a
+changeState getter modifier e = do
+  st <- gets getter
+  let (res, st') = runState e st
+  modify $ modifier st'
+  return res  
+
+-- | 'withLocalState' @localState e@ :
+-- Execute @e@ in current state modified by @localState@, and then restore current state
+withLocalState :: (s -> t) -> State t a -> State s a
+withLocalState localState e = changeState localState (flip const) e

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

@@ -0,0 +1,92 @@+module Main where
+
+import Language.Boogie.Parser
+import Language.Boogie.PrettyPrinter
+import Language.Boogie.TypeChecker
+import Language.Boogie.Interpreter
+import Data.Map (Map, (!))
+import qualified Data.Map as M
+import System.FilePath
+import Text.ParserCombinators.Parsec (parse, parseFromFile)
+import Test.HUnit
+
+main = runTestTT allTests
+
+allTests = TestList [parserTests, typeCheckerTests, interpreterTests]
+
+parserTests = TestLabel "Parser" $ TestList [
+  testCase parserSuccess "AttributeParsing"
+  ]
+
+typeCheckerTests = TestLabel "TypeChecker" $ TestList [
+  testCase (typeCheckerFailure 8)   "BadLabels",
+  testCase (typeCheckerFailure 4)   "Orderings",
+  testCase (typeCheckerFailure 2)   "WhereResolution",
+  testCase (typeCheckerFailure 35)  "Arrays",
+  testCase (typeCheckerFailure 15)  "Frame",
+  testCase (typeCheckerFailure 3)   "FunBody",
+  testCase (typeCheckerFailure 3)   "IfThenElse",
+  testCase (typeCheckerFailure 4)   "Lambda",
+  testCase (typeCheckerFailure 12)  "UpdateExprTyping",
+  testCase (typeCheckerFailure 1)   "TypeVarClash"
+  ]
+
+interpreterTests = TestLabel "Interpreter" $ TestList [
+  testCase interpreterSuccess "NoGuards",
+  testCase interpreterSuccess "EmptyDomains"
+  ]
+  
+-- | Directory with test programs  
+testDir = "tests"  
+-- | Entry point for test programs      
+entryPoint = "Test"        
+  
+testCase kind name = TestLabel name (TestCase $ kind (testDir </> name <.> "bpl")) 
+  
+-- | Test that parser fails on file  
+parserFailure file = do 
+  parseResult <- parseFromFile program file
+  case parseResult of
+    Left parseErr -> return ()
+    Right p -> assertFailure ("Undetected syntax error")  
+  
+-- | Test that parser succeeds on file, and re-parsing pretty printer code produces the same AST
+parserSuccess file = do 
+  parseResult <- parseFromFile program file
+  case parseResult of
+    Left parseErr -> assertFailure (show parseErr)
+    Right p -> case parse program ('*' : file) (show p) of
+      Left parseErr' -> assertFailure (show parseErr')
+      Right p' -> if p == p'
+        then return ()
+        else assertFailure "Re-parsing resulted in a different AST"
+  
+-- | Test that type checker reports n errors on file  
+typeCheckerFailure n file = do 
+  parseResult <- parseFromFile program file
+  case parseResult of
+    Left parseErr -> assertFailure (show parseErr)
+    Right p -> case checkProgram p of
+      Left typeErrs -> let m = length typeErrs in assertBool ("Expected " ++ show n ++ " type errors and got " ++ show m) (m == n)
+      Right context -> assertFailure ("Expected " ++ show n ++ " type errors and got 0")
+      
+-- | Test that type checker succeeds on file
+typeCheckerSuccess file = do 
+  parseResult <- parseFromFile program file
+  case parseResult of
+    Left parseErr -> assertFailure (show parseErr)
+    Right p -> case checkProgram p of
+      Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
+      Right context -> return ()
+      
+-- | Test that interpreter succeeds (no run-time failures or crashes) on procedure entryPoint in file      
+interpreterSuccess file = do 
+  parseResult <- parseFromFile program file
+  case parseResult of
+    Left parseErr -> assertFailure (show parseErr)
+    Right p -> case checkProgram p of
+      Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
+      Right context -> case executeProgram p context entryPoint of
+        Left err -> assertFailure (show err)
+        Right env -> return ()
+

@@ -0,0 +1,43 @@+name:                language-boogie
+version:             0.1
+synopsis:            Interpreter and language infrastructure for Boogie.
+description:         Boogaloo is an interpreter and run-time assertion checker for the Boogie intermediate verification language.
+                     The package also provides a language infrastructure library, including a Boogie AST, parser, type checker, and pretty-printer.
+homepage:            https://bitbucket.org/nadiapolikarpova/boogaloo
+license:             BSD3
+license-file:        LICENSE
+author:              Nadia Polikarpova
+maintainer:          nadia.polikarpova@gmail.com
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.8
+
+source-repository head
+  type:     hg
+  location: https://bitbucket.org/nadiapolikarpova/boogaloo
+
+flag boogaloo
+  Description: Build the boogaloo executable
+  Default:     True
+
+flag tests
+  Description: Build boogaloo-tests executable
+  Default:     False
+
+library
+  exposed-modules:     Language.Boogie.Util, Language.Boogie.TypeChecker, Language.Boogie.Tokens, Language.Boogie.Tester, Language.Boogie.PrettyPrinter, Language.Boogie.Position, Language.Boogie.Parser, Language.Boogie.Interpreter, Language.Boogie.BasicBlocks, Language.Boogie.AST, Language.Boogie.DataFlow, Language.Boogie.NormalForm, Language.Boogie.Intervals
+  -- other-modules:       
+  build-depends:       base ==4.5.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, containers ==0.4.*, mtl ==2.1.*, pretty ==1.1.*, parsec ==3.1.*, transformers ==0.3.*
+  
+executable boogaloo
+  main-is:             Boogaloo.hs             
+  build-depends:       base ==4.5.*, language-boogie ==0.1.*, containers ==0.4.*, parsec ==3.1.*, cmdargs ==0.10.*, random ==1.0.*, time ==1.4.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*  
+  If !flag(boogaloo)
+    buildable: False  
+  
+executable boogaloo-tests
+  main-is:             Tests.hs
+  build-depends:       base ==4.5.*, language-boogie ==0.1.*, containers ==0.4.*, filepath ==1.3.*, parsec ==3.1.*, HUnit ==1.2.*, mtl ==2.1.*, pretty ==1.1.*, transformers ==0.3.*    
+  If !flag(tests)
+    buildable: False  
+