[Haskell-cafe] Proving programs

[Christopher Howard]

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?

-- 
frigidcode.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 553 bytes
Desc: OpenPGP digital signature
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130101/571dc421/attachment.pgp>