Prev: Code Statement
Next: SPARK reserved and predefined words : alternative choices
From: Yannick Duchêne (Hibou57) on 19 May 2010 21:47
Le Wed, 19 May 2010 23:29:22 +0200, Peter C. Chapin <pcc482719(a)gmail.com>
a écrit:
> One thing I like about Ada in general is how you can express a design in
> package specifications and then let the compiler check a few things
> about its
> consistency before embarking on the implementation. With SPARK that
> effect is
> even greater. For example in my Cryptographic_Services package the
> Examiner
> initially complained about how there was no way to initialize one of my
> private types.
I've noticed the same, it requires some good practice to be applied,
someway comparable to what you could get with AdaControl and a good rules
file (I mean AdaControl's rules). As an example, SPARK sees an error if
you forget the give the name of procedure at its end statement.

While sometime, I would like to better understand some choices, like the
one I've meet, which is that it does not accept nested package
specifications, or, more important, why it don't wants “type ... is new
....;”. If I could understand the rational behind this latter restriction,
this could perhaps help me to redesign.
From: Gavino on 20 May 2010 07:03

"Yannick Duch�ne (Hibou57)" <yannick_duchene(a)yahoo.fr> wrote in message
news:op.vczdx3teule2fv(a)garhos...
>While sometime, I would like to better understand some choices, like the
>one I've meet, which is that it does not accept nested package
>specifications, or, more important, why it don't wants "type ... is new
>...;". If I could understand the rational behind this latter restriction,
>this could perhaps help me to redesign.

It's to avoid overloading, especially the implicit declaration of
user-defined subprograms.


From: Yannick Duchêne (Hibou57) on 20 May 2010 11:58
Le Thu, 20 May 2010 13:03:01 +0200, Gavino <invalid(a)invalid.invalid> a
écrit:
>> While sometime, I would like to better understand some choices, like the
>> one I've meet, which is that it does not accept nested package
>> specifications, or, more important, why it don't wants "type ... is new
>> ...;". If I could understand the rational behind this latter
>> restriction,
>> this could perhaps help me to redesign.
>
> It's to avoid overloading, especially the implicit declaration of
> user-defined subprograms.
While this only occurs with tagged types, and SPARK 95 has support for
tagged type. Or may be I'm wrong somewhere, or else, I did not understood
what you were to say.


--
There is even better than a pragma Assert: a SPARK --# check.
From: Gavino on 21 May 2010 06:42

"Yannick Duch�ne (Hibou57)" <yannick_duchene(a)yahoo.fr> wrote in message
news:op.vc0hbmfnxmjfy8(a)garhos...
>Le Thu, 20 May 2010 13:03:01 +0200, Gavino <invalid(a)invalid.invalid> a
�crit:
>> It's to avoid overloading, especially the implicit declaration of
>> user-defined subprograms.
>While this only occurs with tagged types, and SPARK 95 has support for
>tagged type. Or may be I'm wrong somewhere, or else, I did not understood
>what you were to say.

Firstly, derived types can introduce overloaded enumeration literals, which
SPARK prohibits.
Secondly, if the parent type is one declared immediately within the visible
part of a package, then certain subprograms declared there are implicitly
declared for the derived type, again a form of overloading.


From: Yannick Duchêne (Hibou57) on 25 May 2010 16:58
Le Fri, 21 May 2010 12:42:53 +0200, Gavino <invalid(a)invalid.invalid> a
écrit:
> Firstly, derived types can introduce overloaded enumeration literals,
> which
> SPARK prohibits.
> Secondly, if the parent type is one declared immediately within the
> visible
> part of a package, then certain subprograms declared there are implicitly
> declared for the derived type, again a form of overloading.
Yes, I forget about it, and especially about the first one (about
enumeration literals).

This part of the one which is the most troublesome to me with SPARK, as I
like to “type ... is new ...” some types are not be mixed and the
interface defines special function when it is required. At least, when
mixed is done, this is clearly visible and this is a clear indication on
source review to look at it three times better than two.

Subtype is nice with SPARK, as validity conditions are checked. But if the
source is to be as nice with and without SPARK, some troubles comes :
subtype are not so much nice without SPARK. Ada with SPARK less needs
derived types, and subtype is enough, but Ada without SPARK, needs derived
types. So I can't have something which is good without SPARK too... or I
have to make all numeric types independent, but doing so, I miss the
expression of relations between these types.

Any way, thanks for your reply, which was the good one (this recalled me a
detail I had forget, as I'm not really relying on it).

--
There is even better than a pragma Assert: a SPARK --# check.
First  |  Prev  | 
Pages: 1 2
Prev: Code Statement
Next: SPARK reserved and predefined words : alternative choices