Re: Suitability for small Windows projects

[Peter Amey <pna@praxis-cs.co.uk>]

In article <8ss9fb$6m7$1@nnrp1.deja.com>,
  Robert Dewar <robert_dewar@my-deja.com> wrote:
> In article <8smc96$hs7$1@nnrp1.deja.com>,
>   r_c_chapman@my-deja.com wrote:
> > We're thinking about it, but it's a fair way off yet.  Some
> history:
> > generics were broken in Ada83 to a point where they simply
> couldn't
> > be seriously considered for SPARK83.  In Ada95, things are
> better,
> > so there's some possiblility of a limited form of generic
> units in
> > SPARK95 - the main restriction will be, of course, on the form
> > of generic formal parameters allowed.
>
> I don't buy the above for a moment, there is no HUGE difference
> between Ada 83 and Ada 95 here, given that SPARK would only
> allow a limited form of generics in either environment.
>

I hate disagreeing with Robert because it is such a reliable way of
making yourself look stupid; however, I have to risk it in this case.

Generics were not included in SPARK 83 for three reasons:
1. We wanted to write a formal definition of SPARK and were not at all
sure we could do it for generics.  I believe this has been a tricky area
for some of the attempts to produce formal definitions of Ada.
2.  Complexity: we wanted SPARK to be a simple language with simple
semantics.  It was not at all clear that we could defined a subset of
SPARK 83 generics that would be useful, simple and maintain SPARK's
properties of compiler-independence, elaboration-order independence etc.
3.  As Rod alluded to in his reply, the SPARK 83 generic contract model
is indeed "broken".  This is freely acknowledged in the Ada 95 Rationale
in Section II.11 which actually uses the word "broken"!

We are looking at generics for SPARK 95 with the objective of being able
to annotate generics such that their annotations will be valid for any
instantiation.  In principle this could give use "re-usable proof".  The
changes to the generic parameter model of SPARK 95 are essential for
this.  (We may still have to prove freedom from exceptions on an
instantiation-by-instantiation basis but that is another story).

As an example of the kind of difficulty we have to take into
account (not an 83 vs 95 issue in this case), consider a discrete type
parameter.  This would allow the ordering operators to be used as well
as things like 'Pred/'Succ.  Boolean would be a valid match for the
parameter; however, SPARK does not consider Booleans to be ordered so
the body would be illegal in this case.

Our best guess is that will allow parameterisation by type (e.g. stack
of widgets, stack of thingies); parameterisation by some constant (e.g.
stack capable of holding N things); and parameterisation by some literal
value (e.g. port-inboard engine controller, starboard-outboard engine
controller).  Subprogram parameters and generic packages seem rather
unlikely at present.

regards


Peter


Sent via Deja.com http://www.deja.com/
Before you buy.