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

RFC: Quantifiers #3242

Merged
merged 4 commits into from
Jun 27, 2024
Merged

Conversation

feliperodri
Copy link
Contributor

RFC describing the support for existential and universal quantifiers in Kani.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@feliperodri feliperodri added this to the Function Contracts milestone Jun 7, 2024
@feliperodri feliperodri self-assigned this Jun 7, 2024
@feliperodri feliperodri requested a review from a team as a code owner June 7, 2024 21:46
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks Felipe. This is a very well-written RFC!

rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Show resolved Hide resolved
Copy link
Member

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok from my point of view, except I'd prefer a somewhat more precise language.

rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
@feliperodri feliperodri added the T-RFC Label RFC PRs and Issues label Jun 11, 2024
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good! Thanks

rfc/src/rfcs/0010-quantifiers.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0010-quantifiers.md Show resolved Hide resolved
Copy link
Contributor

@qinheping qinheping left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri enabled auto-merge (squash) June 27, 2024 06:48
@feliperodri feliperodri merged commit 997c95c into model-checking:main Jun 27, 2024
25 checks passed
@feliperodri feliperodri deleted the quantifiers-rfc branch June 27, 2024 16:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
T-RFC Label RFC PRs and Issues
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants