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
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 AllE 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
- (|-) :: 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)) -> Name -> Stmt (E a)
- class Assign a where
- ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
- if_ :: E Bool -> Stmt () -> Stmt ()
- incr :: V Int -> Stmt ()
- decr :: V Int -> Stmt ()
- assert :: E Bool -> Stmt ()
- assume :: E Bool -> Stmt ()
- verify :: FilePath -> Int -> Stmt () -> IO ()
- code :: Name -> Stmt () -> IO ()
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 between two points.
Statements
Statement Labeling and Hierarchical Scope
(|-) :: 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.
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)) -> Name -> Stmt (E a)Source
Input variable declaration. Input variables are initialized to 0.
Variable Assignment
Conditional Execution
Incrementing and decrementing.
Assertions and Assumptions
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.
Verification
verify :: FilePath -> Int -> Stmt () -> IO ()Source
Verify a program.
^ verify pathToYices maxK program