verifiable-expressions-0.4.0: An intermediate language for Hoare logic style verification.

Safe HaskellNone
LanguageHaskell2010

Language.Verification.Conditions

Contents

Description

Combinators for generating verification conditions for programs.

Synopsis

Types

data Assignment expr var where Source #

An assignment of a particular expression to a particular variable.

Constructors

Assignment :: var a -> expr var a -> Assignment expr var 

Instances

(Pretty1 k var, Pretty2 k k expr) => Pretty (Assignment k expr var) Source # 

Methods

pretty :: Assignment k expr var -> String Source #

prettysPrec :: Int -> Assignment k expr var -> ShowS Source #

data AnnSeq expr var cmd Source #

An annotated sequence. Consists of runs of assignments, with other commands separated by annotations.

Constructors

JustAssign [Assignment expr var]

Just a series of assignments without annotations

CmdAssign cmd [Assignment expr var]

A command followed by a series of assignments

Annotation (AnnSeq expr var cmd) (Prop (expr var) Bool) (AnnSeq expr var cmd)

An initial sequence, followed by an annotation, then another sequence

Instances

Functor (AnnSeq expr var) Source # 

Methods

fmap :: (a -> b) -> AnnSeq expr var a -> AnnSeq expr var b #

(<$) :: a -> AnnSeq expr var b -> AnnSeq expr var a #

Foldable (AnnSeq expr var) Source # 

Methods

fold :: Monoid m => AnnSeq expr var m -> m #

foldMap :: Monoid m => (a -> m) -> AnnSeq expr var a -> m #

foldr :: (a -> b -> b) -> b -> AnnSeq expr var a -> b #

foldr' :: (a -> b -> b) -> b -> AnnSeq expr var a -> b #

foldl :: (b -> a -> b) -> b -> AnnSeq expr var a -> b #

foldl' :: (b -> a -> b) -> b -> AnnSeq expr var a -> b #

foldr1 :: (a -> a -> a) -> AnnSeq expr var a -> a #

foldl1 :: (a -> a -> a) -> AnnSeq expr var a -> a #

toList :: AnnSeq expr var a -> [a] #

null :: AnnSeq expr var a -> Bool #

length :: AnnSeq expr var a -> Int #

elem :: Eq a => a -> AnnSeq expr var a -> Bool #

maximum :: Ord a => AnnSeq expr var a -> a #

minimum :: Ord a => AnnSeq expr var a -> a #

sum :: Num a => AnnSeq expr var a -> a #

product :: Num a => AnnSeq expr var a -> a #

Traversable (AnnSeq expr var) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b) #

sequenceA :: Applicative f => AnnSeq expr var (f a) -> f (AnnSeq expr var a) #

mapM :: Monad m => (a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b) #

sequence :: Monad m => AnnSeq expr var (m a) -> m (AnnSeq expr var a) #

(Pretty2 * * expr, Pretty1 * var, Pretty cmd) => Pretty (AnnSeq expr var cmd) Source # 

Methods

pretty :: AnnSeq expr var cmd -> String Source #

prettysPrec :: Int -> AnnSeq expr var cmd -> ShowS Source #

type Triplet expr var a = (Prop (expr var) Bool, Prop (expr var) Bool, a) Source #

Generating Verification Conditions

skipVCs :: (HMonad expr, MonadGenVCs expr var m) => Triplet expr var () -> m () Source #

Generates verification conditions for a skip statement.

assignVCs :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) => Triplet expr v (Assignment expr v) -> m () Source #

Generates verification conditions for an assignment.

sequenceVCs :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) => (Triplet expr v cmd -> m a) -> Triplet expr v (AnnSeq expr v cmd) -> m [a] Source #

Generates verification conditions for a sequence of commands.

ifVCs :: (HMonad expr, MonadGenVCs expr v m) => (Triplet expr v cmd -> m a) -> (cond -> Prop (expr v) Bool) -> Triplet expr v (cond, cmd, cmd) -> m (a, a) Source #

Generates verification conditions for a two-branch if command.

multiIfVCs :: (HMonad expr, Monad m) => (Triplet expr v cmd -> m ()) -> (cond -> Prop (expr v) Bool) -> Triplet expr v [(Maybe cond, cmd)] -> m () Source #

Generates verification conditions for a multi-branch if-then-else-... command.

whileVCs Source #

Arguments

:: (HMonad expr, MonadGenVCs expr v m) 
=> (Triplet expr v cmd -> m ()) 
-> (cond -> Prop (expr v) Bool) 
-> Prop (expr v) Bool

Loop invariant

-> Triplet expr v (cond, cmd) 
-> m () 

Generates verification conditions for a while loop.

Combinators

subAssignment :: (HMonad expr, VerifiableVar v) => Assignment expr v -> Prop (expr v) a -> Prop (expr v) a Source #

Substitutes variables in the given proposition based on the given assignment.

chainSub :: (HMonad expr, VerifiableVar v) => Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool Source #

Chains substitutions, substituting using each assignment in the given list in turn.

joinAnnSeq :: AnnSeq expr var cmd -> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd) Source #

Joins two annotations together without a Hoare annotation in between. Fails if this would place two non-assignment commands after each other, because these need an annotation.

newtype JoinAnnSeq expr var cmd Source #

JoinAnnSeq forms a Monoid out of AnnSeq by propagating failure to join arising from joinAnnSeq.

Constructors

JoinAnnSeq 

Fields

Instances

Semigroup (JoinAnnSeq expr var cmd) Source # 

Methods

(<>) :: JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd #

sconcat :: NonEmpty (JoinAnnSeq expr var cmd) -> JoinAnnSeq expr var cmd #

stimes :: Integral b => b -> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd #

Monoid (JoinAnnSeq expr var cmd) Source # 

Methods

mempty :: JoinAnnSeq expr var cmd #

mappend :: JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd #

mconcat :: [JoinAnnSeq expr var cmd] -> JoinAnnSeq expr var cmd #

joiningAnnSeq :: AnnSeq expr var cmd -> JoinAnnSeq expr var cmd Source #

emptyAnnSeq :: AnnSeq expr var cmd Source #

propAnnSeq :: Prop (expr var) Bool -> AnnSeq expr var cmd Source #

cmdAnnSeq :: cmd -> AnnSeq expr var cmd Source #

Propositions