copilot-theorem-4.7.1: k-induction for Copilot.

Safe Haskell | Safe
Language | Haskell2010

Copilot.Theorem

Description

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.

assume :: PropRef Universal -> Proof a Source #

Assume that a property, given by reference, holds.

admit :: Proof a Source #

Assume that the current goal holds.

type Proof a = ProofScheme a () Source #

A proof scheme with unit result.

type PropId = String Source #

A unique property identifier

data PropRef a Source #

Reference to a property.

data Universal Source #

Empty datatype to mark proofs of universally quantified predicates.

data Existential Source #

Empty datatype to mark proofs of existentially quantified predicates.