Le Tue, 01 Jan 2013 14:24:04 -0900, Christopher Howard <christopher.how...@frigidcode.com> 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe