Proving programs

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (565 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proving programs

AUGER Cédric
Le Tue, 01 Jan 2013 14:24:04 -0900,
Christopher Howard <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proving programs

Simon  Thompson
In reply to this post by Christopher Howard
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 <[hidden email]> 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
[hidden email] | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proving programs

Andrés Sicard-Ramírez
On Wed, Jan 2, 2013 at 12:22 PM, Simon Thompson <[hidden email]> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proving programs

satvik chauhan
Which book does that chapter belongs to?

-Satvik

On Thu, Jan 3, 2013 at 11:44 AM, Andrés Sicard-Ramírez <[hidden email]> wrote:
On Wed, Jan 2, 2013 at 12:22 PM, Simon Thompson <[hidden email]> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proving programs

Andrés Sicard-Ramírez
On Thu, Jan 3, 2013 at 8:07 AM, satvik chauhan <[hidden email]> wrote:
> Which book does that chapter belongs to?

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

--
Andrés

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe