I'm having a question inspired by exercise 14 from section 1.2.1 of Donald Knuth's The Art of Computer Programming. It's phrased in the following way:

(R. W. Floyd) Prepare a computer program that accepts, as input, programs in some programming language together with optional assertions, and that attempts to fill in the remaining assertions necessary to make a proof that a computer program is valid.

Knuth directs to see the papers by R. W. Floyd and J. C. King in IFIP Congress proceedings, 1971. However, this document turned out to be very hard to find in the Internet, whilst being necessary to understand the problem better.

I do want to know whether this problem is still unsolved as it was when Knuth last updated that book, and, whether it is solved or not, I want to shed some more light for myself into this problem by reviewing additional related sources connected to it which you know and can share, as the Internet that I know turned out to be a scarce place for such information.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.