- l <= length s && l >= 0 ==>
- runStringConnection s (\c -> readBytes c (fromIntegral l)) ==
- Right (take l s, (drop l s, []))
+ runStringConnection s (\c -> readBytes c (fromIntegral l)) @?=
+ if l < 0
+ then Left "readBytes: negative count"
+ else case compare l (length s) of
+ EQ -> Right (take l s, (drop l s, []))
+ LT -> Right (take l s, (drop l s, []))
+ GT -> Left "EOF in input in readBytes"