From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: *
X-Spam-Status: No, score=1.1 required=5.0 tests=BAYES_40,INVALID_DATE
	autolearn=no autolearn_force=no version=3.4.4
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!samsung!know!news.cs.indiana.edu!nstn.ns.ca!watt.ccs.tuns.ca!macdonaldk
From: macdonaldk@watt.ccs.tuns.ca
Newsgroups: comp.lang.ada
Subject: Help with Ada proof needed.
Message-ID: <1991Mar29.002035.1@watt.ccs.tuns.ca>
Date: 29 Mar 91 04:20:35 GMT
List-Id: <comp.lang.ada>

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