Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
Assignment :: var a -> expr var a -> Assignment expr var |
Instances
(Pretty1 var, Pretty2 expr) => Pretty (Assignment expr var) Source # | |
Defined in Language.Verification.Conditions 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.
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 # | |
Foldable (AnnSeq expr var) Source # | |
Defined in Language.Verification.Conditions 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 # | |
Traversable (AnnSeq expr var) Source # | |
Defined in Language.Verification.Conditions 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 # | |
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.
:: (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
.
JoinAnnSeq | |
|
Instances
Semigroup (JoinAnnSeq expr var cmd) Source # | |
Defined in Language.Verification.Conditions (<>) :: 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 # | |
Defined in Language.Verification.Conditions 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 #
Propositions
module Language.Expression.Prop