Skip to content

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

Open
@celinval

Description

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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