[SystemSafety] Fetzer

paul_e.bennett at topmail.co.uk paul_e.bennett at topmail.co.uk
Tue Jun 18 23:18:56 CEST 2019


On 18/06/2019 at 7:34 PM, "Peter Bernard Ladkin" <ladkin at causalis.com> wrote:
>
>Some of us are old enough to remember the brouhaha caused by the 
>CACM publishing an article in 1988
>by the philosopher James H. Fetzer claimed two things: (a) program 
>verification is impossible, and
>(b) therefore the USG should stop funding it.
>
>I thought, and still do, that (a) has a simple two-line refutation 
>(OK, five lines. The proof is two
>lines, but the set-up takes three). Namely, that when you verify a 
>program (we mean here a real
>honest-to-goodness program, something that executes on HW) you 
>compare two things, the program with
>some sort of specification S. And if S happens to be logically 
>equivalent to TRUE, there is a
>one-inference proof in propositional logic that your program is 
>correct. Ergo verification is prima
>facie possible.
>
>It is also not the sole criterion for dependability: you need also 
>to check that your specification
>is correct.
>
>It is now generally agreed that program verification is indeed a 
>comparison of a program with some
>kind of specification. (I think it was then; it is clearly 
>expressed in Barry Boehm's SEE.)
>
>Fetzer's argument completely omitted considering specifications, 
>which is why it fails.
>
>Somehow, my two-line refutation didn't win acceptance amongst SW 
>engineers (Cliff may remember) and
>it never got published. But I was old and foolish then, and I'm 
>younger than that now.
>
>And where is Fetzer? Writing books that the Sandy Hook massacre 
>never happened, and losing in court.
>https://www.theguardian.com/us-news/2019/jun/18/sandy-hook-
>massacre-victim-father-wins-defamation-lawsuit

I certainly recall a lot of effort went into discussing how we ensured the
specifications could hang together logically way back in the early 1980's.
This was over a number of sessions being held at the then Bristol Polytechnic
but is now UWE Bristol. I sat through talks about Z and VDM as a means of
proferring such proofs. However, there are things about actual customer
specifications that really need quite some effort to bash into the right sort of
shape. Even getting the spec re-written to make some statement about what
the customer wanted and yielded as close to a PASS/FAIL indication as
was possible.

Code, written to meet those specifications should, from such a sound basis,
be  much easier to verify. Of course, with some systems, there was a need
to ensure teh addition of instrumentation points that would be useful to drive
a scope or something.

Therefore, I never believed in the voracity of Felzers claim. I was, after all,
building the control software for a rather large robot that, thankfully, has
successfully operated since 1985 on issue one of the s/w and is expected
to be in operation until 2030. It was interesting to check all the machine
positions were validly detected by a thorough step-by-step test regime that
we tracked with the aid of a Lotus-123 spreadsheet.

Regards

Paul E. Bennett IEng MIET
Systems Engineer
Lunar Mission One Ambassador
-- 
********************************************************************
Paul E. Bennett IEng MIET.....
Forth based HIDECS Consultancy.............
Mob: +44 (0)7811-639972
Tel: Due to relocation - new number TBA. Please use Mobile.
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************



More information about the systemsafety mailing list