From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: tuhs-bounces@minnie.tuhs.org X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from minnie.tuhs.org (minnie.tuhs.org [45.79.103.53]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 74967d10 for ; Tue, 7 Aug 2018 09:20:13 +0000 (UTC) Received: by minnie.tuhs.org (Postfix, from userid 112) id 3CBF4A19FC; Tue, 7 Aug 2018 19:20:12 +1000 (AEST) Received: from minnie.tuhs.org (localhost [127.0.0.1]) by minnie.tuhs.org (Postfix) with ESMTP id 091ADA19CF; Tue, 7 Aug 2018 19:19:49 +1000 (AEST) Authentication-Results: minnie.tuhs.org; dkim=pass (1024-bit key; unprotected) header.d=yaccman.com header.i=@yaccman.com header.b=Mi3WPx2d; dkim-atps=neutral Received: by minnie.tuhs.org (Postfix, from userid 112) id 1EBE1A19CF; Tue, 7 Aug 2018 19:19:47 +1000 (AEST) X-Greylist: delayed 43212 seconds by postgrey-1.35 at minnie.tuhs.org; Tue, 07 Aug 2018 19:19:46 AEST Received: from pdx1-sub0-mail-fallback-a1.g.dreamhost.com (ip-64-90-62-138.dreamhost.com [64.90.62.138]) by minnie.tuhs.org (Postfix) with ESMTPS id 0D109A19CC for ; Tue, 7 Aug 2018 19:19:46 +1000 (AEST) Received: from homiemail-a145.g.dreamhost.com (sled11376.sd.dreamhost.com [10.50.1.152]) (using TLSv1.1 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by pdx1-sub0-mail-fallback-a1.g.dreamhost.com (Postfix) with ESMTPS id 325E328D9B7 for ; Mon, 6 Aug 2018 14:19:34 -0700 (PDT) Received: from homiemail-a145.g.dreamhost.com (localhost [127.0.0.1]) by homiemail-a145.g.dreamhost.com (Postfix) with ESMTP id BA02F6000131D; Mon, 6 Aug 2018 14:19:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=yaccman.com; h=message-id :from:to:in-reply-to:subject:date:content-type:mime-version; s= yaccman.com; bh=K7Jrpd900cqS3MWu0ZCTI6o2HwA=; b=Mi3WPx2dI0eO4Dbo ygiQZYEqFK5MPKpxVLJpBQewnMDcm0UtZg03QtO4OCSFDyqKAJaPGgl7drCkC8Jq +w2F4u3GWoV50C6IZDHU1DtnaUFjWqEhQUqcxXSRysF4uMu/HAc4Z8y+B9MZ/Dyi 5kXADjcnI63mT3V8SEWa7Kyxgv0= Received: from localhost (alc-nat.dreamhost.com [66.33.206.8]) (using TLSv1 with cipher ECDHE-RSA-AES128-SHA (128/128 bits)) (No client certificate requested) (Authenticated sender: scj@yaccman.com) by homiemail-a145.g.dreamhost.com (Postfix) with ESMTPSA id B10E66000130C; Mon, 6 Aug 2018 14:19:31 -0700 (PDT) Message-Id: <50772e199f3dcc5d4eba34d17322b5aef0aa0441@webmail.yaccman.com> From: "Steve Johnson" To: "Hellwig Geisse" , tuhs@minnie.tuhs.org X-Mailer: Atmail 7.8.0.2 X-Originating-IP: 68.65.225.230 in-reply-to: <1533573030.3671.98.camel@mni.thm.de> Date: Mon, 06 Aug 2018 14:19:31 -0700 Content-Type: multipart/alternative; boundary="=_3c4c300af56a09a2439fd363438e27f9" MIME-Version: 1.0 Subject: Re: [TUHS] TUHS Digest, Vol 33, Issue 5 X-BeenThere: tuhs@minnie.tuhs.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: The Unix Heritage Society mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: tuhs-bounces@minnie.tuhs.org Sender: "TUHS" --=_3c4c300af56a09a2439fd363438e27f9 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable =0AI take a somewhat more relaxed view of what a spec should be:=0AIt sh= ould describe a program with enough completeness that a competent=0Aprog= rammer could write it from the spec alone.=0AEach section of the spec sh= ould be capable of being tested.=0AIf all the tests for all the sections= pass, then the program is ready=0Afor general use.=0A=0AThe formal syst= ems I have seen would roll over and die when presented=0Awith=0Aeven a s= imple compiler.=C2=A0 Additionally, being able to specify that a=0Aparti= cular=0Afunction be carried out by a heapsort, for example, would requir= e that=0Athe=0Aformalism could describe the heapsort and prove it correc= t.=C2=A0 These=0Adon't=0Agrow on trees...=0A=0ASteve=0A=0A----- Original= Message -----=0AFrom: "Hellwig Geisse" =0ATo= :=0ACc:=0ASent:Mon, 06 Aug 2018 18:30:30 +0200=0AS= ubject:Re: [TUHS] TUHS Digest, Vol 33, Issue 5=0A=0A On Mo, 2018-08-06 a= t 08:52 -0700, Bakul Shah wrote:=0A > =0A > What counts as a "formal spe= c"? Is it like Justice Potter Stewart's=0A > "I know it when I see it" d= efinition or something better?=0A > =0A=0A For me, a "formal spec" shoul= d serve two goals:=0A 1) You can reason about the thing that is specifie= d.=0A 2) The spec can be "executed" (i.e., there is an=0A =C2=A0 =C2=A0i= nterpreting mechanism, which lets the spec behave=0A =C2=A0 =C2=A0like t= he real thing).=0A=0A Hellwig=0A --=_3c4c300af56a09a2439fd363438e27f9 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I take a somewhat more relaxed view of what a spec should b= e:
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 re= ady
for general use.

The formal syste= ms I have seen would roll over and die when presented with
eve= n a simple compiler.=C2=A0 Additionally, being able to specify that a pa= rticular
function be carried out by a heapsort, for example, w= ould require that the
formalism could describe the heapsort an= d prove it correct.=C2=A0 These don't
grow on trees...

Steve



----- Original Message -----
From:
"Hellwig G= eisse" <hellwig.geisse@mni.thm.de>

To:
<tu= hs@minnie.tuhs.org>
Cc:

Sent:
Mon, 06 Aug 2018 18:30:30 +0200
Subject:
Re: [TUHS] TUHS Digest, Vol 33, Issue 5

<= br>=0AOn Mo, 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
=0A> =0A> What counts as a "formal spec"? Is it like Justice Potter Stewa= rt's
=0A> "I know it when I see it" definition or something better= ?
=0A>

=0AFor me, a "formal spec" should serve two goals:<= br>=0A1) You can reason about the thing that is specified.
=0A2) The= spec can be "executed" (i.e., there is an
=0A=C2=A0 =C2=A0interpreti= ng mechanism, which lets the spec behave
=0A=C2=A0 =C2=A0like the rea= l thing).

=0AHellwig
--=_3c4c300af56a09a2439fd363438e27f9--