JavaToLaurel: emit a procedure (not a function) for @Pure methods#461
Draft
tautschnig wants to merge 1 commit into
Draft
JavaToLaurel: emit a procedure (not a function) for @Pure methods#461tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
Strata is removing Laurel `function`s (Strata PR #1408 "Remove functions"); transparent procedures take their place. jverify emitted a Laurel `function` for every @pure method, so it will stop translating once functions are gone. Emit a `procedure` instead. The transparency choice is unchanged: a @pure method with no ensures becomes a *transparent* procedure (visible body, no OpaqueSpec) — giving callers the same body-visible semantics functions had — and one with ensures (or a non-pure method) is opaque. The `function` and `procedure` builders have identical signatures, so only the constructor differs. Requires a Strata with #1408 (transparent-procedure support): the current pre-#1408 Strata rejects transparent non-functional procedures. Validated against the #1408 branch (`removeFunctions`, based on this submodule pin): @pure methods translate and verify; the residual test deltas are #1408's own diagnostic-wording / behaviour changes (e.g. "does not hold" -> "could not be proved"), matching the test updates #1408 made in Strata, not this change. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Strata is removing Laurel
functions (Strata PR #1408 "Remove functions"); transparent procedures take their place. jverify emitted a Laurelfunctionfor every @pure method, so it will stop translating once functions are gone.Emit a
procedureinstead. The transparency choice is unchanged: a @pure method with no ensures becomes a transparent procedure (visible body, no OpaqueSpec) — giving callers the same body-visible semantics functions had — and one with ensures (or a non-pure method) is opaque. Thefunctionandprocedurebuilders have identical signatures, so only the constructor differs.Requires a Strata with strata-org/Strata/#1408 (transparent-procedure support): the current pre-#1408 Strata rejects transparent non-functional procedures. Validated against the strata-org/Strata#1408 branch (
removeFunctions, based on this submodule pin): @pure methods translate and verify; the residual test deltas are #1408's own diagnostic-wording / behaviour changes (e.g. "does not hold" -> "could not be proved"), matching the test updates #1408 made in Strata, not this change.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.