docs.rs failed to build spec-checker-0.9.4
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
Visit the last successful build:
spec-checker-0.9.3
M10: Spec proof checker. Spec §14.
Specs are properties attached to a function signature. The checker tries to prove a spec holds for every input that satisfies the quantifier constraints, and reports one of:
proved— the property holds (by randomized search across N trials, or by an SMT prover when one is available).counterexample— concrete inputs that falsify the property.inconclusive— the search couldn't decide one way or the other.
Strategies
- Randomized (default, pure-Rust). Generates inputs from a
deterministic seed, checks the property by actually running the
target function in the Lex VM. Reports
provedafter surviving 1000 trials by default. This is honest about the method viaevidence.method = "randomized". - SMT-LIB export. The spec can be lowered to SMT-LIB text for
pasting into an external Z3 (
z3 -smt2 file.smt). We don't link libz3 here to keep the dep surface light; that's a follow-up feature flag.
Spec DSL
spec clamp {
forall x :: Int, lo :: Int, hi :: Int where lo <= hi:
let r := clamp(x, lo, hi)
(r >= lo) and (r <= hi)
}