Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
celinval opened this issue Jul 23, 2024 · 1 comment
Open
Assignees
Labels
Maintenance Maintenance related issues for the challange

Comments

@celinval
Copy link

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.

@celinval celinval added the Maintenance Maintenance related issues for the challange label Jul 23, 2024
@celinval celinval self-assigned this Jul 23, 2024
@celinval
Copy link
Author

celinval commented Oct 8, 2024

I do wonder if we should only update the requires for now.

BTW, don't bother with the rustc_contracts change, because I think rustc might special case attributes starting with rustc_, and the name may change in the future..

@celinval celinval assigned tautschnig and unassigned celinval Oct 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Maintenance Maintenance related issues for the challange
Projects
None yet
Development

No branches or pull requests

2 participants