On software quality and engineering

[Sam Couter]

Matthew Hawkins <matt at mh.dropbear.id.au> wrote:
> How do you prove it is correct?  What is "correct" ?

Software is "correct" is when it fulfils its intended purpose.

It is possible to formally prove a piece of code is correct given
preconditions and postconditions. More correctly, the postconditions can
be shown to be satisfied by a piece of code if the preconditions are
satisfied.

However, this is rarely used in anything other than an academic setting.
The reason for this is because it's FUCKING HARD. Even the most simple
programming constructs like a one-line while loop take three pages of
working to formally prove correct.

It doesn't really solve the problem anyway. What if the bug isn't in the
while loop, it's in your postconditions (specification)? I quote Knuth:
"Beware of bugs in the above code; I have only proved it correct, not
tried it."

Formal specification languages just move the problem around: Instead of
testing, verifying and proving your code, you need to test, verify and
prove your specifications. In effect, the specifications *are* the code.

> For other problems which do not involve mathematics, you may be able to
> build a test harness around that specific part which proves it...

That's not proof, that's just testing. You can verify that it behaves
correctly in every case that you test, but that doesn't mean that it
behaves correctly over the entire input domain (unless you actually test
the entire input domain, which is not feasible most of the time).

> I was under the impression that languages like UML existed for two
> purposes, firstly to demonstrate a solution in a manner that managers
> understand, so they're able to "manage" the project.  Secondly, by
> serving as some kind of middle-ground like Java bytecode, it opens the
> doors for much of the real implementation to be auto-generated, freeing
> programmers from mundane tasks.

UML is a way of representing components and their interfaces and
interactions. It says nothing about operating constraints, behaviour,
system specifications or interface contracts.

Some UML tools are able to automatically construct classes or interfaces
in Java, C++ or other OO languages, but they're just empty skeletons.
The methods need to be implemented by a programmer.
-- 
Sam "Eddie" Couter  |  mailto:sam at couter.dropbear.id.au
Debian Developer    |  mailto:eddie at debian.org
                    |  jabber:sam at jabber.topic.com.au
OpenPGP fingerprint:  A46B 9BB5 3148 7BEA 1F05  5BD5 8530 03AE DE89 C75C
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: not available
Url : http://lists.samba.org/archive/linux/attachments/20021103/c6f5863a/attachment.bin