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

Language.ImProve

Contents

Synopsis

Types

data E a Source

Instances

Eq (E a) 
Fractional (E Float) 
(Num a, AllE a, NumE a) => Num (E a) 
Show (E a) 

data V a Source

Instances

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

class AllE a whereSource

Methods

zero :: (Name -> a -> m (V a)) -> aSource

Instances

class AllE a => NumE a Source

Instances

Expressions

Constants

true :: E BoolSource

True term.

false :: E BoolSource

False term.

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

Arbitrary constants.

Variable Reference

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

References a variable.

Logical Operations

not_ :: E Bool -> E BoolSource

Logical negation.

(&&.) :: E Bool -> E Bool -> E BoolSource

Logical AND.

(||.) :: E Bool -> E Bool -> E BoolSource

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.

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.

(/.) :: E Float -> Float -> E FloatSource

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

Hierarchical Scope and Annotations

scope :: Name -> Stmt a -> Stmt aSource

Creates a hierarchical scope.

annotate :: Name -> Stmt a -> Stmt aSource

Add an annotation to a statement. Useful for requirement trace tags.

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

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

Conditional Execution

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

Conditional if-else.

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

Conditional if without the else.

Incrementing and decrementing.

incr :: V Int -> Stmt ()Source

Increments an E Int.

decr :: V Int -> Stmt ()Source

Decrements an E Int.

Assertions and Assumptions

assert :: Name -> E Bool -> Stmt ()Source

Assert that a condition is true.

assume :: Name -> E Bool -> Stmt ()Source

Declare an assumption condition is true.

Verification

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

Verify a program.

^ verify pathToYices maxK program

Code Generation

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

Generate C code.