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

Safe HaskellNone
LanguageHaskell2010

Language.While.Hoare

Synopsis

Documentation

data PropAnn l a Source #

Constructors

PropAnn (WhileProp l Bool) a 
Instances
(Pretty l, Pretty a) => Pretty (PropAnn l a) Source # 
Instance details

Defined in Language.While.Hoare

type AnnCommand l a = Command l (PropAnn l a) 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.

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.