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

[Patrick Graydon]

On 26 Feb 2014, at 22:33, Peter Bernard Ladkin <ladkin at rvs.uni-bielefeld.de> wrote:

> 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