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

Language.ImProve.Examples

Description

ImProve examples.

Synopsis

Documentation

buildGCD :: IO ()Source

Build the gcdMain code (i.e. gcd.c, gcd.h).

counter :: Stmt ()Source

A rolling counter verification example.

verifyCounter :: IO ()Source

Verify the counter example.

arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()Source

Arbiter specification.

arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()Source

Binding an arbiter implemenation to the arbiter specification.

arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source

An arbiter implementation.

arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source

An another arbiter implementation.

arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)Source

Yet another arbiter implementation.

verifyArbiters :: IO ()Source

Verify the different arbiter implementations.

buildArbiters :: IO ()Source

Build the different arbiter implementations.

runAll :: IO ()Source

Run all examples.