RE: Software Design

RE: Software Design

[amado.alves]

<<
> "There are two ways of constructing a software design. One way is to
> make it so simple that there are obviously no deficiencies. And the
> other way is to make it so complicated that there are no obvious
>deficiencies." C. A. R. Hoare

It will be very interesting to see an operating system or at least
a (visual) text editor, which has obviously no deficiencies, and
at the same time is useful.

I'd like to propose new term "hoareware" for the kind of software
for which the quoted phrase is true.
>>

Cool name. But what's the denotation? I take it you mean (just) the second sentence in Hoare's paragraph. The "correctness by construction" series of papers by Peter Amey touch this (Google for it). Personally I want to believe. And I ponder this evidence from mathematics: that really very *complex* proofs are found flawless, i.e. absolutely correct, e.g. (the proofs of) Fermat's Last Theorem, the Four Coulor Theorem. So in sum I think I agree with what I think you're conjecturing: that for a piece of software to be useful it must be complex by necessity. But the lesson from mathematics says a complex thing can be shown correct. That is, what we need is not simple: it's a way to show (and experience) the complex correct. In a way, anti-Hoare. You know, "0% bugs."
 
(Sorry if I sound rambling. I am :-)
 
The one piece of complex software in the world that is flawless is perhaps TeX. But it took decades to show that. Not satisfactory. I dream of complex programs being proved correct just like complex mathematical proofs: by revision. Clearly one way to accomplish this is to write them in a rigourous and readable language and of course in very good style. Hence "100% Ada."
 

Re: Software Design

[(see below)]

On 13/12/03 2:18 am, in article
mailman.109.1071281924.31149.comp.lang.ada@ada-france.org, "amado.alves"
<amado.alves@netcabo.pt> wrote:

> And I ponder this evidence from mathematics: that really very *complex* proofs
> are found flawless, i.e. absolutely correct, e.g. (the proofs of) Fermat's
> Last Theorem, the Four Coulor Theorem.

But the Wiles proof of FLT was found to be erroneous shortly after after
publication. It has since been "debugged". Its present status is a matter of
the opinion of the mathematicians who participated in that effort, as far as
I can see. The 4CT was greeted with outright scepticism when announced. I do
not know what has happened since to confer "absolutely correct" credentials.

> a piece of software to be useful it must be complex by necessity

Agreed.

> But the lesson from mathematics says a complex thing can be shown correct.

I think this is highly questionable. Moreover, it is the proofs
(metaphorically, the programs) that are complex in the examples above. The
theorems (metaphorically, the specifications) are (very!) simply stated.
Software contends with complex, ill-defined and time-varying requirements
and specifications in a way that does not arise with these famous theorems.

>  That is, what we need is not simple: it's a way to show (and experience)
>  the complex correct. In a way, anti-Hoare. You know, "0% bugs."

Absolutely, yes. But the big problem, for software, is to know what standard
of correctness to hold the program to.

> The one piece of complex software in the world that is flawless is perhaps
> TeX. But it took decades to show that. Not satisfactory. I dream of complex
> programs being proved correct just like complex mathematical proofs: by
> revision. Clearly one way to accomplish this is to write them in a rigourous
> and readable language and of course in very good style. Hence "100% Ada."

Well, people tried and failed to prove the 4CT & FLT for hundreds of years.
8-)

-- 
Bill:Findlay chez Blue:Yonder dot:co:dot:uk (":" => "")

Re: Software Design

[Peter Amey]

[snip]
> 
> 
>>a piece of software to be useful it must be complex by necessity
> 
> 
[snip]

That may be true; however, it should be as simple as possible 
commensurate with performing its designated task.  Being elegant and 
precise is usually harder than being over-complex but always worth the 
effort.

To quote (or at least paraphrase) another mathematician (Pascal): "I 
apologise for writing you such a long letter, I did not have time to 
write a short one".


Peter

RE: Software Design

[Alexandre E. Kopilovitch]

amado.alves wrote:

>I dream of complex programs
>being proved correct just like complex mathematical proofs: by revision.

There is a common misconception (among non-mathematicians) about the nature
and power of mathematical proofs: those proofs do not signify for a final
and eternal truth as many non-mathematicians believe; a proof just exposes
a logic which leads to the theorem's conclusion. So anyone who relies upon
a theorem is supposed to check and agree with that logic. Because of that,
too complex proofs have less value in mathematics then simple proofs (too
few people can actually inspect the logic of, say, 100-page highly demanding
mathematical text), and therefore inventing of a new, simple and
straightforward proof for already proven (but only by lengthy and complex
proof) theorem is always regarded as quite respectable mathematical result.

> Clearly
>one way to accomplish this is to write them in a rigourous and readable language
>and of course in very good style. Hence "100% Ada."

Obviuosly, the language, terminology and notation used in a proof greatly
influences reader's ability to inspect its logic. A clear language,
well-chosen and stable terminology and notation are if fact prerequisites
for wide and effective use of a mathematical result. In this sense Ada
language is certainly on right way - Ada strives to provide exactly that -
clear, well-chosen and stable notation as well as basic level of the language
for programs/software, and a good exposition of a logic and intentions is
a highly useful thing even if it is somehow incomplete and/or unpolished
regarding to mathematical standards.

But anyway, what should be never forgotten - equally in software engineering
and in mathematical applications - that both ends of a proved thing must be
checked every time: that actual prerequisites are strong enough for the proof
to be applicable and that the theorem's conclusion is enough to satisfy
actual requirements. And this is the most critical point in usage of "already
proved" things.



Alexander Kopilovitch                      aek@vib.usr.pu.ru
Saint-Petersburg
Russia

Software Design

[Robert Spooner]

Al,

"There are two ways of constructing a software design. One way is to
make it so simple that there are obviously no deficiencies. And the 
other way is to make it so complicated that there are no obvious 
deficiencies." C. A. R. Hoare

I thought you might enjoy reading that.

Bob

-- 
                             Robert L. Spooner
                      Registered Professional Engineer
                        Associate Research Engineer
                   Intelligent Control Systems Department

          Applied Research Laboratory        Phone: (814) 863-4120
          The Pennsylvania State University  FAX:   (814) 863-7841
          P. O. Box 30
          State College, PA 16804-0030       rls19@psu.edu

Re: Software Design

[Peter Hermann]

Robert Spooner <rls19@psu.edu> wrote:
> I thought you might enjoy reading that.

and I think you should proceed reading the Spark book
"High Integrity Software"   ;-)

cheers,
ph

Re: Software Design

[(see below)]

On 12/12/03 2:43 pm, in article brck7d$m38$1@f04n12.cac.psu.edu, "Robert
Spooner" <rls19@psu.edu> wrote:

> "There are two ways of constructing a software design. One way is to
> make it so simple that there are obviously no deficiencies. And the
> other way is to make it so complicated that there are no obvious
> deficiencies." C. A. R. Hoare

Oh no!
Restrain yourselves, folks!
-- 
Bill:Findlay chez Blue:Yonder dot:co:dot:uk (":" => "")

Re: Software Design

[Alexandre E. Kopilovitch]

> "There are two ways of constructing a software design. One way is to
> make it so simple that there are obviously no deficiencies. And the 
> other way is to make it so complicated that there are no obvious 
>deficiencies." C. A. R. Hoare

It will be very interesting to see an operating system or at least
a (visual) text editor, which has obviously no deficiencies, and
at the same time is useful.

I'd like to propose new term "hoareware" for the kind of software
for which the quoted phrase is true.



Alexander Kopilovitch                      aek@vib.usr.pu.ru
Saint-Petersburg
Russia