Re: Problems with SPARK 2015 and XMLAda

["Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org>]

On 08/20/2015 11:42 AM, Peter Chapin wrote:
> 
> To clarify, SPARK 2014 does allow raise statements in programs. However, each
> Raise statement carries with it a proof obligation that it will never execute.
> What's the point of that? It allows you to use raise statements to document
> "impossible" situations and then have the tools attempt to prove that those
> situations are, indeed, impossible.

SPARK is usually discussed in the context of complete programs, in which you
prove both that a subprogram is correct if the caller meets the precondition,
and that all calls meet the precondition.

However, in the case of a library unit that may be called by multiple programs,
it may be desirable to be able to prove the correctness of the unit without
being able to prove that all calls will be correct. In such cases, having
assertion checking catch the precondition violation and raise an exception is
the best solution should the unit be misused.

Also, some preconditions are very expensive to check; consider the "N is prime"
example discussed here in another thread. In such a case, it may be that the
normal processing allows detecting a precondition violation much more cheaply
than checking the precondition at the time of the call. In that case, a
conditional raise statement, which the condition being provably false if the
precondition is met. Then the unit can be proven correct if the precondition is
met, execute without the expensive precondition check in the case where the call
is not proven correct, and still raise an exception if it is called with the
precondition not met.

So it does seem there are cases where this feature may be useful.

-- 
Jeff Carter
"I've seen projects fail miserably for blindly
applying the Agile catechism: we're Agile, we
don't need to stop and think, we just go ahead
and code!"
Bertrand Meyer
150