From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 1108a1,9a0ff0bffdf63657
X-Google-Attributes: gid1108a1,public
X-Google-Thread: f43e6,9a0ff0bffdf63657
X-Google-Attributes: gidf43e6,public
X-Google-Thread: fac41,9a0ff0bffdf63657
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,4b06f8f15f01a568
X-Google-Attributes: gid103376,public
From: Matthew Heaney <matthew_heaney@acm.org>
Subject: Re: Software landmines (loops)
Date: 1998/09/17
Message-ID: <m3iuin6bim.fsf@mheaney.ni.net>#1/1
X-Deja-AN: 391923151
Sender: matt@mheaney.ni.net
References: <m3ogt3qgca.fsf@mheaney.ni.net> <35f23ce2.7649859@news.erols.com>
 <6snn1b$c90$1@hirame.wwa.com> <35ef7dff.24318728@news.erols.com>
 <EyrHEC.My1@ecf.toronto.edu> <35f79e53.98130474@news.erols.com>
 <slrn6v1k5p.1lb.jdege@jdege.visi.com> <m3emtq4vhd.fsf@mheaney.ni.net>
 <35F6A611.2DD979FD@oma.com>
NNTP-Posting-Date: Wed, 16 Sep 1998 20:30:13 PDT
Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada
Date: 1998-09-17T00:00:00+00:00
List-Id: <comp.lang.ada>

Tim Ottinger <ottinger@oma.com> writes:

> Matthew Heaney wrote a very fine, well-researched note
> here. I think it was great, except that he took "reason
> about..." to mean "understand...". To understand a code
> fragment is not the same as to reason about it. 

I treat them as essentially the same.  I can reason about a code
fragment implemented in a real programming language, or I can reason
about a code fragment using Dijkstra's abstract programming language.

I can make mistakes in reasoning using either language.  So formalism is
great, but is not a panacea.  It's just another tool that should be in
every programmer's toolbox.

It may be time to cite another couple of papers on this very topic:

Program Verification: The Very Idea
James H. Fetzer
CACM, Sep 1988, Vol 31, No 9, p1048-1063

Social Processes and Proofs of Theorems and Programs
Richard A. De Millo
Richard J. Lipton 
Alan J. Perlis
CACM, May 1979, Vol 22, No 5, p271-280


> That said, I have to plan to go restructure a little 
> code, and catch up on reading /Structured Programming/
> (Dahl, Dijkstra, Hoare, academic press "computer
> science classics" series, ISBN 0-12-200550-3). 

I just got back from a business trip, and got about halfway through that
other classic, A Discipline of Programming (Prentice-Hall, 1976).  Great
stuff, although I recommend that those unfamiliar with the predicate
transformer technique start with David Gries' Science Of Programming.