Re: Correctness proving (Was: Clear and Unambiguous SOFTWARE requirements/specifications possible?)

Responding to Perryman...

General correctness proving is NP-complete.

Sure. But we solve np-Complete problems all the time.

No, we don't.
We come up with reasonable schemes that find "good" results (by some
given notion of "good" ) . And at times those schemes actually produce
the optimal result.

Sorry, but that is only true for heuristic algorithms where the algorithm may only find a local optimum.

The bulk of OR techniques -- like linear programming, dynamic programming, Out Of Kilter, etc. -- all provide a deterministic solution for problems like Traveling Salesman that will always be the absolute optimum.

(BTW, before you go too much further down this road be aware that I spent two decades of my career solving np-Complete problems.)

So for a sufficiently large system, complete proof of correctness is
effectively impossible (which is why ATP is one of the CS "grand
challenges" ) .

As I indicated, I think that feasibility is a matter of existing technology. The computers aren't big enough and the algorithms/languages for formal methods aren't sophisticated enough yet to enable dealing with large applications.

[More precisely, the representation of correctness proofs has not yet been formalized so that existing or future Operations Research techniques can be applied. Solving np-Complete problems requires both an algorithm and a representation of the problem that is appropriate for the algorithm. Today's technologies for correctness proofs are rudimentary at best, especially for representing the problem.]

1. Correctness is primarily based on the theorems of propositional, and
(first-order) predicate logic. The interactions between even the most basic
statements that can be defined for a system (FORALL etc) , are
combinatorial.

A potentially combinatorial solution does not preclude solving the problem; it just takes longer in the worst case. But those worst case situations arise so rarely that they are not worth worrying about.


The most basic OR problems (linear Simplex etc) do not suffer
combinatorial explosion.

Actually, they do. All OR algorithms I know of will resort to examining all possible solutions in the worst case, including Revised Dual Simplex. It just doesn't happen very often.

2. Proof of correctness is governed by matters far more brutal than
amount of computation (nasty as that is) . You have to deal with :

- decidability

Can you show that the things you want to hold are either true or false ??

- completeness

Assuming the things you want to hold are decidable, do you have enough
statements about the system to be able to show those things hold ??


#2 states there are things that you are never going to be able to show.
NP-complete states there are things that at worst require perhaps more
computational resource / effort than you may be prepared to expend / wait
for.


As I indicated in my other post, I think the computing space is *designed* so that such issues aren't a problem. The issue here is proving correctness of programs that are well-formed within the constraints of the computing space. The fact that problems exist that cannot be solved within those constraints is purely academic because one can't properly construct the program whose correctness can't be checked. IOW, it's the Catch-22 of Turing computing.


--
There is nothing wrong with me that could
not be cured by a capful of Drano.

H. S. Lahman
hsl@xxxxxxxxxxxxxxxxx
Pathfinder Solutions
http://www.pathfindermda.com
blog: http://pathfinderpeople.blogs.com/hslahman
"Model-Based Translation: The Next Step in Agile Development". Email
info@xxxxxxxxxxxxxxxxx for your copy.
Pathfinder is hiring: http://www.pathfindermda.com/about_us/careers_pos3.php.
(888)OOA-PATH
.

Relevant Pages

  • Re: Association vs Dependency
    ... The unique thing about the computing space is that it is highly ... Programming is all about FUNCTION. ... only methodology I've used for over a decade is S-M or the MBSE variant. ...
    (comp.object)
  • beta version of Victor Shoups book, "A Computational Introduction to Number Theory and Algebra&
    ... Computing with Large Integers ... The Basic Euclidean Algorithm ... Factoring and Computing Euler's phi-Function are Equivalent ... The Existence of Finite Fields ...
    (sci.crypt)
  • Re: Theodore Adorno, a prophet of data systems design
    ... > correct algorithm proof is a rarity. ... > to hinge on how one reads the bit about actual programming experience. ... > Perhaps Mr Nilges doesn't read those threads ... >> to people as a way of asserting authority easily. ...
    (comp.programming)
  • Re: Theodore Adorno, a prophet of data systems design
    ... with the idea of "proving" an algorithm to be correct. ... Perhaps Mr Nilges doesn't read those threads ... this newsgroup isn't about "asserting authority". ... since (in the context of a programming discussion) colour only ...
    (comp.programming)
  • Re: Why does Cantor a target for cranks?
    ... and wildberger doesn't give this the recognition it deserves ... that if we have a computing process that generates a stream of ... then it's meaningful for such a specific process (algorithm) ... or conflating various groups of order 6 into the ...
    (sci.math)