In particular define more precisely what are the SPARK global contracts
and specify which errors can be found (and how) during the different
phases of the project (software requirements development, etc.).