improve-0.0.11: An imperative, verifiable programming language for high assurance applications.

Language.ImProve

Description

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_` a
case 1:                   [ (a ==. 1, do1)
do1();                , (a ==. 2, do2)
break;                , (true   , do3)
case 2:                   ]
do2();
break;
default:
do3();
}
```

Assertion Statements

```assert(condition);        `assert` condition
```

Statement Labels

```label: {                  "label" `|-` 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                     `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
}

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
```

Synopsis

# Types

data E a Source

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 Source

A mutable variable.

Instances

 Eq a => Eq (V a) PathName (V a)

class AllE a Source

Instances

 AllE Bool AllE Float AllE Int

class AllE a => NumE a Source

Instances

 NumE Float NumE Int

# Expressions

## Constants

True term.

False term.

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

Arbitrary constants.

## Variable Reference

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

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

## Logical Operations

Logical negation.

Logical AND.

Logical OR.

and_ :: [E Bool] -> E BoolSource

The conjunction of a E Bool list.

or_ :: [E Bool] -> E BoolSource

The disjunction of a E Bool list.

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

True iff the predicate is true for any element.

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

True iff the predicate is true for all elements.

Logical implication.

## Equality and Comparison

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

Equal.

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

Not equal.

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

Less than.

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

Less than or equal.

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

Greater than.

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

Greater than or equal.

## Min, Max, and Limiting

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

Returns the minimum of two numbers.

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

Returns the minimum of a list of numbers.

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

Returns the maximum of two numbers.

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

Returns the maximum of a list of numbers.

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

Limits between min and max.

## Arithmetic Operations

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

Multiplication.

Floating point division.

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

Integer division.

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

Modulo.

## Conditional Operator

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

Conditional expression.

``` mux test onTrue onFalse
```

## Lookups

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

Linear interpolation and extrapolation between two points.

# Statements

data Stmt a Source

The Stmt monad holds variable declarations and statements.

Instances

## Variable Hierarchical Scope and Statement Labeling

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

Creates a new hierarchical scope for variable names.

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

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 aSource

Creates a new hierarchical scope and labels a statement with the same name.

## Variable Declarations

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

Boolean variable declaration.

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

Boolean variable declaration and immediate assignment.

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

Int variable declaration.

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

Int variable declaration and immediate assignment.

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

Float variable declaration.

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

Float variable declaration and immediate assignment.

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

Input variable declaration. Input variables are initialized to 0.

## Variable Assignment

class Assign a whereSource

Methods

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

Instances

## Conditional Execution

Conditional if-else.

Conditional if without the else.

case_ :: [(E Bool, Stmt ())] -> Stmt ()Source

Condition case statement.

## Incrementing and decrementing.

Increments an E Int.

Decrements an E Int.

## Assertions and Assumptions

Assert that a condition is true.

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 a program.

^ verify pathToYices maxK program

# Code Generation

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

Generate C code.