[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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)