Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
class ExtractIO m =>
ProvableM (m :: Type -> Type) asbv Data.SBV.Internals A type a is provable if we can turn it into a predicate, i.e., it has to return a boolean. This class captures essentially prove calls.
-
sbv Data.SBV.Internals No documentation available.
Power :: Int -> RegExp -> RegExpsbv Data.SBV.RegExp Exactly n repetitions, i.e., nth power
PartialCorrectness :: InductionStepsbv Data.SBV.Tools.Induction No documentation available.
-
sbv Data.SBV.Tools.Induction No documentation available.
-
sbv Data.SBV.Tools.KnuckleDragger Proof for a property. This type is left abstract, i.e., the only way to create on is via a call to lemma/theorem etc., ensuring soundness. (Note that the trusted-code base here is still large: The underlying solver, SBV, and KnuckleDragger kernel itself. But this mechanism ensures we can't create proven things out of thin air, following the standard LCF methodology.)
-
sbv Data.SBV.Tools.KnuckleDragger A proposition is something SBV is capable of proving/disproving in KnuckleDragger.
module Data.SBV.Tools.
Polynomial Implementation of polynomial arithmetic
class (Num a, Bits a) =>
Polynomial asbv Data.SBV.Tools.Polynomial Implements polynomial addition, multiplication, division, and modulus operations over GF(2^n). NB. Similar to sQuotRem, division by 0 is interpreted as follows:
x pDivMod 0 = (0, x)
for all x (including 0) Minimal complete definition: pMult, pDivMod, showPolynomial-
sbv Data.SBV.Tools.WeakestPreconditions A program over a state is simply a statement, together with a pre-condition capturing environmental assumptions and a post-condition that states its correctness. In the usual Hoare-triple notation, it captures:
{precondition} program {postcondition}We also allow for a stability check, which is ensured at every assignment statement to deal with ghost variables. In general, this is useful for making sure what you consider as "primary inputs" remain unaffected. Of course, you can also put any arbitrary condition you want to check that you want performed for each Assign statement. Note that stability is quite a strong condition: It is intended to capture constants that never change during execution. So, if you have a program that changes an input temporarily but always restores it at the end, it would still fail the stability condition. The setup field is reserved for any symbolic code you might want to run before the proof takes place, typically for calls to setOption. If not needed, simply pass return (). For an interesting use case where we use setup to axiomatize the spec, see Documentation.SBV.Examples.WeakestPreconditions.Fib and Documentation.SBV.Examples.WeakestPreconditions.GCD.