Christopher Howard | 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
AUGER Cédric | 2 Jan 10:03 2013
Picon

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:
(Continue reading)

Simon Thompson | 2 Jan 18:22 2013
Picon

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
Andrés Sicard-Ramírez | 3 Jan 07:14 2013
Picon

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
satvik chauhan | 3 Jan 14:07 2013
Picon

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 <andres.sicard.ramirez <at> gmail.com> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe




_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andrés Sicard-Ramírez | 3 Jan 14:11 2013
Picon

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane