Re: Strategies with SPARK which does not support exceptions

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 17 Jun 2010 19:11:29 +0200, Warren <ve3wwg@gmail.com> a écrit:
> It is often not sufficient to simply know that OK is false.
> For example, wouldn't it be nice for the user to know that
> the open failed because of permissions, instead of the file
> not existing.
>
> Warren

Hillo Warren

I see what you mean (I like the C analogy for this, that is meaningful),  
while I don't fully agree with this later point : an exception typically  
do not holds such details. The exception says “If fails”, and don't say  
why (or just sightly, via its ID). Don't confuse Ada exception mechanism  
with other OO exception mechanisms, which comes with many and too much  
(because unusable in real life) members to hold informations about the  
exception occurence.

By the way, you are talking about propagated exceptions (as you talked  
about callers). I did not already set up a strategy for this. The way I  
was talking about just applies to exception raised and caught inside the  
same subprogram. I suppose this way could be extended to propagated  
exceptions, but I'm afraid of bloating doing so. I though about something  
looking like “software register” (analogy with CPU status registers), but  
I'm afraid this may not be safe (while luckily, SPARK can help a lot to  
properly use global variables ;) ).

Have a nice day

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.