ProofChecker: An Accessible Environment for Automata Theory Correctness Proofs
By Stallmann, Matthias; Balik, Suzanne; Rodman, Robert; Bahram, Sina; Grace, Michael; High, Susan; ITiCSE ’07 - Proceedings of the 12th Annual SIGCSE Conference on Innovation and Technology in Computer Science Education,Publication Date: June 23-27, 2007
Review of ProofChecker, a graphical computer program, developed at North Carolina State University and based on the notion of formal correctness proofs that allow students to draw a deterministic finite automaton (DFA) and determine whether it correctly recognizes a given computer language. Keyboard shortcuts, together with the use of a screen reader to voice the accessible descriptions provided by the program, allow visually impaired students to draw and manipulate the DFA. Because the states of a DFA partition the language over its alphabet into equivalence classes, each state has a language associated with it. Conditions describing the language of each state are entered by the student. A brute-force approach, i.e. a computer problem-solving technique of systematically enumerating all possible candidates for the solution, is then used to check that each state’s condition correctly describes all of the strings in its language and that none of the strings meet the conditions for another state. A student’s DFA can be saved in an XML file and submitted for grading. An automated checking tool, ProofGrader, can be used to compare a student’s DFA with the correct DFA for a given language.
Published by: Association for Computing Machinery (Website:http://www.acm.org)
SIGCSE (ACM Special Interest Group on Computer Science Education) (Web Site: http://sigcse.org )
