Re: Suitability for small Windows projects

Re: Suitability for small Windows projects

[Gerhard Haering]

In article <8qr809$cjj@newshost.fujitsu.com.au>, Ray Smith wrote:
>Hi There,
>
>I have been looking into Ada for hobby programming.
>(I am a professional Cobol / Visual Basic programmer with small amounts of
>experience in about a dozen of other languages)
>
>I have read the FAQ, browsed www.adahome.com but still had a couple of
>questions I hope someone can answer.
>
>1.  Can Ada (Assume gnat) produce standalone Windows executables?  If so,
>how big are they compared to equivalent C executables? If no, how many files
>would need to be distributed to run the application?
>

GNAT can of course produce standalone Windows EXEs. These are statically
linked to the GNAT runtime and thus relatively large. If you ask me, I
also stumbled across the 100 KB Hello World compiled by GNAT. I used to
care about executable size, I do no more. Hardisk space is ridiculously
cheap and if you deliver software, you burn it on CD anyways.

>2.  Are there "good" libraries available for GUI, Winsockets and database
>connectivity?

There are libraries for all of these, but I haven't tried many of them
myself. You might want to check out http://www.adapower.com It's an
excellent place for Ada programmers. For GUI, there are several Windows
GUI packages. There is a binding to GLADE, a GTK+ cross platform GUI
builder. There is a binding to Winsock. ODBC, MySQL and Postgres database
bindings do also exist, but they seem to be much lower level than, say ADO
in Visual Basic.

>
>3.  Are there any DirectX or libraries available for making games? (I have
>read the history of Ada and understand the goals but that doesn't mean Ada
>can't be used for fun!!!)

The nearest thing I recall is an Ada game package for Linux framebuffer
and X ;-)


Gerhard Haering

Re: Suitability for small Windows projects

[Jeff Creem]

"Ray Smith" <Ray.Smith@fujitsu.com.au> wrote in message
news:8qr809$cjj@newshost.fujitsu.com.au...
> Hi There,
>
> I have been looking into Ada for hobby programming.
> (I am a professional Cobol / Visual Basic programmer with small amounts of
> experience in about a dozen of other languages)
>
> I have read the FAQ, browsed www.adahome.com but still had a couple of
> questions I hope someone can answer.
>
> 1.  Can Ada (Assume gnat) produce standalone Windows executables?  If so,
> how big are they compared to equivalent C executables? If no, how many
files
> would need to be distributed to run the application?
>
> 2.  Are there "good" libraries available for GUI, Winsockets and database
> connectivity?
>
> 3.  Are there any DirectX or libraries available for making games? (I have
> read the history of Ada and understand the goals but that doesn't mean Ada
> can't be used for fun!!!)
>
> Thanks,
>
> Ray Smith


I use Ada for fun all of the time (of course our ideas of fun are probably
different).

Go to www.adapower.com. It is more up to date and has a lot more information
about
using Ada on windows (mostly GNAT but there is no reason it has to be
GNAT...There are other
windows Ada compilers).

In fact, if you are going to write a game there is currently a $500.00 prize
being offered at adapower for
such a beast.

If you want to use DirectX you will need to download the directX SDK from
microsoft. I believe the
latest one comes with MS type libraries (to support thinks like Visual Basic
and other Langs).
With the type libraries and the COM tools at adapower you could be able to
build a very nice
DirectX binding (I have not played with the latest version but I was amazed
at how well earlier versions worked).

Depending on what you are doing or want to do I also sort of like doing some
GUI stuff with Gtk+
(http://gtkada.eu.org) Then your GUI can run on Solaris, Linux and
Win32...Gtk+ Probably not best choice for games
unless combined with OpenGL or something.

Good luck,
Jeff

Suitability for small Windows projects

[Ray Smith]

Hi There,

I have been looking into Ada for hobby programming.
(I am a professional Cobol / Visual Basic programmer with small amounts of
experience in about a dozen of other languages)

I have read the FAQ, browsed www.adahome.com but still had a couple of
questions I hope someone can answer.

1.  Can Ada (Assume gnat) produce standalone Windows executables?  If so,
how big are they compared to equivalent C executables? If no, how many files
would need to be distributed to run the application?

2.  Are there "good" libraries available for GUI, Winsockets and database
connectivity?

3.  Are there any DirectX or libraries available for making games? (I have
read the history of Ada and understand the goals but that doesn't mean Ada
can't be used for fun!!!)

Thanks,

Ray Smith

Re: Suitability for small Windows projects

[Tarjei T. Jensen]

Ray Smith
>I'm so surprised Ada isn't mentioned in magazines, newspapers and web
>development resource sites etc.


No reason to be surprised. Nobody in the Ada community except Richard Riehle
writes about Ada anywhere. You would probably have to threaten people with
serious physical injury in order to get them to write articles that makes Ada
visible outside "the congregation". On the other hand, we preach a lot to the
converted.


Greetings,

Re: Suitability for small Windows projects

[Gautier]

Tarjei T. Jensen:

> No reason to be surprised. Nobody in the Ada community except Richard Riehle
> writes about Ada anywhere. You would probably have to threaten people with
> serious physical injury in order to get them to write articles that makes Ada
> visible outside "the congregation". On the other hand, we preach a lot to the
> converted.

The french magazine "Programmez" has from time to time an article or a resource
about Ada - due to the efforts of J-P Rosen I think. On a recent issue I've
seen in the nearby supermarket there was on the cover something like
"CD includes...  GNATS 3.2, the ADA compiler for Linux" :-).
Someone succeeded to write an article in Dr Dobbs about Ada, games, tasking ->
  http://www.beesknees.freeserve.co.uk/articles/gnat.html

But these are isolated examples of course. Beside articles, a good way can be
to informatively (not religiously) advertise on other newsgroups. If you
type as keywords even basic Ada features (inline, generic, default parameter...)
on http://www.deja.com/usenet/ you'll be surprised how people wish them for
their common programming and they will be surprised that these features exist
in Ada for long...
______________________________________________________
Gautier  --  http://members.xoom.com/gdemont/gsoft.htm

Re: Suitability for small Windows projects

[Georg Bauhaus]

Gautier (gautier.demontmollin@maths.unine.ch) wrote:
: Tarjei T. Jensen:


: If you
: type as keywords even basic Ada features (inline, generic, default parameter...)
: on http://www.deja.com/usenet/ you'll be surprised how people wish them for
: their common programming and they will be surprised that these features exist
: in Ada for long...

Have you seen the new keywords added in Component Pascal,
successor to Oberon-2? :-)  And not a single mention of Ada :-(
http://www.oberon.ch/resources/component_pascal/evolution.html

Re: Suitability for small Windows projects

[tmoran]

I can address some of your questions:

1.  Can Ada (Assume gnat) produce standalone Windows executables?
  There are at least 5 vendors selling Ada compilers that target
Windows, including Gnat.  They vary in price and features. (Duh!)
Look at www.adapower.com for links.

2.  Are there "good" libraries available for GUI, Winsockets and database
connectivity?
  Win32Ada  A "thin" 1-1 binding that comes with Gnat and Aonix compilers.
  Ada Foundation Classes binding to MFC is available at least for Aonix.
  Jewl (John English's Windows Library) is available on the net.  A
    recent .zip file was 175K long.
  GWindows - Win32 RAD Ada 95 GUI Development Framework is available
    on the net.  A recent zip was 360K
  Claw (Class Library for Ada Windows) A stripped down version is available
    for free on the net.  A recent zip was 430K
  Windex, an object-oriented thick binding is available on the net.
    A recent zip was 620K
  Claw full version is available via www.rrsoftware.com   A recent
    zip was 1.6M, with a 95 page printed manual.
  Several sockets bindings are available on the net.
  An ODBC binding is available on the net, 50K zip.
  A binding to GTK is also available.

  Many of these can be downloaded for free. They vary greatly in features.
  Look at www.adapower.com for links.

Full Disclosure: I'm one of the developers of Claw.

Re: Suitability for small Windows projects

[Jeffrey Carter]

Ray Smith wrote:
> 
> Hi There,
> 
> I have been looking into Ada for hobby programming.
> (I am a professional Cobol / Visual Basic programmer with small amounts of
> experience in about a dozen of other languages)
> 
> I have read the FAQ, browsed www.adahome.com but still had a couple of
> questions I hope someone can answer.

adahome is, unfortunately, not maintained. A better site is
www.adapower.com.

> 
> 1.  Can Ada (Assume gnat) produce standalone Windows executables?  If so,
> how big are they compared to equivalent C executables? If no, how many files
> would need to be distributed to run the application?

Yes. If you want to do it the hard way, look at the examples that come
with GNAT. An easier way is to use GtkAda, a binding to GTK+ that has
been ported to Windows (www.adapower.com/gtkada/). However, GtkAda does
not yet support standalone executables. The easiest way is to use JEWL.
On adapower, follow the Links link to find JEWL in the Brighton
University Resource Kit for Students. Just above that link you will find
the Ada on Win32 link.

> 
> 2.  Are there "good" libraries available for GUI, Winsockets and database
> connectivity?

Yes. Adapower should be able to help you there.

> 
> 3.  Are there any DirectX or libraries available for making games? (I have
> read the history of Ada and understand the goals but that doesn't mean Ada
> can't be used for fun!!!)

Also on adapower is a link for Game Programming with Ada.

-- 
Jeff Carter
"You couldn't catch clap in a brothel, silly English K...niggets."
Monty Python & the Holy Grail

Re: Suitability for small Windows projects

[Ray Smith]

Thanks to everyone for responding.

http://www.adapower.com/  has lots of excellent info, should keep me busy
for a few weeks!

I'm so surprised Ada isn't mentioned in magazines, newspapers and web
development resource sites etc.
From my limited reading Ada is at least a match for the popular
C++/Java/Visual Basic/Delphi environments but yet doesn't even get a
mention.

>I also stumbled across the 100 KB Hello World compiled by GNAT. I used to
> care about executable size, I do no more. Hardisk space is ridiculously
> cheap and if you deliver software, you burn it on CD anyways.

It's not really the hard disk space I'm worried about,
Producing "reasonably" small standalone executables has two benefits for me:
1.  Programs can be easily downloaded from the net.
2.  The smaller the executable size the less RAM resources it uses (in
general).

The "100 KB Hello World" I beleive is good.
It's the "1.4 MB Hello World" program in Visual Basic with a 1.36 MB runtime
file that I'm trying to avoid.

Thanks again,

Ray Smith

Re: Suitability for small Windows projects

[tmoran]

>2.  Are there "good" libraries available for GUI, Winsockets and database
>connectivity?
  A downside to the plethora of libraries is of course that the farther
you go using one, the harder it becomes to switch to another.

Re: Suitability for small Windows projects

[Alexey V. Litvinov]

Ray Smith О©╫О©╫О©╫О©╫О©╫ О©╫ О©╫О©╫О©╫О©╫О©╫О©╫О©╫О©╫О©╫ <8qrs0i$kq2@newshost.fujitsu.com.au> ...

>I'm so surprised Ada isn't mentioned in magazines, newspapers and web
>development resource sites etc.
>From my limited reading Ada is at least a match for the popular
>C++/Java/Visual Basic/Delphi environments but yet doesn't even get a
>mention.

Good question...
I'm also occasionly take the book about her, and later been surprised that
earlier
I don't know nothing about this nice language.

>The "100 KB Hello World" I beleive is good.
>It's the "1.4 MB Hello World" program in Visual Basic with a 1.36 MB
runtime
>file that I'm trying to avoid.
>
Little hint: If you wish you may use executable packer (such as AsPack or
UPX)
little test:
hello.exe - 182k
after AsPack (www.aspack.com)
(24%) 45k.
In gnat also exist util gnatelim.exe for throwing unused routines from
executable.

Re: Suitability for small Windows projects

[Gautier]

Georg:

> Have you seen the new keywords added in Component Pascal,
> successor to Oberon-2? :-)  And not a single mention of Ada :-(
> http://www.oberon.ch/resources/component_pascal/evolution.html

That's terrible - I won't sleep anymore ;-). B.T.W. the text
is funny enough - especially the part about "String Support"...
They seem to develop that thing in "huis clos", for years.
By the time there were available compilers (Modula-2) it was already
disastrous. When I think a fraction of my taxes vanish there 8-( !

______________________________________________________
Gautier  --  http://members.xoom.com/gdemont/gsoft.htm

Re: Suitability for small Windows projects

[Ted Dennison]

In article <8qtsek$j7c$2@news-hrz.uni-duisburg.de>,
  sb463ba@l1-hrz.uni-duisburg.de (Georg Bauhaus) wrote:
> Have you seen the new keywords added in Component Pascal,
> successor to Oberon-2? :-)  And not a single mention of Ada :-(
> http://www.oberon.ch/resources/component_pascal/evolution.html

Hmmm. More interesting to me are some of the differences. I love those
procedure attributes. Ada has just one: "abstract". But it would be
really nice to be able to tell just by looking at the subprogram
prototype if a routine is an extension, extendable, or final. Right now
you have to look in other places (sometimes *several* other places) to
get that information.

--
T.E.D.

http://www.telepath.com/~dennison/Ted/TED.html


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

Re: Suitability for small Windows projects

[Brian Rogoff]

On Thu, 28 Sep 2000, Ted Dennison wrote:
> In article <8qtsek$j7c$2@news-hrz.uni-duisburg.de>,
>   sb463ba@l1-hrz.uni-duisburg.de (Georg Bauhaus) wrote:
> > Have you seen the new keywords added in Component Pascal,
> > successor to Oberon-2? :-)  And not a single mention of Ada :-(
> > http://www.oberon.ch/resources/component_pascal/evolution.html
> 
> Hmmm. More interesting to me are some of the differences. I love those
> procedure attributes. Ada has just one: "abstract". But it would be
> really nice to be able to tell just by looking at the subprogram
> prototype if a routine is an extension, extendable, or final. Right now
> you have to look in other places (sometimes *several* other places) to
> get that information.

I guess what I find most interesting is that a group of researchers
unconstrained by backward compatibility come up with a language that I
find significantly less elegant than Ada 95, even though it is roughly at
the same point in language design space. What about generics? 

And, since it is more relevant to Ada, what of generics in SPARK? I
remember asking about this a long time ago and someone from Praxis said 
a future version might support some form of generics. 

I shouldn't even mention overloading since it is controversial, but I
think the other Wirth family languages suffer for that omission. 
 
-- Brian

Re: Suitability for small Windows projects

[DuckE]

> It's not really the hard disk space I'm worried about,
> Producing "reasonably" small standalone executables has two benefits for
me:
> 1.  Programs can be easily downloaded from the net.
> 2.  The smaller the executable size the less RAM resources it uses (in
> general).
>
> The "100 KB Hello World" I beleive is good.
> It's the "1.4 MB Hello World" program in Visual Basic with a 1.36 MB
runtime
> file that I'm trying to avoid.
>

The issue of the size of executables has been beat to death on this
newsgroup.

My experience is you take a fairly big initial hit on size for the run-time
library, but
the incremental size isn't any worse than other languages (sometimes
better).

SteveD

> Thanks again,
>
> Ray Smith
>
>

Re: Suitability for small Windows projects

[Wes Groleau]

> No reason to be surprised. Nobody in the Ada community except Richard Riehle
> writes about Ada anywhere. 

Part of the problem (for some of us) is that the objections to Ada are
so
asinine that we have a hard time controlling our anger.  :-)

-- 
Wes Groleau
http://freepages.genealogy.rootsweb.com/~wgroleau

Re: Suitability for small Windows projects

[tmoran]

>> No reason to be surprised. Nobody in the Ada community except Richard Riehle
>> writes about Ada anywhere.
>
>Part of the problem (for some of us) is that the objections to Ada are
>so asinine that we have a hard time controlling our anger.  :-)
  The just arrived March 2000 "ACM Computing Surveys" has a 37 page
article "The Programming Languages and Systems for Prototyping
Concurrent Applications".  There are 4 mentions of Ada.  Three are to
the effect Ada was used in such and such a system.  The most recent
citation is 1991.  The fourth says "Languages based on the message
passing model include occam, Ada, SR, and many others.  As these
languages with their variations of message passing have been studied
extensively in the literature, we refer to Bal et al [1989] for an
overview, and do not discuss them in detail here."  #.#

Re: Suitability for small Windows projects

[Lao Xiao Hai]

"Tarjei T. Jensen" wrote:

> No reason to be surprised. Nobody in the Ada community except Richard Riehle
> writes about Ada anywhere. You would probably have to threaten people with
> serious physical injury in order to get them to write articles that makes Ada
> visible outside "the congregation". On the other hand, we preach a lot to the
> converted.

This is Richard Riehle speaking.   I appreciate the kind words about my articles
concerning Ada.    However, much credit should be given to others who have
been writing and publishing articles over the years.   Paul Pukite and Joyce
Tokar
come to mind immediately.   For many years, Do-While Jones was a lone voice
with detailed and entertaining articles regarding Ada.   More recently, there was
a
piece in COTS Journal written by the Ada Product Manager at Green Hills Software.

Others, including Tom Moran, have been published in Dr. Dobbs.    Ben Brosgol
and Ed Seidiwitz have kept the flame alive with their writing and their
conference
presentations.   Many others whose names do not jump out at me in this moment
have also contributed to the published Ada literature in periodicals.

Another thing I am noticing is the increase in awareness of Ada at both computer
conferences and in newly published books.    For a while there was almost no
mention of Ada.   Lately, especially in books on real-time and embedded systems,
I see more acknowledgement of Ada.   In a little book on embedded systems from
O'Reilly, the author even expresses a preference for Ada even though he
illustrates
his examples using C because of its popularity.   He also has some unkind things
to
say about C++.   In a recent comparative programming languages book, Programming
Language Pragmatics (Kaufmann),  the author is unusually fair regarding Ada.  In
Bob Binder's hefty tome on Object-Oriented Testing, Ada is one of the small set
of
languages selected for examples.

This trend is encouraging.  Instead of cheerleading articles about Ada, there is
great
value in seeing respected authors include it, matter-of-factly, in there
discussions of
larger issues.

Editors of periodicals are more amenable to articles that describe solutions
where Ada
was the programming language.   Almost no editor will choose an article that is
simply promoting Ada.   They will be fair if you have a viewpoint to share that
has
value to the computing community.  Most will not reject a good article simply
because you selected Ada for the solution.   They will reject an article that is
nothing
more than Ada evangelism.

There are so many exciting success stories out there that involve Ada.   It would
be
great to see more of you crafting some of those stories into publishable
articles.  If
you are unsure of your writing skills, enlist the help of a colleague who has
good
writing ability.

Richard Riehle

Re: Suitability for small Windows projects

[r_c_chapman]

In article
<Pine.BSF.4.21.0009280825480.29105-100000@shell5.ba.best.com>,
  Brian Rogoff <bpr@shell5.ba.best.com> wrote:

> And, since it is more relevant to Ada, what of generics in SPARK? I
> remember asking about this a long time ago and someone from Praxis
said
> a future version might support some form of generics.

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.

A particular issue would be the validity of the Examiner's static
analysis: we'd like the analysis results for a generic body
to be valid for all possible instantiations of that body.  This is
probably achievable for the static semantic rules (including flow
analysis), but looks far more difficult for the proof stuff - exception
freedom proofs critically depend on statically knowing attributes
such as 'First and 'Last of types, so we might have to do VC
generation on a per-instantiation basis.  This is hard, since
it imples implementing at least a simple form of expander
phase in the Examiner - something we currently don't have!

As always, we'll listen to users' requests, but this is not
currently a high-priority.
 - Rod Chapman
   SPARK Team
   Praxis Critical Systems


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

Re: Suitability for small Windows projects

[Robert Dewar]

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.


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

Re: Suitability for small Windows projects

[Peter Amey]

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.

Re: Suitability for small Windows projects

[Robert A Duff]

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

Re: Suitability for small Windows projects

[Peter Amey]

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.