Language Overview

ImProve Home

Types

ImProve is domain specific language (DSL) embedded in Haskell and makes use of Haskell's elegant type system to manage ImProve data types. First off, all ImProve programs are defined inside the Stmt monad:

someImProveFunction :: Stmt ()
someImProveFunction = ...

The Stmt monad captures program statements, such as IF statements and variable assignments, as well as local variable declarations.

ImProve has three primitive types:

booleans
ints
floats

To share operators across ImProve types, two type classes are defined. 'AllE' encompasses all primitive types, while 'NumE' contains just ints and floats:

class Eq a => AllE a
instance AllE Bool
instance AllE Int
instance AllE Float

class AllE a => NumE a
instance NumE Int
instance NumE Float

To distinguish between these types and Haskell types, ImProve uses parametric types 'V' for variables and 'E' for expressions. For example:

-- Airspeed is an input and an immutable expression.
airspeed :: E Float
airspeed = input float ["adc", "airspeed"]

-- A integer counter intended to be modified by the program.
counter :: V Int
counter = global int ["outputs", "counter"] 0

ImProve purposely distinguishes between mutable variables (V types) from immutable expressions (E types). This provides added safety by allowing the programmer to specify things that can be modified (variables) from things that shall not (expressions). Using these Haskell parametric types, along with Haskell GADTs, the Haskell type checker is able to verify type correctness of the resulting ImProve program -- even before the ImProve compiler starts running!

Variable Declarations

There are two methods for declaring variables: either global or local. A global variable declaration (introduced with the keyword 'global') provides its full hierarchical, whereas a local variable declaration only provides its local name. For this reason, local variables must be declared within the Stmt monad. Global variables may be declared anywhere. Some examples:

someStmt :: Stmt ()
someStmt = do
  a    <- int  "a"    22    -- Declares a local variable 'a' with an initial value of 22.
  flag <- bool "flag" False -- Declares a local boolean variable 'flag' with an initial value of False.
  ...

-- A global variable with an initial value of 0.
engineSpeedCommand :: V Float
engineSpeedCommand = global float ["ouputs", "engine_commands", "speed"] 0

Local Variable Instantiation

A local variable declaration always creates a new variable whose state persists across the execution of the encompassing ImProve function. Though similar to a C static variable, the semantics are different. For example, compare the following C and ImProve functions:

int incrementCounter()
{
        static int counter = 0;
        counter = counter + 1;
        return counter;
}

incrementCounter :: Name -> Stmt (E Int)
incrementCounter name = do
  counter <- int name 0
  counter <== ref counter + 1
  return $ ref counter

For C, the counter variable is static, and thus will retain is value between calls to incrementCounter. Also, there is only one counter variable, which is shared with all applications of incrementCounter.

The ImProve version of incrementCounter also creates a counter variable. Like the C version, the variable retains its state. However unlike C, a new instance of the variable is created for every call to incrementCounter. This is because all ImProve functions are elaborated at compile time -- ImProve has no notion of subroutines (functions, procedures). ImProve's so called functions are nothing more than Haskell functions that perform macro expansion.

Expressions

Constants

Boolean constants:

true  :: E Bool
false :: E Bool

Numeric E types are members of common Haskell numeric classes, so numeric E constants can be created just like Haskell constants:

three :: E Int
three = 3

pi :: E Float
pi = 3.14

To convert arbitrary Haskell values to ImProve constants, use the 'constant' function:

constant :: AllE a => a -> E a

haskellOne :: Int
haskellOne = 1

improveOne ::E Int
improveOne = constant haskellOne

Variable References

To use variables in compound expressions requires that V types be cast to E types. This is the purpose of the 'ref' function:

ref :: AllE a => V a -> E a

For example:

someStmt :: Stmt ()
someStmt = do
  counter <- int "counter" 0
  counter <== ref counter + 1  -- Increment the counter by 1.  Note the assignment operator (<==).

'ref' is not just for putting variables into expressions. It is also a useful defensive coding mechanism. Say for instance a function needs the value of a counter, but it should not have permission to modify the counter. Simply 'ref' the counter and pass the immutable E type to the function:

someFunction :: E Int -> Stmt ()
someFunction counter = do
  ...

top :: Stmt ()
top = do
  counter <- int "counter" 0
  someFunction (ref counter)  -- Provides an immutable reference of counter value to 'someFunction'.

Logical Expressions

The basic AND, OR, and NOT operators:

not_  :: E Bool -> E Bool
(&&.) :: E Bool -> E Bool -> E Bool
(||.) :: E Bool -> E Bool -> E Bool

not_ a &&. (b ||. c)

ImProve also provides a implication operator, which is defined as follows:

(-->) :: E Bool -> E Bool -> E Bool
a --> b = not_ a ||. b

Haskell various logical utilities (and, or, any, all) have equivalent ImProve versions:

and_ :: [E Bool] -> E Bool
or_  :: [E Bool] -> E Bool
any_ :: (a -> E Bool) -> [a] -> E Bool
all_ :: (a -> E Bool) -> [a] -> E Bool

Equality and Comparison Expressions

Equality and comparison operators:

(==.) :: AllE a => E a -> E a -> E Bool
(/=.) :: AllE a => E a -> E a -> E Bool
(<.)  :: NumE a => E a -> E a -> E Bool
(<=.) :: NumE a => E a -> E a -> E Bool
(>.)  :: NumE a => E a -> E a -> E Bool
(>=.) :: NumE a => E a -> E a -> E Bool

(a ==. b) ||. (a >. 22)

ImProve also has functions akin to Haskell's 'min', 'max', 'minimum', and 'maximum':

min_     :: NumE a => E a -> E a -> E a
minimum_ :: NumE a => [E a] -> E a
max_     :: NumE a => E a -> E a -> E a
maximum_ :: NumE a => [E a] -> E a

Statements

ImProve has three basic types of statements:

Variable Assignment Statements
Conditional Statements (if, case)
Verification Directives (theorems, assumptions)

Variable Assignments

Variable assignments use the assignment operator:

counter <== ref counter + 1
flag    <== not_ $ ref flag
three   <== 1 + 2

Conditional Statements

ImProve provides two types of IF statements for when an ELSE clause is provided or not:

ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
if_    :: E Bool -> Stmt () -> Stmt ()

-- With an ELSE clause.
ifelse resetCounter
  (do
    counter <== 0
    flag    <== false)
  (do
    counter <== ref counter + 1
    flag    <== true)

-- Without an ELSE clause.
if_ faultActive
  (do
    engageCommand <== false)

Using some Haskell monadic tricks, ImProve provides a CASE (switch) statement:

case_ $ do
  ref state ==. 1 ==> do
    state   <== 2
    flag    <== false

  ref state ==. 2 ==> do
    state   <== 3
    counter <== 0

  ref state ==. 3 &&. ref counter <. 20 ==> do
    counter <== counter + 1
    flag <== true

  ref state ==. 3 ==>
    state <== 1

  true ==> do  -- default
    state <== 1

Verification Directives

ImProve verification is based on program assertions called 'theorems'. ImProve theorems follows the basic semantics of C assertions: every time the assertion (theorem) statement is executed, the associated boolean expression must be true. In addition to the boolean expression, ImProve theorems also require an identifying name, a search depth (k value), and a list of lemmas (previously proven theorems to aid verification):

theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem

someStmt :: Stmt ()
someStmt = do
  ...
  theorem "a_must_be_equal_to_b" 1 [] $ a ==. b
  ...

Sometimes theorem verification depends on assumptions of external software, i.e. the behavior of the inputs. ImProve handles this with the 'assume' function, which produces a lemma to feed other theorems. For example:

assume :: Name -> E Bool -> Stmt Theorem

a = input int ["inputs", "a"]
b = input int ["inputs", "b"]

someStmt :: Stmt ()
someStmt = do
  assume1 <- assume "a_greater_than_b" $ a >. b
  ...
  theorem "something" 1 [assume1] $ something_that_depends_on_a_gt_b
  ...

Unlike theorems, assumptions are not verified with ImProve. However in code generation, assumptions are asserted just like theorems, since the assumptions may be invalid and potentially could be caught in higher level testing or analysis.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly