Le Tue, 01 Jan 2013 14:24:04 -0900, Christopher Howard a écrit :

I'm working through a video lecture describing how to prove programs correct, by first translating the program into a control flow representation and then using propositional logic. In the control flow section, the speaker described how the program should be understood in terms of an input vector (X, the inputs to the program), a program vector (Y, the storage variables), and an output vector (Z, the outputs of the program), with X mapping into Y, Y being affected by execution, and X and Y mapping into Z.

However, only part way into the video, two practical questions come to mind:

1. Does this approach need to be adjusted for a functional language, in which computation is (at least idealistically) distinct from control flow?

2. How do we approach this for programs that have an input loop (or recursion)? E.g., I have an application that reads one line for stdin, modifies said line, outputs to stdout, and repeats this process until EOF? Should I be thinking of every iteration as a separate program?

Have you heard of Agda and Curry-Howard? For imperative programs, you may also be interested in Hoare logic. There are also some tools you may be interested in: - Atelier B - Why3 And probably many others.