SPARK is a tool which works modularly on your code. It cuts your code into small digestable pieces, "modules", and looks at each module separately. When it analyzes a module, it simply assumes that the other modules are correct. In SPARK, the notion of "module"  which is used is the subprogram. For any subprogram P, the contract of P (Pre- and Postcondition, and Globals and Depends contracts) summarizes what the analysis of other subprograms should assume about P when they call it. Of course, these assumptions are checked when P itself is analyzed. As such assumptions appear when a call appears in the subprogram text, one can draw such a picture to see where the assumptions happen:

On this picture, the blue boxes are suprograms which have been proved with SPARK and the blue arrows are calls between those subprograms, the green arrows are the assumptions which are made. Note that the assumption arrows go both ways, because (for example) the callee assumes its precondition, and the caller assumes the other guy's postcondition. As everything is proved with SPARK, all these mutual assumptions are in fact checked and not a problem. Note that even though there are recursive calls, the whole argument is not circular if you assume termination of the program - this is called partial correctness in the academic literature.

So in fact everything is OK, all assumptions are checked and we don't even need to draw such pictures right?

Well, what happens if everything is not proved? In this case, you end up with a picture like this:

The unfilled subprogram hasn't been proved. Now some of the green assumption arrows have become red: the assumption has not been checked by the SPARK tool. If we don't do anything, then the proofs of some other subprograms (striped) may become invalid.

There are many valid reasons for such a situation to arise, for example when the offending subprogram is not implemented in SPARK, but in full Ada or C, or if the proof of that subprogram would be very difficult.

As the assumptions cannot be checked with the SPARK tool, the solution is of course to check them using some other means. However, a prerequisite to that is knowing about them.

The paper we presented at the conference "Test and Proof 2014" in York, UK last week does exactly that: it proposes to change the SPARK tools so that the unmet assumptions are reported to the user if requested. In this way, the user can discharge them e.g. using test, or review, or static analysis.

The full paper is attached to this article, please check it out!