Published in Volume XXXIV, Issue 1, 2024, pages 39-66, doi: 10.47743/SACS.2024.1.39
Authors: A.-I. Lungu , V. Teodorescu , A. Zaborilă , O. Andrei, D. Lucanu
Abstract
Algorithm design courses are fundamental to computer science curricula, but fostering algorithmic thinking in students is challenging due to the diverse skills and creativity required. Dedicated teaching support tools can help both course instructors and students in this effort. We have developed the Alk platform to promote algorithmic thinking, leveraging the theoretical foundations of Matching Logic. Alk features an intuitive algorithm language that provides a flexible computational model suitable for analysis, symbolic execution, and checking properties of algorithms. In this paper, we present an overview of the Alk platform tool and demonstrate, through use cases, how it fosters various algorithmic thinking skills. We conclude that the Alk platform is a valuable tool for learning and teaching algorithms, effectively enhancing students’ understanding and skills. Future work will extend its capabilities of supporting symbolic execution, probabilistic algorithms, as well as estimation of execution time, further broadening its impact on computer science education.
References
[1] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive Software Verification – The KeY Book – From Theory to Practice, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. doi:10.1007/978-3-319-49812-6.
[2] Sandrine Blazy. Teaching deductive verification in Why3 to undergraduate students. In Brijesh Dongol, Luigia Petre, and Graeme Smith, editors, 3rd International Workshop and Tutorial on Formal Methods Teaching, FMTea 2019, volume 11758, pages 52–66. Springer, 2019. doi:10.1007/978-3-030-32441-4\_4.
[3] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let’s verify this with Why3. International Journal on Software Tools for Technology Transfer, 17(6):709–727, 2015. doi:10.1007/s10009-014-0314-5.
[4] Xiaohong Chen, Dorel Lucanu, and Grigore Roşu. Matching logic explained. Journal of Logical and Algebraic Methods in Programming, 120:100638, 2021. doi:10.1016/j.jlamp.2021.100638.
[5] Xiaohong Chen and Grigore Roşu. Matching µ-logic. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785675.
[6] Xiaohong Chen and Grigore Roşu. Matching mu-logic: Foundation of K framework. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO’19), volume 139 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1–4. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. doi:10.4230/LIPIcs.CALCO.2019.1.
[7] Xiaohong Chen and Grigore Roşu. K – A semantic framework for programming languages and formal analysis. In Jonathan P. Bowen, Zhiming Liu, and Zili Zhang, editors, 5th International School on Engineering Trustworthy Software Systems, volume 12154 of Lecture Notes in Computer Science, pages 122–158. Springer, 2019. doi:10.1007/978-3-030-55089-9\_4.
[8] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, 3rd Edition. MIT Press, 2009. URL: http://mitpress.mit.edu/books/introduction-algorithms.
[9] Patrick Cousot. Principles of Abstract Interpretation. MIT Press, 2021.
[10] Léo Creuse, Claire Dross, Christophe Garion, Jérôme Hugues, and Joffrey Huguet. Teaching deductive verification through Frama-C and SPARK for non computer scientists. In Brijesh Dongol, Luigia Petre, and Graeme Smith, editors, 3rd International Workshop and Tutorial on Formal Methods Teaching, FMTea 2019, volume 11758, pages 23–36. Springer, 2019. doi:10.1007/978-3-030-32441-4\_2.
[11] Paul Denny, James Prather, Brett A. Becker, James Finnie-Ansley, Arto Hellas, Juho Leinonen, Andrew Luxton-Reilly, Brent N. Reeves, Eddie Antonio Santos, and Sami Sarsa. Computing education in the era of generative AI. Commununications of the ACM, 67(2):56–67, 2024. doi:10.1145/3624720.
[12] Jose Divasón and Ana Romero. Using Krakatoa for teaching formal verification of Java programs. In Brijesh Dongol, Luigia Petre, and Graeme Smith, editors, 3rd International Workshop and Tutorial on Formal Methods Teaching, FMTea 2019, volume 11758 of Lecture Notes in Computer Science, pages 37–51. Springer, 2019. doi:10.1007/978-3-030-32441-4\_3.
[13] Marco Eilers and Peter Müller. Nagini: A static verifier for Python. In Hana Chockler and Georg Weissenbacher, editors, 30th International Conference on Computer Aided Verification, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, volume 10981 of Lecture Notes in Computer Science, pages 596–603. Springer, 2018. doi:10.1007/978-3-319-96145-3\_33.
[14] Claire Le Goues, K. Rustan M. Leino, and Michal Moskal. The Boogie verification debugger (tool paper). In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pages 407–414. Springer, 2011. doi:10.1007/978-3-642-24690-6\_28.
[15] Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, and Martin Hentschel. Formal specification with the Java modeling language. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors, Deductive Software Verification – The KeY Book – From Theory to Practice, volume 10001 of Lecture Notes in Computer Science, pages 193–241. Springer, 2016. doi:10.1007/978-3-319-49812-6\_7.
[16] Norbert Hundeshagen and Martin Lange. A proposal for a framework to accompany formal methods learning tools – (short paper). In João F. Ferreira, Alexandra Mendes, and Claudio Menghi, editors, 4th International Workshop and Tutorial on Formal Methods Teaching, FMTea 2021, volume 13122 of Lecture Notes in Computer Science, pages 35–42. Springer, 2021. doi:10.1007/978-3-030-91550-6\_3.
[17] Nikolai Kosmatov and Julien Signoles. Frama-C, A collaborative framework for C code verification: Tutorial synopsis. In Yliès Falcone and César Sánchez, editors, 16th International Conference on Runtime Verification, RV 2016, volume 10012 of Lecture Notes in Computer Science, pages 92–115. Springer, 2016. doi:10.1007/978-3-319-46982-9\_7.
[18] Derrick G. Kourie and Bruce W. Watson. The Correctness-by-Construction Approach to Programming. Springer, 2012. doi:10.1007/978-3-642-27919-5.
[19] Timothy H. Lehmann. Using algorithmic thinking to design algorithms: The case of critical path analysis. The Journal of Mathematical Behavior, 71:101079, 2023. doi:10.1016/j.jmathb.2023.101079.
[20] K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, 16th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348–370. Springer, 2010. doi:10.1007/978-3-642-17511-4\_20.
[21] K. Rustan M. Leino. Program proving using intermediate verification languages (IVLs) like Boogie and Why3. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, 2012 ACM Conference on High Integrity Language Technology, HILT ’12, pages 25–26. ACM, 2012. doi:10.1145/2402676.2402689.
[22] Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, and Grigore Roşu. Generating proof certificates for a language-agnostic deductive program verifier. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):56–84, 2023. doi:10.1145/3586029.
[23] Dorel Lucanu, Vlad Rusu, and Andrei Arusoaie. A generic framework for symbolic execution: A coinductive approach. Journal of Symbolic Computation, 80:125–163, 2017. doi:10.1016/j.jsc.2016.07.012.
[24] Alexandru-Ioan Lungu and Dorel Lucanu. Alk Language reference manual. https://github.com/alk-language/java-semantics/wiki/Reference-Manual. Accessed: October, 2022.
[25] Alexandru-Ioan Lungu and Dorel Lucanu. Alk platform. https://github.com/alk-language/java-semantics. Accessed: June, 2024.
[26] Alexandru-Ioan Lungu and Dorel Lucanu. A matching logic foundation for Alk. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022, volume 13572 of Lecture Notes in Computer Science, pages 290–304. Springer, 2022. doi:10.1007/978-3-031-17715-6\_19.
[27] Alexandru-Ioan Lungu and Dorel Lucanu. Supporting algorithm analysis with symbolic execution in Alk. In Yamine Aı̈t Ameur and Florin Craciun, editors, 16th International Symposium on Theoretical Aspects of Software Engineering, TASE 2022, volume 13299 of Lecture Notes in Computer Science, pages 406–423. Springer, 2022. doi:10.1007/978-3-031-10363-6\_27.
[28] Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Alexander Pretschner, Doron Peled, and Thomas Hutzelmann, editors, Dependable Software Systems Engineering, volume 50 of NATO Science for Peace and Security Series – D: Information and Communication Security, pages 104–125. IOS Press, 2017. doi:10.3233/978-1-61499-810-5-104.
[29] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of program analysis. Springer, 1999. doi:10.1007/978-3-662-03811-6.
[30] Xavier Rival and Kwangkeun Yi. Introduction to static analysis: an abstract interpretation perspective. MIT Press, 2020.
[31] Grigore Roşu. Matching logic. Logical Methods in Computer Science, 13(4), 2017. doi:10.23638/LMCS-13(4:28)2017.
[32] Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Thüm, Derrick G. Kourie, and Bruce W. Watson. Tool support for correctness-by-construction. In Anne Koziolek, Ina Schaefer, and Christoph Seidl, editors, Software Engineering 2021, Fachtagung des GI-Fachbereichs Softwaretechnik, volume P-310 of Lecture Notes in Informatics, pages 93–94. Gesellschaft für Informatik e.V., 2021. doi:10.18420/SE2021\_34.
[33] Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuctă, Brandon M. Moore, Traian-Florin Şerbănuţă, and Grigore Roşu. All-path reachability logic. Logical Methods in Computer Science, 15(2), 2019. doi:10.23638/LMCS-15(2:5)2019.
[34] Vlad Teodorescu, Andrei Zaborilă, and Dorel Lucanu. Alk VS Code extension. https://github.com/Andreizabo/alk-vscode-extension/tree/main. Accessed: October, 2022.
[35] Frédéric Vogels, Bart Jacobs, and Frank Piessens. Featherweight VeriFast. Logical Methods in Computer Science, 11(3), 2015. doi:10.2168/LMCS-11(3:19)2015.
[36] Jeannette M. Wing. Computational thinking. Commununications of the ACM, 49(3):33–35, 2006. doi:10.1145/1118178.1118215.
Bibtex
@article{sacscuza:lucanu2024alk,
title={Alk: A Formal-Methods-based Educational Platform for Enhancing Algorithmic Thinking},
author={A.-I. Lungu , V. Teodorescu , A. Zaborilă , O. Andrei, D. Lucanu},
journal={Scientific Annals of Computer Science},
volume={34},
number={1},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2024},
pages={39-66},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.47743/SACS.2024.1.39}
}