Attribute Macro pre::assure

#[assure]

Assure that a precondition holds.

This is the counterpart of the pre attribute.

Currently this attribute does not work by itself. It needs to be used inside of a context that is annotated by a pre attribute.

Basic usage example

Suppose you want to call the function use_foo from the example in the pre attribute documentation.

First you need to find out what its preconditions are. You can do that by looking at its documentation. For this example we can also look at the source code for the function and see the precondition there.

It has one precondition:

• is only called after init_foo was called

Armed with that knowledge, we can write the code to call the function.

use pre::pre;

#[pre] // This is required, so `assure` works
fn main() {
    // This call allows us to safely assure the precondition later.
    init_foo(/* ... */);

    #[assure(
        "is only called after `init_foo` was called",
        reason = "we just called `init_foo`"
    )]
    use_foo(/* ... */);
}

Terminology

The term assure was chosen because it most accurately describes the function of the attribute.

There are no guarantees that a precondition holds, other than the fact that the programmer promises that it does. The burden is still on the programmer in this case. pre only makes sure that the programmer cannot forget that a precondition exists and that no precondition is changed without the programmer noticing.

Syntax

The basic syntax of the assure attribute is:

#[assure(
    <first precondition>,
    reason = "<the reason why the first precondition can be assured>"
)]
#[assure(
    <second precondition>,
    reason = "<the reason why the second precondition can be assured>"
)]
#[assure(
    <third precondition>,
    reason = "<the reason why the third precondition can be assured>"
)]
foo();

To learn more about the precondition syntax and the possible types of preconditions, you should look at the documentation of the pre attribute.