| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Copilot.Theorem.Prove
Description
Connection to theorem provers.
Synopsis
- data Output = Output Status [String]
- data Status
- data Prover = forall r.Prover {
- proverName :: String
- startProver :: Spec -> IO r
- askProver :: r -> [PropId] -> [PropId] -> IO Output
- closeProver :: r -> IO ()
- type PropId = String
- data PropRef a where
- type Proof a = ProofScheme a ()
- type UProof = Writer [Action] ()
- data ProofScheme a b where
- Proof :: Writer [Action] b -> ProofScheme a b
- data Action where
- data Universal
- data Existential
- check :: Prover -> Proof a
- prove :: Spec -> PropId -> UProof -> IO Bool
- combine :: Prover -> Prover -> Prover
Documentation
Output produced by a prover, containing the Status of the proof and
additional information.
Status returned by a prover when given a specification and a property to prove.
A connection to a prover able to check the satisfiability of specifications.
The most important is askProver, which takes 3 arguments :
- The prover descriptor
- A list of properties names which are assumptions
- A properties that have to be deduced from these assumptions
Constructors
| forall r. Prover | |
Fields
| |
type Proof a = ProofScheme a () Source #
A proof scheme with unit result.
type UProof = Writer [Action] () Source #
A sequence of computations that generate a trace of required prover
Actions.
data ProofScheme a b where Source #
A proof scheme is a sequence of computations that compute a result and
generate a trace of required prover Actions.
Constructors
| Proof :: Writer [Action] b -> ProofScheme a b |
Instances
| Applicative (ProofScheme a) Source # | |
Defined in Copilot.Theorem.Prove Methods pure :: a0 -> ProofScheme a a0 # (<*>) :: ProofScheme a (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b # liftA2 :: (a0 -> b -> c) -> ProofScheme a a0 -> ProofScheme a b -> ProofScheme a c # (*>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b # (<*) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a a0 # | |
| Functor (ProofScheme a) Source # | |
Defined in Copilot.Theorem.Prove Methods fmap :: (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b # (<$) :: a0 -> ProofScheme a b -> ProofScheme a a0 # | |
| Monad (ProofScheme a) Source # | |
Defined in Copilot.Theorem.Prove Methods (>>=) :: ProofScheme a a0 -> (a0 -> ProofScheme a b) -> ProofScheme a b # (>>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b # return :: a0 -> ProofScheme a a0 # | |
Prover actions.
data Existential Source #
Empty datatype to mark proofs of existentially quantified predicates.
prove :: Spec -> PropId -> UProof -> IO Bool Source #
Try to prove a property in a specification with a given proof scheme.
Return True if a proof of satisfiability or validity is found, false
otherwise.
combine :: Prover -> Prover -> Prover Source #
Combine two provers producing a new prover that will run both provers in parallel and combine their outputs.
The results produced by the provers must be consistent. For example, if one
of the provers indicates that a property is Valid while another indicates
that it is Invalid, the combination of both provers will return an
Error.