Safe Haskell	None
Language	Haskell2010

Language.Verification.Conditions

Contents

Types
Generating Verification Conditions
Combinators
Propositions

Description

Combinators for generating verification conditions for programs.

Synopsis

data Assignment expr var where
- Assignment :: var a -> expr var a -> Assignment expr var
data AnnSeq expr var cmd
- = JustAssign [Assignment expr var]
- | CmdAssign cmd [Assignment expr var]
- | Annotation (AnnSeq expr var cmd) (Prop (expr var) Bool) (AnnSeq expr var cmd)
type Triplet expr var a = (Prop (expr var) Bool, Prop (expr var) Bool, a)
skipVCs :: (HMonad expr, MonadGenVCs expr var m) => Triplet expr var () -> m ()
assignVCs :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) => Triplet expr v (Assignment expr v) -> m ()
sequenceVCs :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) => (Triplet expr v cmd -> m a) -> Triplet expr v (AnnSeq expr v cmd) -> m [a]
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)
multiIfVCs :: (HMonad expr, Monad m) => (Triplet expr v cmd -> m ()) -> (cond -> Prop (expr v) Bool) -> Triplet expr v [(Maybe cond, cmd)] -> m ()
whileVCs :: (HMonad expr, MonadGenVCs expr v m) => (Triplet expr v cmd -> m ()) -> (cond -> Prop (expr v) Bool) -> Prop (expr v) Bool -> Triplet expr v (cond, cmd) -> m ()
subAssignment :: (HMonad expr, VerifiableVar v) => Assignment expr v -> Prop (expr v) a -> Prop (expr v) a
chainSub :: (HMonad expr, VerifiableVar v) => Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
joinAnnSeq :: AnnSeq expr var cmd -> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
newtype JoinAnnSeq expr var cmd = JoinAnnSeq {
- tryJoinAnnSeq :: Maybe (AnnSeq expr var cmd)
}
joiningAnnSeq :: AnnSeq expr var cmd -> JoinAnnSeq expr var cmd
emptyAnnSeq :: AnnSeq expr var cmd
propAnnSeq :: Prop (expr var) Bool -> AnnSeq expr var cmd
cmdAnnSeq :: cmd -> AnnSeq expr var cmd
module Language.Expression.Prop

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

Instances details

(Pretty1 var, Pretty2 expr) => Pretty (Assignment expr var) Source #
Instance details Defined in Language.Verification.Conditions Methods pretty :: Assignment expr var -> String Source # prettysPrec :: Int -> Assignment 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

Instances details

Functor (AnnSeq expr var) Source #
Instance details Defined in Language.Verification.Conditions 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 #
Instance details Defined in Language.Verification.Conditions Methods fold :: Monoid m => AnnSeq expr var m -> m # foldMap :: Monoid m => (a -> m) -> AnnSeq expr var a -> 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 #
Instance details Defined in Language.Verification.Conditions 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 #
Instance details Defined in Language.Verification.Conditions 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

Instances details

Semigroup (JoinAnnSeq expr var cmd) Source #
Instance details Defined in Language.Verification.Conditions 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 #
Instance details Defined in Language.Verification.Conditions 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