ProofChecker
ProofChecker is a graphical program that allows students, both sighted and visually impaired, to draw a deterministic finite automaton (DFA) and determine whether or not it recognizes a given regular language. Sighted students use the mouse, keyboard, and graphical controls to draw the DFA and access other functionality. Visually impaired students can do the same thing with the help of keyboard shortcuts, the Jaws® for Windows® screen reader and the Java Access Bridge.
ProofChecker relies on the fact that the states of a DFA partition the language over its alphabet into equivalence classes which are themselves languages. Students define the state languages using conditional expressions containing function calls and/or regular expressions, thus creating a part of a "correctness proof" for the DFA. ProofChecker then "checks the proof" alerting the student to errors or success. This is done by generating all strings over the alphabet up to an arbitrary length l and checking that each string meets the condition of the state in which it ends up and that it does not meet the condition of any other state. Using l = n + 2, where n is the number of states, has thus far resulted in only one counter-example in which a student's DFA was deemed correct by ProofChecker, but in fact was not, as detected by the ProofGrader program.
ProofGrader, which may be used for grading purposes, compares a student's DFA to the correct DFA for a given language for equivalence. If the DFA's are not equivalent, short strings that are accepted by the student's DFA and not by the correct DFA and vice-versa are listed. This is helpful for tracking down student errors and assigning partial credit.
More information about ProofChecker and ProofGrader may be found in
ProofChecker: An Accessible Environment for Automata Theory Correctness Proofs, M. Stallmann, S. Balik, R. Rodman, S. Bahram, M. Grace and S. High, in Proc. of 12th ITiCSE Tech. Symp. on Computer Science Education, 2007, pp 48-52.
Talk PPT 2007 Talk PPT 2003 Demo PPT 2007 Demo PPT 2003ProofChecker/ProofGrader 1.1.2 download Documentation for Developers