Re: [TUHS] TUHS Digest, Vol 33, Issue 5

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" &lt;hellwig.geisse(a)mni.thm.de&gt; 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: 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