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); assert
name k condition
Statement Labels
label: { "label" -|
do
a(); a
b(); b
}
Expressions
Constant Literals truetrue
falsefalse
0 0 100 100 1.0 1 3.14 3.14 Variable Reference aref
a Logical Expressions ! anot_
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 / bdiv_
a b -- int a % bmod_
a b abs(a)abs
a min(a, b)min_
a b max(a, b)max_
a b Conditional Expression a ? b : cmux
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
- data E a
- data V a
- class Eq a => AllE a where
- zero :: a
- class AllE a => NumE a
- type Name = String
- true :: E Bool
- false :: E Bool
- constant :: AllE a => a -> E a
- ref :: AllE a => V a -> E a
- not_ :: E Bool -> E Bool
- (&&.) :: E Bool -> E Bool -> E Bool
- (||.) :: E Bool -> E Bool -> E Bool
- and_ :: [E Bool] -> E Bool
- or_ :: [E Bool] -> E Bool
- any_ :: (a -> E Bool) -> [a] -> E Bool
- all_ :: (a -> E Bool) -> [a] -> E Bool
- (-->) :: E Bool -> E Bool -> E Bool
- (==.) :: 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
- 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
- limit :: NumE a => E a -> E a -> E a -> E a
- (*.) :: NumE a => E a -> a -> E a
- (/.) :: E Float -> Float -> E Float
- div_ :: E Int -> Int -> E Int
- mod_ :: E Int -> Int -> E Int
- mux :: AllE a => E Bool -> E a -> E a -> E a
- linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float
- data Stmt a
- (-|) :: Name -> Stmt a -> Stmt a
- var :: AllE a => Name -> a -> Stmt (V a)
- var' :: AllE a => Name -> E a -> Stmt (E a)
- bool :: Name -> Bool -> Stmt (V Bool)
- bool' :: Name -> E Bool -> Stmt (E Bool)
- int :: Name -> Int -> Stmt (V Int)
- int' :: Name -> E Int -> Stmt (E Int)
- float :: Name -> Float -> Stmt (V Float)
- float' :: Name -> E Float -> Stmt (E Float)
- input :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a
- global :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a
- class Assign a where
- ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
- if_ :: E Bool -> Stmt () -> Stmt ()
- case_ :: Case () -> Stmt ()
- (==>) :: E Bool -> Stmt () -> Case ()
- incr :: V Int -> Stmt ()
- decr :: V Int -> Stmt ()
- assume :: Name -> E Bool -> Stmt ()
- assert :: Name -> Int -> E Bool -> Stmt ()
- verify :: FilePath -> Stmt () -> IO ()
- data Target
- code :: Target -> Name -> Stmt () -> IO ()
- analyze :: (Statement -> IO a) -> Stmt () -> IO a
Types
A logical, arithmetic, comparative, or conditional expression.
Expressions
Constants
Variable Reference
Logical Operations
Equality and Comparison
Min, Max, and Limiting
Arithmetic Operations
Conditional Operator
Lookups
linear :: (Float, Float) -> (Float, Float) -> E Float -> E FloatSource
Linear interpolation and extrapolation of two points.
Statements
Variable Hierarchical Scope and Statement Labeling
(-|) :: Name -> Stmt a -> Stmt aSource
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 -> E a -> Stmt (E a)Source
Generic variable declaration and immediate assignment.
bool' :: Name -> E Bool -> Stmt (E Bool)Source
Boolean variable declaration and immediate assignment.
float' :: Name -> E Float -> Stmt (E Float)Source
Float variable declaration and immediate assignment.
input :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E aSource
Input variable declaration. Input variables are initialized to 0.
Variable Assignment
Conditional Execution
Incrementing and decrementing.
Assumptions and assertions.
assume :: Name -> E Bool -> Stmt ()Source
Assume a condition is true. Assumptions are used as lemmas to other assertions.