2 Jan 00:24 2013

## Proving programs

```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

```
```_______________________________________________
```
2 Jan 10:03 2013

### Re: Proving programs

```Le Tue, 01 Jan 2013 14:24:04 -0900,
Christopher Howard <christopher.howard <at> 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:
```

2 Jan 18:22 2013

### Re: Proving programs

```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 <christopher.howard <at> frigidcode.com> wrote:

> 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 <at> kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt
```
3 Jan 07:14 2013

### Re: Proving programs

```On Wed, Jan 2, 2013 at 12:22 PM, Simon Thompson <s.j.thompson <at> kent.ac.uk> wrote:
> Christopher, there's an introduction to proof for functional programs at
>
>   http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf
>

Simon, is it possible to get the list of the bibliographic references
used in the chapter?

Best regards,

--

--
Andrés

_______________________________________________
```
3 Jan 14:07 2013

### Re: Proving programs

Which book does that chapter belongs to?

-Satvik

On Thu, Jan 3, 2013 at 11:44 AM, Andrés Sicard-Ramírez wrote:
On Wed, Jan 2, 2013 at 12:22 PM, Simon Thompson <s.j.thompson <at> kent.ac.uk> wrote:
> Christopher, there's an introduction to proof for functional programs at
>
>   http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf
>

Simon, is it possible to get the list of the bibliographic references
used in the chapter?

Best regards,

--
Andrés

_______________________________________________

```_______________________________________________
```
3 Jan 14:11 2013

### Re: Proving programs

```On Thu, Jan 3, 2013 at 8:07 AM, satvik chauhan <mystic.satvik <at> gmail.com> wrote:
> Which book does that chapter belongs to?

http://www-fp.dcs.st-and.ac.uk/pfpbook/

--

--
Andrés

_______________________________________________