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

Safe HaskellNone
LanguageHaskell2010

Language.While.Hoare.Prover

Documentation

checkPartialHoare :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> Query (WhileVar l) (SBV Bool) Source #

provePartialHoare :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV, VarEnv (WhileVar l) ~ ()) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> IO (Either (VerifierError (WhileVar l)) Bool) Source #