First of all, is this only possible on algorithms which have no side effects?
Secondly, where could I learn about this process, any good books, articles, etc?
+2
A:
Usually proofs of correctness are very specific to the algorithm at hand.
However, there are several well known tricks that are used and re-used again. For example, with recursive algorithms you can use loop invariants.
Another common trick is reducing the original problem to a problem for which your algorithm's proof of correctness is easier to show, then either generalizing the easier problem or showing that the easier problem can be translated to a solution to the original problem. Here is a description.
If you have a particular algorithm in mind, you may do better in asking how to construct a proof for that algorithm rather than a general answer.
ldog
2010-01-27 19:06:25
Algorithm reduction (especially described as in the link you offer) is a theoretical tool to demonstrate that a problem is at least as hard as another. These proofs, often done in the Turing machine computation model, are hand-wavy affairs and nothing like formal (machine-checkable) proofs. They are often done for problems to hard to be useful in practice (the example in your link is for the Halting problem; showing a problem is NP-hard by reducing a known NP-hard problem to it is also popular). In short, I'm not sure problem reduction, as linked, has anything to do with formal correctness.
Pascal Cuoq
2010-01-28 20:51:02
Hmm maybe reduction is not the correct term I should be using here. When I say reduction I meant something along the lines of the following example. Suppose that you have an algorithm that computes the intersection of N rectangles, which you know is correct. Suppose you have another problem for which there exists a non-trivial translation of that problem to the problem of computing the intersection of N rectangles. Then you use the first algorithm to compute the solution to the latter problem. All that remains is showing that the translation is correct.
ldog
2010-01-28 21:26:51
But I can see that this is confusing, its a trick that relies on the fact that you make use of a well known algorithm that is known to be correct (in this case the one to compute the intersection of N rectangels.) I can see where the confusion comes as to whether this is a method of proving or providing a correct algorithm.
ldog
2010-01-28 21:27:12
+5
A:
COQ is a proof assistant that produces correct ocaml output. It's pretty complicated though. I never got around to looking at it, but my coworker started and then stopped using it after two months. It was mostly because he wanted to get things done quicker, but if you need to verify an algorithm this might be a good idea.
Here is a course that uses COQ and talks about proving algorithms.
And here is a tutorial about writing academic papers in COQ.
nlucaroni
2010-01-27 19:07:05
+1
A:
I think that verifying the correctness of an algorithm would be validating its conformance with a specification. There is a branch of theoretical Computer Science called Formal Methods which may be what you are looking for if you need to get as close to proof as you can. From wikipedia,
Formal Methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems
You will be able to find many learning resources and tools from the multitude of links on the linked Wikipedia page and from the Formal Methods wiki.
Brabster
2010-01-27 19:07:46
+2
A:
Buy these books: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
The Gries book, Scientific Programming is great stuff. Patient, thorough, complete.
S.Lott
2010-01-27 19:09:09
+3
A:
- It's generally a lot easier to verify/prove correctness when no side effects are involved, but it's not an absolute requirement.
- You might want to look at some of the documentation for a formal specification language like Z. A formal specification isn't a proof itself, but is often the basis for one.
Jerry Coffin
2010-01-27 19:13:04
And if you like Z, be confident that you will find tools to incorporate it in the process of writing a formally correct algorithm: http://www.bmethod.com/php/methode-b-en.php
Pascal Cuoq
2010-01-28 20:40:12
+1
A:
Logic in Computer Science, by Huth and Ryan, gives a reasonably readable overview of modern systems for verifying systems. Once upon a time people talked about proving programs correct - with programming languages which may or may not have side effects. The impression I get from this book and elsewhere is that real applications are different - for instance proving that a protocol is correct, or that a chip's floating point unit can divide correctly, or that a lock-free routine for manipulating linked lists is correct.
ACM Computing Surveys Vol 41 Issue 4 (October 2009) is a special issue on software verification. It looks like you can get to at least one of the papers without an ACM account by searching for "Formal Methods: Practice and Experience".
mcdowella
2010-01-27 20:16:23
"Formal methods" encompass all the objectives you cited. I'm in the sub-field of "proving programs correct" and I have to admit that until now the big industrial successes have come from the other sub-fields (just wait till next year!). A conference such as FMWEEK is somewhat puzzling because it gathers people with all these different approaches and objectives, but we do have a lot in common and a lot to exchange.
Pascal Cuoq
2010-01-28 20:27:07
+1
A:
The tool Frama-C, for which Elazar suggests a demo video in the comments, gives you a specification language, ACSL, for writing function contracts and various analyzers for verifying that a C function satisfies its contract and safety properties such as the absence of run-time errors.
An extended tutorial, ACSL by example, shows examples of actual C algorithms being specified and verified, and separates the side-effect-free functions from the effectful ones (the side-effect-free ones are considered easier and come first in the tutorial). This document is also interesting in that it was not written by the designers of the tools it describe, so it gives a fresher and more didactic look at these techniques.
Pascal Cuoq
2010-01-28 20:36:32
A:
If you are familiar with LISP then you should definitely check out ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
redtuna
2010-02-04 01:30:28