
An introduction to computer programming motivated by successively transforming mathematical characterizations of program state.
The point of my post was that studying Dijkstra is essential even if we cannot follow his methods to the letter. The key is to improve our own thinking and adopt better and more productive work-habits.
You might also want to checkout Dijkstra's A Method of Programming and Wirth's Systematic Programming: An Introduction.
Two more;
* EWD316 - A Short Introduction to the Art of Programming.
* A Method of Programming - Book co-authored with W.H.J.Feijen. For some reason, this is not well known though it was written as a course textbook. Draft version here: https://www.softwareresearch.net/fileadmin/src/docs/teaching...
If you look at one of the books where he and his colleagues teach how to do this (for example, A Method of Programming, by Dijkstra and Fiejen) it's pretty clear that the programmer him(her)self is supposed to come up with the formal specification. Much of the book is about how to write the specifications.
The formal specifications are just assertions - they are Boolean expressions that express properties of the solution. For example the formal specification for a square root function might be abs(r*r - x) < d, where x is the number, r is the root, and d is an error tolerance.
In general these formal specifications cannot be mechanically compiled into an executable program - they are nonconstructive - like the square root example above. So you still have to find or invent an algorithm.
An interesting feature of Dijkstra's method is, he does suggest some heuristics for getting from the assertions to the code, that can help you discover an algorithm. They remove the mystery surrounding how some non-obvious algorithms were discovered.
Dijkstra's approach is actually a lot like test-driven development - the idea is, you start with some assertions that describe what the code is supposed to do, then you check the assertions as you go -- instead of writing a bunch of code and checking it at the end. The difference is just how you check the assertions - by running tests or by attempting a proof. Test cases are formal specifications too - they are just incomplete - somebody said they are 'specification by example'.