We must include the standard I/O definitions, since we want to
    send formatted output to stdout and stderr.
    <<Header files to include>>=
    #include <stdio.h>
    @