Skip to content

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

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.

Activity

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

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