List of all items

Structs

• backend::monte_carlo::MonteCarloVerifier
• backend::smt::SmtAssertion
• backend::smt::SmtProofObligation
• backend::smt::SmtVariable
• backend::why3::Why3Generator
• contracts::RareEvent
• distributions::Bernoulli
• distributions::Exponential
• distributions::Normal
• distributions::Uniform
• prob::Prob
• prob::ProbabilityDensity

Enums

• backend::smt::ObligationKind
• backend::smt::SmtSort
• contracts::EventVerification
• contracts::VerificationResult

Traits

• contracts::ProbabilisticContract
• contracts::StatisticalProperty

Attribute Macros

• ensures_expected
• prob_ensures
• prob_requires

Functions

• backend::smt::expected_value_obligation
• backend::smt::hoeffding_obligation
• backend::smt::postcondition_obligation
• backend::smt::precondition_obligation
• statistical::bounds::chernoff_bound
• statistical::bounds::compute_confidence
• statistical::bounds::hoeffding_bound
• statistical::estimators::confidence_interval
• statistical::estimators::estimate_probability
• statistical::estimators::sample_size_for_precision