Skip to content

Clarify the contract of push_to/pull_from #358

Description

@akrzemi1

One minor problem and one major.

The minor problem. Why does the overload of pull_from has this negative requirement requires (!ReadSource) given that the subsumption relation between ReadStream and ReadSource already expresses it? An analogous thing applies to push_to.

The major problem. What is the intended postcondition of co_await push_to and co_await pull_from?

  1. Do we guarantee that the pumping will be performed (with the understanding that if it fails to be met, then the exception triggers stack unwinding and making sure that the code relying on the postcondition is never evaluated)?
  2. Or is it just "we will be issuing instructions to read from one stream and to write to another stream, and see what happens, and we will give you the status, and you deal with it"?

#350 depends on the answer to the postcondition question.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    Status
    Backlog

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions