"Proof-Directed Debugging" Revisited

EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version. Kwangkeun Yi. JFP. 16(6):663-670.

Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for developing programs with an article in this journal. Unfortunately, his example uses both higher-order functions and continuation-passing style, which is too difficult for students in an introductory programming course. In this pearl, we present a first-order version of Harper's example and demonstrate that it is easy to transform the final version into an efficient state machine. Our new version convinces students that the approach is useful, even essential, in developing both correct and efficient programs.

The problem is regular expression matching: checking whether a string S belongs to the language specified by the regular expression r.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Less hard-core proofs, but perhaps similar...

The subject makes me recall an old project for regular folks doing programming and debugging.

This is a nice paper!

This is a nice paper!