Problem-solving Systematization: Introducing Formal Methods in Basic Education


Widely employed within critical systems, Formal Methods for specification and verification have gained significance in a world where computer systems continue to expand in scale. Teaching Formal Methods at the higher education level has long been accompanied by well documented challenges. However, since it is often considered an advanced subject within software engineering, it is rarely included in basic education. Targeting this unconventional audience, this paper explores a new approach to formal specification based on the systematization of problem-solving. An example of recursion elimination is presented.

Palavras-chave: Formal Methods, Basic Education, Graph Grammar


Isayama, D., Ishiyama, M., Relator, R., and Yamazaki, K. (2016). Computer Science Education for Primary and Lower Secondary School Students: Teaching the Concept of Automata. ACM Transactions on Computing Education (TOCE), 17(1):1-28.

Kiesmüller, U. (2009). Diagnosing Learners' Problem-solving Strategies Using Learning Environments with Algorithmic Problems in Secondary Eeducation. ACM Transactions on Computing Education (TOCE), 9(3):1-26.

Krath, J., Schurmann, L., and von Korflesch, H. F. (2021). Revealing the Theoretical Basis of Gamification: A Systematic Review and Analysis of Theory in Research on Gamification, Serious Games and Game-based Learning. Computers in Human Behavior, 125:106963.

Reichert, R. (2003). Theory of Computation as a Vehicle for Teaching Fundamental Concepts of Computer Science. PhD thesis, ETH Zurich.

Resnick, M., Maloney, J., Monroy-Hernandez, A., Rusk, N., Eastmond, E., Brennan, K., Millner, A., Rosenbaum, E., Silver, J., Silverman, B., et al. (2009). Scratch: Programming for All. Communications of the ACM, 52(11):60-67.

Roggenbach, M., Cerone, A., Schlingloff, B.-H., Schneider, G., and Shaikh, S. A. (2021). Formal Methods for Software Engineering. Springer.

Rozenberg, G. (1997). Handbook of Graph Grammars and Computing by Graph Transformation, volume 1. World scientific.

Silva Junior, B. A., Cavalheiro, S. A. C., and Foss, L. (2021b). GrameStation: Specifying Games with Graphs. In Anais do XXXII Simpósio Brasileiro de Informática na Educação, pages 499-511, Porto Alegre, RS, Brasil. SBC.

Silva Junior, B. A., Cavalheiro, S. A., and Foss, L. (2021). Theoretical Computer Science in Basic Education: A Systematic Review. In Anais do VI Workshop-Escola de Informática Teórica, pages 133-140. SBC.

Wing, J. M. (2006). Computational Thinking. Communications of the ACM, 49(3):33-35.

Yang, K., Liu, X., and Chen, G. (2020). The Influence of Robots on Students' Computational Thinking: A Literature Review. International Journal of Information and Education Technology, 10(8):627-631.
SILVA, Júlia Veiga da; SILVA JUNIOR, Braz Araujo da; FOSS, Luciana; CAVALHEIRO, Simone André da Costa. Problem-solving Systematization: Introducing Formal Methods in Basic Education. In: WORKSHOP-ESCOLA DE INFORMÁTICA TEÓRICA (WEIT), 7. , 2023, Rio Grande/RS. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 71-78. DOI: