Christopher, there's an introduction to proof for functional programs at
http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf
I hope that you find it useful.
Kind regards
Simon
On 1 Jan 2013, at 23:24, Christopher Howard
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?
Simon Thompson | Professor of Logic and Computation School of Computing | University of Kent | Canterbury, CT2 7NF, UK s.j.thompson@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt