|
|
|
@ -46,7 +46,7 @@ In general, the following invariant holds for the read position, write position, |
|
|
|
|
[literal] |
|
|
|
|
[subs="verbatim,quotes"] |
|
|
|
|
-- |
|
|
|
|
`0` <= _read position_ <= _write position_ <= _capacity_ |
|
|
|
|
0 <= read position <= write position <= capacity |
|
|
|
|
-- |
|
|
|
|
|
|
|
|
|
When reading bytes from the `DataBuffer`, the read position is automatically updated in accordance with |
|
|
|
|