Re: Suitability for small Windows projects

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

In article <wccbswb37ls.fsf@world.std.com>,
  Robert A Duff <bobduff@world.std.com> wrote:
> Peter Amey <pna@praxis-cs.co.uk> writes:
>
> >...  (We may still have to prove freedom from exceptions on an
> > instantiation-by-instantiation basis but that is another story).
>
> I don't see why you can't do it in an assume-the-worst way.
> And it seems desirable to make the proof totally independent of
> the instantiation.  Otherwise, your proofs are violating
> the contract model!

I really hope we can and with judicious use of attributes we may be able
to.  The idea of formally proven, exception-free, re-usable components
has a certain attraction.  It's just a bit too early to say.

>
> > 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.
>
> No, if you don't want Booleans to be ordered, then SPARK should
disallow
> instantiating with Boolean.  (By the way, *why* are Booleans not
ordered
> in SPARK?)

We will almost certainly adopt the view of prohibiting instantiation
with Boolean since all the alternatives would unduly restrict the use
generics could be put to.

Booleans were origially not ordered because the underlying language we
use for proof (FDL - Functional Description Language) does not have them
it was possible to construct rather esoteric invalid proofs by taking
advantage of that fact.  There has been a useful payoff in our proof of
exception freedom work: Boolean expressions in SPARK cannot raise
constraint errors.  For example you can't take 'Succ of True or other
sillies.  The limitation is not too restrictive in practice and we sugar
the pill by allowing Boolean'first and 'last but just defining them to
be synonyms of False and True.  So the only things really missing are <,
>, Succ and Pred.

[snip]
>
> What's the difficulty with subp params?  They of course have to have
> pre- and postconditions, and you would need to prove that the
> precondition of the formal implies the precondition of the actual and
so
> forth.  Also globals annotations?  Are there any specific problems
> (other than the fact that it's a big chunk of work)?

I don't think we _know_ it can't be done but it certainly is "a big
chunk of work"!  The usual SPARK tradition is to try and get something
useful into the language and do the gold-plating later; I would be very
pleased to do this with a limited form of generics and worry about
subprogram parameters later.

Thanks for the ideas and interest.

Peter



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