Crate formal_spec

Source

Attribute Macrosยง

ensures
proof
requires