I always believed in this. When given a more complex problem or a trickier algorithm it helps enormously if you can express it in mathematical notation and have some calculus at your disposal that manipulates these expressions. In Java and other iterative programming languages it makes sense to work with things like precondition and postcondition (ideally as mathematical expressions) and calculi like weakest precondition, loop invariants etc. I've written a small paper that illustrates the concepts and gives some pointers to literature. I will keep posting examples to solving problems this way in this blog. Also check out this paper for another nice example of deriving a program.
