diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -154,6 +154,7 @@
   , true
   , false
   , constant
+  , zero
   -- ** Variable Reference
   , ref
   -- ** Logical Operations
@@ -192,6 +193,8 @@
   -- ** Variable Hierarchical Scope and Statement Labeling 
   , (-|)
   -- ** Variable Declarations
+  , var
+  , var'
   , bool
   , bool'
   , int
@@ -386,14 +389,22 @@
   (_, path, _) <- get
   return path
 
+-- | Generic variable declaration.
 var :: AllE a => Name -> a -> Stmt (V a)
 var name init = do
   path <- getPath
   return $ V False (path ++ [name]) init
 
+-- | Generic variable declaration and immediate assignment.
+var' :: AllE a => Name -> E a -> Stmt (E a)
+var' name value = do
+  a <- var name zero
+  a <== value
+  return $ ref a
+
 -- | Input variable declaration.  Input variables are initialized to 0.
 input  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a
-input f path = ref $ V True path $ zero f
+input _ path = ref $ V True path zero
 
 -- | Global variable declaration.
 global  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a
@@ -458,11 +469,8 @@
 evalStmt :: Int -> [Name] -> Stmt () -> (Int, [Name], Statement)
 evalStmt id path (Stmt f) = snd $ f (id, path, Null)
 
-class Assign a where
-  (<==) :: V a -> E a -> Stmt ()
-instance Assign Bool  where a <== b = statement $ Assign a b
-instance Assign Int   where a <== b = statement $ Assign a b
-instance Assign Float where a <== b = statement $ Assign a b
+class Assign a where (<==) :: V a -> E a -> Stmt ()
+instance AllE a => Assign a where a <== b = statement $ Assign a b
 
 -- | Theorem to be proven or used as lemmas to assist proofs of other theorems.
 data Theorem = Theorem' Int
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -3,6 +3,7 @@
   , code
   ) where
 
+import Language.ImProve.Code.Ada
 import Language.ImProve.Code.C
 import Language.ImProve.Code.Modelica
 import Language.ImProve.Code.Simulink
@@ -10,7 +11,8 @@
 
 -- | Code generation targets.
 data Target
-  = C
+  = Ada
+  | C
   | Modelica
   | Simulink
   deriving Eq
@@ -20,6 +22,7 @@
 code target name stmt = f name stmt
   where
   f = case target of
+    Ada      -> codeAda
     C        -> codeC
     Modelica -> codeModelica
     Simulink -> codeSimulink
diff --git a/Language/ImProve/Code/Ada.hs b/Language/ImProve/Code/Ada.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code/Ada.hs
@@ -0,0 +1,140 @@
+module Language.ImProve.Code.Ada (codeAda) where
+
+import Control.Monad.State
+import Data.List
+import Text.Printf
+
+import Language.ImProve.Core
+import Language.ImProve.Tree hiding (Branch)
+import qualified Language.ImProve.Tree as T
+
+-- | Generate Ada.
+codeAda :: Name -> Statement -> IO ()
+codeAda name stmt = do
+  writeFile (name ++ ".ads") $ unlines
+    [ "-- Generated by ImProve."
+    , ""
+    , "package " ++ name ++ " is"
+    , ""
+    , indent $ unlines
+       [ codeVariables name scope
+       , name ++ "_Variables : " ++ name ++ "_Record0;"
+       , ""
+       , "procedure " ++ name ++ ";"
+       ]
+    , "end " ++ name ++ ";"
+    , ""
+    ]
+  writeFile (name ++ ".adb") $ unlines
+    [ "-- Generated by ImProve."
+    , ""
+    , "with Ada.Assertions;"
+    , ""
+    , "package body " ++ name ++ " is"
+    , ""
+    , indent $ unlines
+       [ "procedure " ++ name ++ " is"
+       , "   use Ada.Assertions;"
+       , "begin"
+       , indent $ codeStmt name [] stmt
+       , "end " ++ name ++ ";"
+       , ""
+       ]
+    , "end " ++ name ++ ";"
+    , ""
+    ]
+  where
+  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
+    [] -> error "program contains no useful statements"
+    a  -> T.Branch (name ++ "_variables") a
+
+instance Show Statement where show = codeStmt "none" []
+
+codeStmt :: Name -> [Name] -> Statement -> String
+codeStmt name path a = case a of
+  Assign a b -> name ++ "_Variables." ++ pathName a ++ " := " ++ codeExpr b ++ ";\n"
+  Branch a b Null -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "end if;\n"
+  Branch a b c    -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "\nelse\n" ++ indent (codeStmt name path c) ++ "end if;\n"
+  Sequence a b -> codeStmt name path a ++ codeStmt name path b
+  Theorem _ _ _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
+  Assume _ a      -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
+  Label name' a -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)
+  Null -> ""
+  where
+
+  codeExpr :: E a -> String
+  codeExpr a = case a of
+    Ref a     -> name ++ "_Variables." ++ pathName a
+    Const a   -> showConst $ const' a
+    Add a b   -> group [codeExpr a, "+", codeExpr b]
+    Sub a b   -> group [codeExpr a, "-", codeExpr b]
+    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]
+    Div a b   -> group [codeExpr a, "/", showConst (const' b)]
+    Mod a b   -> group [codeExpr a, "mod", showConst (const' b)]
+    Not a     -> group ["not", codeExpr a]
+    And a b   -> group [codeExpr a, "and",  codeExpr b]
+    Or  a b   -> group [codeExpr a, "or",  codeExpr b]
+    Eq  a b   -> group [codeExpr a, "=",  codeExpr b]
+    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]
+    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]
+    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]
+    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]
+    Mux a b c -> group ["if", codeExpr a, "then", codeExpr b, "else", codeExpr c] 
+    where
+    group :: [String] -> String
+    group a = "(" ++ intercalate " " a ++ ")"
+
+indent :: String -> String
+indent = unlines . map ("   " ++) . lines
+
+type Rec = State (Int, String)
+
+codeVariables :: Name -> Tree Name (Bool, Path, Const) -> String
+codeVariables name a = indent s
+  where
+  (_, s) = execState (typ a) (0, "")
+  typ :: Tree Name (Bool, Path, Const) -> Rec String
+  typ a = case a of
+    T.Branch _ items -> do
+      i <- nextId
+      fields <- mapM field items
+      let typeName = printf "%s_Record%d" name i
+      appendCode $ unlines
+        [ printf "type %s is" typeName
+        , indent $ unlines
+          [ "record"
+          , indent $ unlines $ fields
+          , "end record;"
+          ]
+        ]
+      return typeName
+    Leaf _ (_, _, init) -> return $ printf "%s := %s" (showConstType init) (showConst init)
+
+  field :: Tree Name (Bool, Path, Const) -> Rec String
+  field a = do
+    t <- typ a
+    case a of
+      T.Branch name _         -> return $ printf "%-30s : %s;"   name t
+      Leaf name (input, _, _) -> return $ printf "%-30s : %s;%s" name t (if input then "  -- input" else "")
+
+  nextId :: Rec Int
+  nextId = do
+    (i, s) <- get
+    put (i + 1, s)
+    return i
+  
+  appendCode :: String -> Rec ()
+  appendCode s = modify $ \ (i, s') -> (i, s' ++ s)
+
+showConst :: Const -> String
+showConst a = case a of
+  Bool  a  -> show a
+  Int   a  -> show a
+  Float a  -> show a
+
+showConstType :: Const -> String
+showConstType a = case a of
+  Bool  _ -> "Boolean"
+  Int   _ -> "Integer range -2147483648 .. 2147483647"
+  Float _ -> "Float"
+
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -48,19 +48,19 @@
 instance PathName VarInfo where pathName (_, path, _) = pathName path
 
 class Eq a => AllE a where
-  zero   :: (Name -> a -> m (V a)) -> a
+  zero   :: a
   const' :: a -> Const
 
 instance AllE Bool where
-  zero = const False
+  zero = False
   const' = Bool
 
 instance AllE Int where
-  zero = const 0
+  zero = 0
   const' = Int
   
 instance AllE Float where
-  zero = const 0
+  zero = 0
   const' = Float
 
 class    AllE a => NumE a
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
deleted file mode 100644
--- a/Language/ImProve/Examples.hs
+++ /dev/null
@@ -1,198 +0,0 @@
--- | ImProve examples.
-module Language.ImProve.Examples
-  ( buildGCD
-  , counter
-  , verifyCounter
-  , arbiterSpec
-  , arbiter
-  , arbiter1
-  , arbiter2
-  , arbiter3
-  , verifyArbiters
-  , buildArbiters
-  , runAll
-  ) where
-
-import Language.ImProve
-
--- | Computes the greatest common divison of two integers.
---   Returns true if the computation is done, and the result.
-gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)
-gcd' a b = do
-  a0 <- int "a0" 0  -- Copy of input 'a'.
-  b0 <- int "b0" 0  -- Copy of input 'b'.
-  a1 <- int "a1" 0  -- Working copy of 'a'.
-  b1 <- int "b1" 0  -- Working copy of 'b'.
-
-  -- A new input to process.
-  "startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do
-    a0 <== a
-    b0 <== b
-    a1 <== a
-    b1 <== b
-
-  -- Reduce a1.
-  "reduceA" -| if_ (ref a1 >. ref b1) $ do
-    a1 <== ref a1 - ref b1
-
-  -- Reduce b1.
-  "reduceB" -| if_ (ref b1 >. ref a1) $ do
-    b1 <== ref b1 - ref a1
-
-  -- Done if a1 == b1.
-  return (ref a1 ==. ref b1, ref a1)
-
-
--- | A top level wrapper for gcd'.
-gcdMain :: Stmt ()
-gcdMain = do
-  let a = input int ["a"]  -- Input variable 'a'.
-      b = input int ["b"]  -- Input variable 'b'.
-  done   <- bool "done"   False  -- Variable signalling completion.
-  result <- int  "result" 0      -- Result of GCD.
-
-  -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)
-  (done', result') <- "gcd" -| gcd' a b
-
-  -- Bind the results to the output variables.
-  done   <== done'
-  result <== result'
-
--- | Build the gcdMain code (i.e. gcd.c, gcd.h).
-buildGCD :: IO ()
-buildGCD = code C "gcd" gcdMain
-
-
-
--- | A rolling counter verification example.
-counter :: Stmt ()
-counter = do
-  -- The counter variable.
-  counter <- int "counter" 0
-
-  -- Specification.
-  theorem "GreaterThanOrEqualTo0" 1 [] $ ref counter >=. 0
-  theorem "LessThan10"            1 [] $ ref counter <=. 9
-
-  -- Implementation.
-  ifelse (ref counter ==. 9) (counter <== 0) (counter <== ref counter + 1)
-
--- | Verify the 'counter' example.
-verifyCounter :: IO ()
-verifyCounter = verify "yices" counter
-
-
-
--- | Arbiter specification.
-arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
-arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
-
-  -- Mutual exclusion.  At most, only one requester granted at a time.
-  theorem "OneHot" 1 [] $      grantA &&. not_ grantB &&. not_ grantC
-                      ||. not_ grantA &&.      grantB &&. not_ grantC
-                      ||. not_ grantA &&. not_ grantB &&.      grantC
-                      ||. not_ grantA &&. not_ grantB &&. not_ grantC
-  
-  -- No grants without requests.
-  theorem "NotRequestedA" 1 [] $ not_ requestA --> not_ grantA
-  theorem "NotRequestedB" 1 [] $ not_ requestB --> not_ grantB
-  theorem "NotRequestedC" 1 [] $ not_ requestC --> not_ grantC
-
-  -- Grants to single requests.
-  theorem "OnlyRequestA" 1 [] $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA
-  theorem "OnlyRequestB" 1 [] $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB
-  theorem "OnlyRequestC" 1 [] $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC
-
-  -- Priority.
-  theorem "Highest" 1 [] $ requestA --> grantA
-  theorem "Medium"  1 [] $ (not_ requestA &&. requestB) --> grantB
-  theorem "Lowest"  1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
-
-  return ()
-
--- | An arbiter implementation.
-arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter1 (requestA, requestB, requestC) = do
-  let grantA = requestA
-      grantB = requestB
-      grantC = requestC
-  return (grantA, grantB, grantC)
-
--- | An another arbiter implementation.
-arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter2 (requestA, requestB, requestC) = do
-  grantA <- bool "grantA" False
-  grantB <- bool "grantB" False
-  grantC <- bool "grantC" False
-
-  "GrantA" -| if_ (requestA)                                     (grantA <== true)
-  "GrantB" -| if_ (not_ requestA &&. requestB)                   (grantB <== true)
-  "GrantC" -| if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
-
-  return (ref grantA, ref grantB, ref grantC)
-
--- | Yet another arbiter implementation.
-arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
-arbiter3 (requestA, requestB, requestC) = do
-  let grantA = requestA
-      grantB = not_ requestA &&. requestB
-      grantC = not_ requestA &&. not_ requestB &&. requestC
-  return (grantA, grantB, grantC)
-
--- | Binding an arbiter implemenation to the arbiter specification.
-arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
-arbiter name implementation = name -| do
-  -- Create input variables.
-  let requestA = input bool ["requestA"]
-      requestB = input bool ["requestB"]
-      requestC = input bool ["requestC"]
-  let requests = (requestA, requestB, requestC)
-
-  -- Instantiate implementation.
-  grants@(grantA, grantB, grantC) <- "impl" -| implementation requests
-
-  -- Bind specification.
-  arbiterSpec requests grants
-
-  -- Create output variables.
-  bool' "grantA" grantA
-  bool' "grantB" grantB
-  bool' "grantC" grantC
-  return ()
-
--- | Verify the different arbiter implementations.
-verifyArbiters :: IO ()
-verifyArbiters = do
-  putStrLn "\nVerifying arbiter1 ..."
-  verify "yices" $ arbiter "arbiter1" arbiter1
-
-  putStrLn "\nVerifying arbiter2 ..."
-  verify "yices" $ arbiter "arbiter2" arbiter2
-
-  putStrLn "\nVerifying arbiter2 ..."
-  verify "yices" $ arbiter "arbiter3" arbiter3
-
--- | Build the different arbiter implementations.
-buildArbiters :: IO ()
-buildArbiters = do
-  putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."
-  code C "arbiter1" $ arbiter "arbiter1" arbiter1
-
-  putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."
-  code C "arbiter2" $ arbiter "arbiter2" arbiter2
-
-  putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."
-  code C "arbiter3" $ arbiter "arbiter3" arbiter3
-
--- | Run all examples.
-runAll :: IO ()
-runAll = do
-  putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."
-  buildGCD
-  putStrLn "\nVerifying counter ..."
-  verifyCounter
-  putStrLn "\nVerifying arbiters ..."
-  verifyArbiters
-  putStrLn "\nBuilding arbiters ..."
-  buildArbiters
-
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.3.3
+version: 0.3.4
 
 category: Language, Formal Methods, Embedded
 
@@ -9,7 +9,7 @@
   ImProve is an imperative programming language for high assurance applications.
   ImProve uses infinite state, unbounded model checking to verify programs adhere
   to specifications.  Yices (required) is the backend SMT solver.
-  ImProve compiles to C, Simulink, and Modelica.
+  ImProve compiles to C, Ada, Simulink, and Modelica.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>
@@ -31,17 +31,17 @@
     exposed-modules:
         Language.ImProve
         Language.ImProve.Code
+        Language.ImProve.Code.Ada
         Language.ImProve.Code.C
         Language.ImProve.Code.Common
         Language.ImProve.Code.Modelica
         Language.ImProve.Code.Simulink
         Language.ImProve.Core
-        Language.ImProve.Examples
         Language.ImProve.Path
         Language.ImProve.Tree
         Language.ImProve.Verify
 
-    extensions: GADTs, FlexibleInstances, TypeSynonymInstances
+    extensions: GADTs, FlexibleInstances, TypeSynonymInstances, UndecidableInstances
 
     ghc-options: -W