verifyPostConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)
verifyPreConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)
addPreConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)