Skip to content

Update contract syntax to include contract forms as proposed in the MCP #44

Open
@celinval

Description

@celinval

The experimental contract support MCP has been approved. The syntax proposed looks like the following:

    #[rustc_contracts::requires(for safety: self.len() > 0)]
    #[rustc_contracts::ensures(
        for safety: |output| output == old(self.start),
        for correctness: |_output| self.len() == old(self.len()) - 1)]
    unsafe fn next_unchecked(&mut self) -> usize {
        // function body
    }

The main difference to today's implementations are the following:

  1. Contract forms (for safety vs for correctness). More forms may be added later.
  2. rustc_contracts prefix instead of contracts.

Note that # 2 may not be a problem, per the initial PR. No matter what, we will still need to address # 1.

Metadata

Metadata

Assignees

Labels

MaintenanceMaintenance related issues for the challange

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions