Writing an unformal specification (a special case)

[fl]

 

If you look at the specification of fgetc in the C standard p. 296

 

http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf

 

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

 

[fl]

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