Re: Help with Ada proof needed.

[g_harrison@vger.nsu.edu (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 ---------------------------------