> ... (I have removed the point for clarity's sake.)
(I have removed the pointer for clarity's sake.)
> postcondition: result = EOF \/ \E x \in CInt result = x
postcondition: result = EOF \/ \E x \in CInt ( x >= 0 /\ result = x )
The condition is important because EOF is negative.
We might also add a conversion operator it would be still closer to the standard.
(Here we suppose that ConvertUnsignedChar2Int(x) can't be negative but it's not
clear at all.)
postcondition: result = EOF \/ \E x \in CUnsignedChar result = ConvertUnsignedChar2Int(x)
--
FL