Re: [SystemSafety] Scalability of Formal Methods [was: Logic]

From: Patrick Graydon < >
Date: Thu, 27 Feb 2014 05:41:36 +0100

On 26 Feb 2014, at 22:33, Peter Bernard Ladkin <ladkin_at_xxxxxx

> Fetzer claims to show that programs can never be proved correct. Here is a simple, trivial counterexample to that claim. Consider the specification "P OR (NOT P)", where "P" is any proposition you care to express. Constructivists, who may doubt excluded middle, may rather consider "NOT P OR (NOT NOT P)". Call this specification S. Take any program you like: Prog. There is a rigorous proof that Prog fulfils S. For the classical statement, the proof is a couple lines long (think of it as the two lines of the truth table); for the constructivist about double that.

It seems I didn’t actually read this example earlier. That’ll teach me to reply at 2 in the morning because my flu woke me up again.

I can’t see how this example actually tells us anything interesting. If we’re free to define our terms to mean whatever we want, then we can define ‘specification’ to include statements that are trivially true and thus do not distinguish between non-empty sets of conforming and non-conforming programs. But nobody actually cares whether you can ‘prove’ that a program fulfils a spec that says ‘my program might do nothing or anything at all’. So if that is the counterexample, all you’ve succeeded in doing in my mind is demonstrating that I am interested in a narrower class of specifications, namely those that serve some engineering purpose.

— Patrick

Dr Patrick John Graydon
Postdoctoral Research Fellow
School of Innovation, Design, and Engineering (IDT) Mälardalens Högskola (MDH), Västerås, Sweden

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Feb 27 2014 - 05:41:49 CET

This archive was generated by hypermail 2.3.0 : Fri Feb 22 2019 - 15:17:06 CET