Help with Ada proof needed.

Help with Ada proof needed.

[macdonaldk]

I have a quick question.  If you choose to respond, I would be happy if you
could respond directly to me.

All work was done on an HP 9000/375 running HP-UX 7.03.

----------------------------------------------------------------------

In an Ada assignment, we were to use the delay statement in the body of a
function; an relevant example is as follows:

function TEST is

begin
-- a few simple arithmetic statements.

	delay 0.3;

-- a few more simple arithmetic statements.
end TEST;

The use of the delay statement was unnecessary, but the assignment required
its presence.

Part of the assignment asked us to prove that the delay actually occurred.

The students proved this by stating that, according to the Ada standard, a
delay statement, as used above, will cause a delay for at least 0.3 seconds.
We compiled the program on an Ada compiler.  Therefore, the delay operated as
expected.

The lecturer, however, wanted us to display the time of day both before and
after the delay occurred.  He argued that the elapsed time would prove that
the delay occurred.  This proof would make use of the CALENDAR package.

We argued that the lecturer's proof assumes that the CALENDAR package
operates properly; thus, shouldn't the CALENDAR package need to be proved to
operate correctly too?

Which leads us to the need to construct a complete Ada test suite, which
was already done by people FAR more experienced than us at testing Ada.

The fact that we are using an Ada compiler certifies the compiler operates
according to the Ada standard, and further proof on our part is not necessary.

----------------------------------------------------------------------

Although the proof presented by the students is not absolute, it is more
conclusive than that proposed by our lecturer.

Who do you feel is correct: are we correct, or do we have too much faith
in Ada.

Kevin Macdonald
Technical University of Nova Scotia
Halifax, Nova Scotia

Re: Help with Ada proof needed.

[Luke J. Rheaume]

>The fact that we are using an Ada compiler certifies the compiler operates
>according to the Ada standard, and further proof on our part is not 
>necessary.

The fact that you are useing an "Ada" compiler does not necessarily mean 
that it is a "Validated" "Ada" compiler.  The only way to know for sure is 
to get the validation number and the test version against which the 
compiler was validated.  DoD had to change there rules on the use of the 
"Ada" as a trademarked name because of a law suit....It use to be that you 
couldn't call it Ada unless you were validated, but that has changed.

Luke J. Rheaume
ljr@mitre.org

Re: Help with Ada proof needed.

[David Emery]

I personally do not know of any commercial (i.e. you pay $$ for it)
Ada compiler that is not validated.  It's of course possible now to
call something "Ada" and not have it be validated.  It's also very
unlikely, as the seller would receive major abuse from people who
discovered their Ada programs won't run.

DoD dropped the trademark registration because of a legal opinion that
stated the trademark was not enforcable.  

				dave emery
				emery@aries.mitre.org

Re: Help with Ada proof needed.

[George C. Harrison, Norfolk State University]

In article <1991Mar29.002035.1@watt.ccs.tuns.ca>, macdonaldk@watt.ccs.tuns.ca writes:
> In an Ada assignment, we were to use the delay statement in the body of a
> function; an relevant example is as follows:
> 
> function TEST is
> 
> begin
> -- a few simple arithmetic statements.
> 	delay 0.3;
> -- a few more simple arithmetic statements.
> end TEST;
> 
> Part of the assignment asked us to prove that the delay actually occurred.
> 
> The students proved this by stating that, according to the Ada standard, a
> delay statement, as used above, will cause a delay for at least 0.3 seconds.
> We compiled the program on an Ada compiler.  Therefore, the delay operated as
> expected.
> 
> The lecturer, however, wanted us to display the time of day both before and
> after the delay occurred.  He argued that the elapsed time would prove that
> the delay occurred.  This proof would make use of the CALENDAR package.
> 
> We argued that the lecturer's proof assumes that the CALENDAR package
> operates properly; thus, shouldn't the CALENDAR package need to be proved to
> operate correctly too?
> 
> Although the proof presented by the students is not absolute, it is more
> conclusive than that proposed by our lecturer.
> 
I happen to agree with you on this.  But I get the impression that the lecturer
wanted you to print the time or compute the time-difference using CALENDAR
rather than doing any testing of the "correctness" of delay.  

If he (or she) wanted you do use CALENDAR, then that he (or she) should have
said that.  You should get at least half credit for a cleaver (though
frustrating) answer.  :-)  

If indeed the lecturer wanted you to actually TEST (or simulate the test) of
the delay statement, then the use of CALENDAR would have been (in most cases)
appropriate.  On the surface the delay (number of DURATION type) and the
routines in CALENDAR seem to be independent, but if package body CALENDAR uses
delay in your implementation, this test solution might be invalid.

-- George C. Harrison                              -----------------------
----- Professor of Computer Science                -----------------------
----- Norfolk State University                     -----------------------
----- 2401 Corprew Avenue, Norfolk, Virginia 23504 -----------------------
----- INTERNET:  g_harrison@vger.nsu.edu ---------------------------------