Skip to content

Clarify documentation of postcondition capture #1239

@jamadagni

Description

@jamadagni

- **Preconditions and postconditions.** A function declaration can include `pre(condition)` and `post(condition)` before the `= /* function body */`. Before entering the function body, preconditions are fully evaluated and postconditions are captured (and performs their captures, if any). Immediately before exiting the function body via a normal return, postconditions are evaluated. If the function exits via an exception, postconditions are not evaluated.

Before entering the function body, … and postconditions are captured (and performs their captures, if any)

Can this wording please be clarified a bit more?

The part in the () is clear enough, as it is about the values which need to be captured before entering the function body, but the other usage of the word “postconditions are captured” seems to indicate that there are two kinds of capture going on. What is it?

(I could as this as a discussion Q&A but I feel the documentation should be clarified hence filing as issue.)

Thanks!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions