Safe Haskell	None
Language	Haskell2010

Language.Verification.Conditions

Contents

Types
Generating Verification Conditions
Combinators
Propositions

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 tryJoinAnnSeq :: Maybe (AnnSeq expr var cmd)

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

module Language.Expression.Prop