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

Combining testing and proving in dependent type theory

Peter Dybjer (Institutionen för datavetenskap, Programmeringslogik) ; Haiyan Qiao (Institutionen för datavetenskap, Programmeringslogik) ; Makoto Takeyama (Institutionen för datavetenskap, Programmeringslogik)
Lecture Notes in Computer Science. Proceedings - 16th International Conference on Theorem Proving in Higher Order Logics, Rome, 8-12 September 2003 (0302-9743). Vol. 2758 (2003), p. 188-203.
[Konferensbidrag, refereegranskat]

We extend the proof assistant Agda/Alfa for dependent type theory with a modified version of Claessen and Hughes' tool QuickCheck for random testing of functional programs. In this way we combine testing and proving in one system. Testing is used for debugging programs and specifications before a proof is attempted. Furthermore, we demonstrate by example how testing can be used repeatedly during proof for testing suitable subgoals. Our tool uses testdata generators which are defined inside Agda/Alfa. We can therefore use the type system to prove properties about them, in particular surjectivity stating that all possible test cases can indeed be generated.

Denna post skapades 2006-08-25. Senast ändrad 2013-03-13.
CPL Pubid: 17641


Läs direkt!

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

Institutioner (Chalmers)

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


Annan matematik

Chalmers infrastruktur