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
condition
Statement Labels
label: { "label" '|' do a(); a b(); b }
Expressions
Constant Literals truetrue
falsefalse
0 0 100 100 1.0 1 -- float 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
- class AllE a => NumE a
- type Name = String
- data Theorem
- 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
- 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 :: E Bool -> Stmt ()
- theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem
- verify :: FilePath -> Stmt () -> IO ()
- code :: Name -> Stmt () -> IO ()
Types
A logical, arithmetic, comparative, or conditional expression.
A mutable variable.
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 between two points.
Statements
Variable Hierarchical Scope and Statement Labeling
(-|) :: Name -> Stmt a -> Stmt aSource
Labels a statement and creates a variable scope. 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.
Variable Declarations
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 theorems.
assume :: E Bool -> Stmt ()Source
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.
theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt TheoremSource
Defines a new theorem.
theorem name k lemmas proposition