Re: Suitability for small Windows projects

[Robert A Duff <bobduff@world.std.com>]

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!

> 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?)

> 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.

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)?

- Bob