If you look at the specification of fgetc in the C standard p. 296
and if you try to guess what are the preconditions and postconditions
of this routine, you will soon come to the conclusion that it is impossible
to give a formal equivalent of this specification because FILE is
not defined nor are the concepts of "next character", "being at the end of file"...
Most of this specification are indications about how the routine must
be implemented not a contract.
The more accurate contract we can expect to give is:
precondition: stream \in FILES (I have removed the point for clarity's sake.)
postcondition: result = EOF \/ \E x \in CInt result = x
(FILES is a CONSTANT, CInt is the range of the quantities of type int,
EOF a CONSTANT with some assumptions).
(I use the trick given by Stephan Merz in "A predictable choice in this group below.)
I wonder if mixing material related to the implementation to material
related to the contract is a good practice? I would say no.
(By the way fgetc is unsecure. On some implementations the conversion
of an unsigned char to an int wil lead to an unspecified behavior. It should be
documented in my opinion.)
--
FL