Add preconditions and postconditions

[jyn514]

https://docs.rs/contracts/0.4.0/contracts/

• self-documenting
• catches more bugs
• only runs in debug mode
• what's not to love?

[jyn514]

To avoid compiling this for end users, a friend suggested using a feature which is enabled by default only in dev mode:

[profile.dev]
features = ["contracts", "color-backtrace"]

[karroffel]

Just mentioning that contracts by default will always run, but you can use the override_debug feature to make them debug only. In that case no further profile configuration should be needed, at least for the contracts crate.

[jyn514]

Just mentioning that contracts by default will always run, but you can use the override_debug feature to make them debug only. In that case no further profile configuration should be needed, at least for the contracts crate.

This will not run the contracts, but it will still compile the contracts crate.

[karroffel]

But compiling the attributes without the contracts crate will fail, unless I misunderstand how you intend to use the crate 🙃

[jyn514]

Something like this:

#[cfg_attr(feature = "contracts", post(old(self.lval) || old(self) == ret))]
fn rval(self) -> Expr {
    unimplemented!();
}

That does seem super verbose though ...