Language.ImProve

ImProve is an imperative programming language for high assurance applications.

ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications, which are written in the form of assertion statements. If it is unable to verify an assertion, ImProve will emit a counter example that shows a precise program trace that exercises the assertion violation.

The following compares the syntax of C and ImProve:

Variable Declarations

float a = 0.0;            a <- float "a" 0
bool b = true;            b <- bool "b" true
int c = d + e + 3;        c <- int' "c" (d + e + 3)

Variable Assignments

a = 1;                    a <== 1

Conditional Statements

if (condition) {          if_ condition $ do 
    a();                      a
    b();                      b
    c();                      c
}

if (condition {           ifelse condition
    a();                      (do a
    b();                          b
    c();                          c)
}                             (do d
else {                            e 
    d();                          f)
    e();
    f();
}                                 

Assertion Statements

assert(condition);        assert condition

Statement Labels

hello: {                  "hello" -: do
    a();                      a
    b();                      b
}

Expressions

Constant Literals

true                      true
false                     false
0                         0
100                       100
1.0                       1     -- float
3.14                      3.14

Variable Reference

a                         ref a

Logical Expressions

! a                       not_ a
a && b                    a &&. b
a || b                    a ||. b

Comparison Expressions

a == b                    a ==. b
a != b                    a /=. b
a < b                     a <. b
a > b                     a >. b
a <= b                    a <=. b
a >= b                    a >=. b

Arithmetic Expressions

a + b                     a + b
a * b                     a *. b
a / b                     a /. b     -- float
a / b                     a 'div_' b -- int
a % b                     a 'mod_' b
abs(a)                    abs a
min(a, b)                 min_ a b
max(a, b)                 max_ a b

Conditional Expression

a ? b : c                 mux a b c

Function Definitions and Function Calls (All ImProve functions are Haskell functions that are inlined at compile time.)

int add(int a, int b) {                             add :: E Int -> E Int -> E Int
  return a + b;                                     add a b = a + b
}

three = add(1, 2);                                  three <== add 1 2

void incrCounter(int *counter, int amount) {        incrCounter :: V Int -> E Int -> Stmt ()
  *counter = *counter + amount;                     incrCounter counter amount = counter <== ref counter + amount
}

incrCounter(&counter, 22);                          incrCounter counter 22

Types

data E a

A logical, arithmetic, comparative, or conditional expression.

Instances

Eq (E a)

Fractional (E Float)

(Num a, AllE a, NumE a) => Num (E a)

Show (E a)

data V a

A mutable variable.

Instances

Eq a => Eq (V a)

PathName (V a)

class AllE a

Instances

AllE Bool

AllE Float

AllE Int

class AllE a => NumE a

Instances

NumE Float

NumE Int

type Name = String

Expressions

Constants

true :: E Bool

True term.

false :: E Bool

False term.

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

Arbitrary constants.

Variable Reference

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

References a variable to be used in an expression (E).

Logical Operations

not_ :: E Bool -> E Bool

Logical negation.

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

Logical AND.

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

Logical OR.

and_ :: [E Bool] -> E Bool

The conjunction of a E Bool list.

or_ :: [E Bool] -> E Bool

The disjunction of a E Bool list.

any_ :: (a -> E Bool) -> [a] -> E Bool

True iff the predicate is true for any element.

all_ :: (a -> E Bool) -> [a] -> E Bool

True iff the predicate is true for all elements.

(-->) :: E Bool -> E Bool -> E Bool

Equality and Comparison

(==.) :: AllE a => E a -> E a -> E Bool

Equal.

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

Not equal.

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

Less than.

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

Less than or equal.

(>.) :: NumE a => E a -> E a -> E Bool

Greater than.

(>=.) :: NumE a => E a -> E a -> E Bool

Greater than or equal.

Min, Max, and Limiting

min_ :: NumE a => E a -> E a -> E a

Returns the minimum of two numbers.

minimum_ :: NumE a => [E a] -> E a

Returns the minimum of a list of numbers.

max_ :: NumE a => E a -> E a -> E a

Returns the maximum of two numbers.

maximum_ :: NumE a => [E a] -> E a

Returns the maximum of a list of numbers.

limit :: NumE a => E a -> E a -> E a -> E a

Limits between min and max.

Arithmetic Operations

(*.) :: NumE a => E a -> a -> E a

Multiplication.

(/.) :: E Float -> Float -> E Float

Floating point division.

div_ :: E Int -> Int -> E Int

Integer division.

mod_ :: E Int -> Int -> E Int

Modulo.

Conditional Operator

mux :: AllE a => E Bool -> E a -> E a -> E a

Conditional expression.

 mux test onTrue onFalse

Lookups

linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float

Linear interpolation and extrapolation between two points.

Statements

data Stmt a

The Stmt monad holds variable declarations and statements.

Instances

Monad Stmt

Statement Labeling and Hierarchical Scope

(-:) :: Name -> Stmt a -> Stmt a

Labels a statement. Labels are used in counter examples to trace the program execution. And assertion names, and hence counter example trace file names, are produce from labels.

(!) :: Name -> Stmt a -> Stmt a

Creates a new hierarcical scope for variable names.

Variable Declarations

bool :: Name -> Bool -> Stmt (V Bool)

Boolean variable declaration.

bool' :: Name -> E Bool -> Stmt (E Bool)

Boolean variable declaration and immediate assignment.

int :: Name -> Int -> Stmt (V Int)

Int variable declaration.

int' :: Name -> E Int -> Stmt (E Int)

Int variable declaration and immediate assignment.

float :: Name -> Float -> Stmt (V Float)

Float variable declaration.

float' :: Name -> E Float -> Stmt (E Float)

Float variable declaration and immediate assignment.

input :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)

Input variable declaration. Input variables are initialized to 0.

Variable Assignment

class Assign a where

Methods

(<==) :: V a -> E a -> Stmt ()

Instances

Assign Bool

Assign Float

Assign Int

Conditional Execution

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

Conditional if-else.

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

Conditional if without the else.

Incrementing and decrementing.

incr :: V Int -> Stmt ()

Increments an E Int.

decr :: V Int -> Stmt ()

Decrements an E Int.

Assertions and Assumptions

assert :: E Bool -> Stmt ()

Assert that a condition is true.

assume :: E Bool -> Stmt ()

Declare an assumption condition is true. Assumptions expressions must contain variables directly or indirectly related to the assertion under verification, otherwise they will be ignored.

Verification

verify :: FilePath -> Int -> Stmt () -> IO ()

Verify a program.

^ verify pathToYices maxK program

Code Generation

code :: Name -> Stmt () -> IO ()

Generate C code.