Issue 3497: Postconditions for basic_syncbuf::emit()

Title: Postconditions for basic_syncbuf::emit()
Status: new
Section: [syncstream.syncbuf.members]
Submitter: Jonathan Wakely

Created on 2020-11-10.00:00:00 last changed 48 months ago

Messages

msg11622 (view)

Date: 2020-11-15.00:00:00

[ 2020-11-21; Reflector prioritization ]

Set priority to 3 during reflector discussions.

msg11610 (view)

Date: 2020-11-10.00:00:00

[syncstream.syncbuf.members] p2 says:

Postconditions: On success, the associated output is empty.

Are there any postconditions on failure? If part of the associated output was written, is that part still in the associated output? Will another call to emit() duplicate that part?

History
Date	User	Action	Args
2020-11-21 14:02:41	admin	set	messages: + msg11622
2020-11-10 00:00:00	admin	create