Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide a partial answer to one of its main issue which is scalability.
Copilot-theorem is a Copilot library aimed at checking automatically some safety properties on Copilot programs. It includes:
- A prover producing native inputs for the Kind2 model checker.
- A What4 backend that uses SMT solvers to prove safety properties.
Synopsis
- instantiate :: Proof Universal -> Proof Existential
- assume :: PropRef Universal -> Proof a
- admit :: Proof a
- type Proof a = ProofScheme a ()
- type PropId = String
- data PropRef a
- data Universal
- data Existential
Documentation
instantiate :: Proof Universal -> Proof Existential Source #
Instantiate a universal proof into an existential proof.
type Proof a = ProofScheme a () Source #
A proof scheme with unit result.
data Existential Source #
Empty datatype to mark proofs of existentially quantified predicates.