DocumentCode :
3251404
Title :
Verifying Haskell programs by combining testing and proving
Author :
Dybjer, Peter ; Haiyan, Qiao ; Takeyama, Makoto
Author_Institution :
Dept. of Comput. Sci., Chalmers Univ. of Technol., Goteborg, Sweden
fYear :
2003
fDate :
6-7 Nov. 2003
Firstpage :
272
Lastpage :
279
Abstract :
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.
Keywords :
binary decision diagrams; formal specification; functional languages; program debugging; program verification; theorem proving; type theory; Agda-Alfa proof assistant; BDD-algorithm; Haskell program; component function; program debugging; program specification; program testing; program verification; proof development; proof-assistant; random testing; type theory; Binary decision diagrams; Boolean functions; Costs; Data structures; Debugging; Formal verification; Functional programming; Logic; System testing; Writing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Quality Software, 2003. Proceedings. Third International Conference on
Print_ISBN :
0-7695-2015-4
Type :
conf
DOI :
10.1109/QSIC.2003.1319111
Filename :
1319111
Link To Document :
بازگشت