CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verifying Haskell programs by combining testing and proving

Peter Dybjer (Institutionen för datavetenskap, Programmeringslogik) ; Haiyan Qiao (Institutionen för datavetenskap, Programmeringslogik) ; Makoto Takeyama (Institutionen för datavetenskap, Programmeringslogik)
Proceedings 3rd International Conference on Quality Software, IEEE Computer Society Press p. 272-279. (2003)
[Konferensbidrag, refereegranskat]

We propose a method for improving confidence in the correctness of Haskell programs by combining testing and proving. Testing is used for debugging programs and specification before a costly proof attempt. During a proof development, testing also quickly eliminates wrong conjectures. Proving helps us to decompose a testing task in a way that is guaranteed to be correct. To demonstrate the method we have extended the Agda/Alfa proof assistant for dependent type theory with a tool for random testing. As an example we show how the correctness of a BDD-algorithm written in Haskell is verified by testing properties of component functions. We also discuss faithful translations from Haskell to type theory.

Nyckelord: program verification, random testing, proof-assistants, type theory, BDDs and Haskell



Denna post skapades 2006-08-25. Senast ändrad 2013-02-28.
CPL Pubid: 17642

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)

Ämnesområden

Annan matematik

Chalmers infrastruktur