# Re: Writing an unformal specification (a special case)

> ...  (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

• References: