Safe Haskell	None
Language	Haskell2010

Language.While.Hoare

Synopsis

type WhileProp l = Prop (WhileExpr l)
data PropAnn l a = PropAnn (WhileProp l Bool) a
type AnnCommand l a = Command l (PropAnn l a)
type MonadGen l = WriterT [WhileProp l Bool] Maybe
generateVCs :: VerifiableVar (WhileVar l) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
generateVCs' :: VerifiableVar (WhileVar l) => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l ()
splitSeq :: AnnCommand l a -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))

Documentation

type WhileProp l = Prop (WhileExpr l) Source #

data PropAnn l a Source #

Constructors

PropAnn (WhileProp l Bool) a

Instances

Instances details

(Pretty l, Pretty a) => Pretty (PropAnn l a) Source #
Instance details Defined in Language.While.Hoare Methods pretty :: PropAnn l a -> String Source # prettysPrec :: Int -> PropAnn l a -> ShowS Source #

type AnnCommand l a = Command l (PropAnn l a) Source #

type MonadGen l = WriterT [WhileProp l Bool] Maybe Source #

generateVCs :: VerifiableVar (WhileVar l) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool] Source #

Generate verification conditions to prove that the given Hoare partial correctness triple holds.

generateVCs' :: VerifiableVar (WhileVar l) => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l () Source #

splitSeq :: AnnCommand l a -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)) Source #

Split the command into all the top-level sequenced commands, interspersed with annotations. Returns Nothing if the command's sequences are not sufficiently annotated.