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();
}

switch (a) {              case_ $ do
    case 1:                   a ==. 1 ==> do1
        do1();                a ==. 2 ==> do2
        break;                true    ==> do3
    case 2:
        do2();
        break;
    default:
        do3();
}

Assertion Statements

assert(condition);        theorem name k lemmas condition

Statement Labels

label: {                  "label" -| do
    a();                      a
    b();                      b
}

Expressions

Constant Literals

true                      true
false                     false
0                         0
100                       100
1.0                       1
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                     div_ a b   -- int
a % b                     mod_ a 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, which are inlined at code generation.)

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 Eq a => AllE a where

Methods

zero :: a

Instances

AllE Bool

AllE Float

AllE Int

class AllE a => NumE a

Instances

NumE Float

NumE Int

type Name = String

data Theorem

Theorem to be proven or used as lemmas to assist proofs of other theorems.

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

Logical implication.

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 of two points.

Statements

data Stmt a

The Stmt monad holds variable declarations and statements.

Instances

Monad Stmt

Variable Hierarchical Scope and Statement Labeling

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

Labels a statement and creates a new variable scope. Labels are used in counter examples to help trace the program execution.

Variable Declarations

var :: AllE a => Name -> a -> Stmt (V a)

Generic variable declaration.

var' :: AllE a => Name -> E a -> Stmt (E a)

Generic variable declaration and immediate assignment.

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)) -> Path -> E a

Input variable declaration. Input variables are initialized to 0.

global :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a

Global variable declaration.

Variable Assignment

class Assign a where

Methods

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

Instances

AllE a => Assign a

Conditional Execution

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

Conditional if-else.

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

Conditional if without the else.

case_ :: Case () -> Stmt ()

Condition case statement.

(==>) :: E Bool -> Stmt () -> Case ()

Incrementing and decrementing.

incr :: V Int -> Stmt ()

Increments an E Int.

decr :: V Int -> Stmt ()

Decrements an E Int.

Assumptions and theorems.

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

Assume a condition is true. Assumptions are used as lemmas to other theorems.

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

Defines a new theorem.

 theorem name k lemmas proposition

Verification

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

Verify a program.

 verify pathToYices program

Code Generation

data Target

Code generation targets.

Constructors

Ada

C

Modelica

Simulink

Instances

Eq Target

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

Generate code.

General Analysis

analyze :: (Statement -> IO a) -> Stmt () -> IO a

Generic program analysis.