Article

ProofChecker: an accessible environment for automata theory correctness proofs

Authors:

Matthias F. Stallmann,

Susan D. HighAuthors Info & Claims

ITiCSE '07: Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education

Pages 48 - 52

https://doi.org/10.1145/1268784.1268801

Published: 25 June 2007 Publication History

Get Access

Abstract

ProofChecker is a graphical program based on the notion of formal correctness proofs that allows students, both sighted and visually impaired, to draw a deterministic finite automaton (DFA) and determine whether or not it correctly recognizes a given language. Sighted students use the mouse and graphical controls to draw and manipulate the DFA. Keyboard shortcuts, together with the use of a screen reader to voice the accessible descriptions provided by the program, allow visually impaired students to do the same.

Because the states of a DFA partition thelanguage over its alphabet into equivalence classes, each state has a language associated with it. Conditions that describe the language of each state are entered by the student in the form of conditional expressions with function calls and/or regular expressions. A brute-force approach 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 in a state's language meet the condition for another state. Feedback is provided that either confirms that the DFA correctly meets thegiven conditions or alerts the student to a mismatch between the conditions and the DFA.

A student's DFA can be saved in an XML file and submitted for grading. An automated checking tool, known as ProofGrader, can be used to compare a student's DFA with the correct DFA for a given language, thus greatly speeding up the grading of student assignments.

References

[1]

E. Bergman and E. Johnson. Towards accessible human-computer interaction. Advances in human-computer interaction (vol. 5) pages 87--113, 1995.

Digital Library

Google Scholar

[2]

Accessibility features of svg. Available at http://www.w3.org/TR/SVG-access/.

Google Scholar

[3]

R. F. Cohen, A. V. Fairley, D. Gerry, and G. R. Lima. Accessibility in introductory computer science. In Proc. 36th SIGCSE Tech. Symp. on Computer Science Education pages 17--21, 2005.

Digital Library

Google Scholar

[4]

J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation Addison-Wesley, 1979.

Digital Library

Google Scholar

[5]

Package javax. accessibility. Available at http://java.sun.com/j2se/1.5.0/docs/api/javax/accessibility/package summary.html

Google Scholar

[6]

Jaws ® for Windows ®. Available at http://www.freedomscientific.com/fs_products/software_jaws.asp

Google Scholar

[7]

S. H. Kurniawan and A. G. Sutcliffe. Mental models of blind users in the windows environment. In ICCHP '02: Proceedings of the 8th International Conference on Computers Helping People with Special Needs pages 568--574, London, UK, 2002. Springer-Verlag.

Digital Library

Google Scholar

[8]

H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation Prentice Hall, 1998.

Digital Library

Google Scholar

[9]

J. C. Martin. Introduction to Languages and the Theory of Computation McGraw-Hill, 2003.

Digital Library

Google Scholar

[10]

S. D. Network. Java access bridge. Available at http://java.sun.com/products/accessbridge/.

Google Scholar

[11]

S. H. Rodger, B. Bressler, T. Finley, and S. Reading. Turning automata theory into a hands-on course. In Proc. 37th SIGCSE Tech. Symp. on Computer Science Education pages 379--383, 2006.

Digital Library

Google Scholar

[12]

S. H. Rodger and T. W. Finley. JFLAP: An Interactive Formal Languages and Automata Package Jones and Bartlett, 2006.

Digital Library

Google Scholar

[13]

T. A. Sudkamp. An Introduction to the Theory of Computer Science Languages and Machines Addison-Wesley, 2006.

Digital Library

Google Scholar

[14]

T. M. White and T. P. Way. jFAST: a Java ?nite automata simulator. SIGCSE Bull. 38(1):384--388, 2006.

Digital Library

Google Scholar

Cited By

View all

Crescenzi PRossi LApollaro GSmith King LMusicant DCamp TTymann P(2012)Making turing machines accessible to blind studentsProceedings of the 43rd ACM technical symposium on Computer Science Education10.1145/2157136.2157190(167-172)Online publication date: 29-Feb-2012
https://dl.acm.org/doi/10.1145/2157136.2157190
Bernareggi C(2010)Non-sequential mathematical notations in the LAMBDA systemProceedings of the 12th international conference on Computers helping people with special needs10.5555/1880751.1880818(389-395)Online publication date: 14-Jul-2010
https://dl.acm.org/doi/10.5555/1880751.1880818
D'antoni LKini DAlur RGulwani SViswanathan MHartmann B(2015)How Can Automatic Feedback Help Students Construct Automata?ACM Transactions on Computer-Human Interaction10.1145/272316322:2(1-24)Online publication date: 10-Mar-2015
https://dl.acm.org/doi/10.1145/2723163
Show More Cited By

Index Terms

ProofChecker: an accessible environment for automata theory correctness proofs
1. Theory of computation
  1. Formal languages and automata theory
    1. Grammars and context-free languages

Recommendations

ProofChecker: an accessible environment for automata theory correctness proofs
Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education (ITiCSE'07)

ProofChecker is a graphical program based on the notion of formal correctness proofs that allows students, both sighted and visually impaired, to draw a deterministic finite automaton (DFA) and determine whether or not it correctly recognizes a given ...
Limited Automata and Context-Free Languages
Non-Classical Models of Automata and Applications V

Limited automata are one-tape Turing machines which are allowed to rewrite each tape cell only in the first d visits, for a given constant d. For each d ≥ 2, these devices characterize the class of context-free languages. We investigate the equivalence ...
On the power of quantum finite state automata
FOCS '97: Proceedings of the 38th Annual Symposium on Foundations of Computer Science

In this paper, we introduce 1-way and 2-way quantum finite state automata (1qfa's and 2qfa's), which are the quantum analogues of deterministic, nondeterministic and probabilistic 1-way and 2-way finite state automata. We prove the following facts ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ITiCSE '07: Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education

June 2007

386 pages

ISBN:9781595936103

DOI:10.1145/1268784

General Chair:
Janet Hughes
University of Dundee, UK
,
Program Chairs:
Ramanee Peiris
University of Dundee, UK
,
Paul Tymann
Rochester Institute of Technology

ACM SIGCSE Bulletin Volume 39, Issue 3
Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education (ITiCSE'07)
September 2007
366 pages
ISSN:0097-8418
DOI:10.1145/1269900
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 June 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ITiCSE07

Sponsor:

ITiCSE07: 12th Annual Conference on Innovation and Technology in Computer Science Education

June 25 - 27, 2007

Dundee, Scotland

Acceptance Rates

ITiCSE '07 Paper Acceptance Rate 62 of 210 submissions, 30%;

Overall Acceptance Rate 552 of 1,613 submissions, 34%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
286
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Crescenzi PRossi LApollaro GSmith King LMusicant DCamp TTymann P(2012)Making turing machines accessible to blind studentsProceedings of the 43rd ACM technical symposium on Computer Science Education10.1145/2157136.2157190(167-172)Online publication date: 29-Feb-2012
https://dl.acm.org/doi/10.1145/2157136.2157190
Bernareggi C(2010)Non-sequential mathematical notations in the LAMBDA systemProceedings of the 12th international conference on Computers helping people with special needs10.5555/1880751.1880818(389-395)Online publication date: 14-Jul-2010
https://dl.acm.org/doi/10.5555/1880751.1880818
D'antoni LKini DAlur RGulwani SViswanathan MHartmann B(2015)How Can Automatic Feedback Help Students Construct Automata?ACM Transactions on Computer-Human Interaction10.1145/272316322:2(1-24)Online publication date: 10-Mar-2015
https://dl.acm.org/doi/10.1145/2723163
Balik SMealin SStallmann MRodman RCamp TTymann PDougherty JNagel K(2013)GSKProceeding of the 44th ACM technical symposium on Computer science education10.1145/2445196.2445266(221-226)Online publication date: 6-Mar-2013
https://dl.acm.org/doi/10.1145/2445196.2445266
Howles T(2009)A study of attrition and the use of student learning communities in the computer science introductory programming sequenceComputer Science Education10.1080/0899340090280931219:1(1-13)Online publication date: Mar-2009
https://doi.org/10.1080/08993400902809312

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

ProofChecker: an accessible environment for automata theory correctness proofs

Limited Automata and Context-Free Languages

On the power of quantum finite state automata