[TUHS] TUHS Digest, Vol 33, Issue 5

[Steve Johnson]

I take a somewhat more relaxed view of what a spec should be:
It should describe a program with enough completeness that a competent
programmer could write it from the spec alone.
Each section of the spec should be capable of being tested.
If all the tests for all the sections pass, then the program is ready
for general use.

The formal systems I have seen would roll over and die when presented
with
even a simple compiler.  Additionally, being able to specify that a
particular
function be carried out by a heapsort, for example, would require that
the
formalism could describe the heapsort and prove it correct.  These
don't
grow on trees...

Steve

----- Original Message -----
From: "Hellwig Geisse" <hellwig.geisse at mni.thm.de>
To:<tuhs at minnie.tuhs.org>
Cc:
Sent:Mon, 06 Aug 2018 18:30:30 +0200
Subject:Re: [TUHS] TUHS Digest, Vol 33, Issue 5

 On Mo, 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
 > 
 > What counts as a "formal spec"? Is it like Justice Potter Stewart's
 > "I know it when I see it" definition or something better?
 > 

 For me, a "formal spec" should serve two goals:
 1) You can reason about the thing that is specified.
 2) The spec can be "executed" (i.e., there is an
    interpreting mechanism, which lets the spec behave
    like the real thing).

 Hellwig

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://minnie.tuhs.org/pipermail/tuhs/attachments/20180806/a9e9dd10/attachment.html>