Re: Strategies with SPARK which does not support exceptions

[Claude <claude.defour@orange.fr>]

On Jun 17, 8:33 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Hello,
>
> (This topic will probably not be the most exiting topic to some people).
>
> When I use SPARK, or even when I don't use SPARK while I still have SPARK  
> design style in mind (even with Pascal which I still use), I have like any  
> one else, to forget about exceptions.
>
> So, let us talk and comment about design strategies in this area (if  
> someones wish to).

Hello Yannick

You are talking about Ada.  Just add annotation and you get SPARK and
static analysis.

SPARK is about
  - Data and information flow analysis annotations ensure that data
are used in the expected way.
  - Proof of absence of run-time errors that can spare exception error
handling and defensive programming.

Just have a look on the Phil Torney web site (SparkSure) and download
his Proof of Absence of Run-Time Error tutorial
http://www.sparksure.com/resources/Proof_Annotations.zip

It worth to have a glance at it...

Claude