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@mni.thm.de>

To:
<tuhs@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