5 ms·
> Poor man's runtime "dynamic" version. AKA: A much worse version. Contracts don't have to be evaluated dynamically, that's just one way they're implemented. S
by Jtsummers 4d ago
> Poor man's runtime "dynamic" version. AKA: A much worse version.
Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.
- rurban 3d agoMy rcc C compiler has a compile-time contracts and range/interval prover also. Needs -O3. For full formal proofs it's easier to use cbmc or esbmc though