A strong foundation in formal methods for software engineering is important in educating novice programmers. Semantic modeling is the necessary foundation for formal methods. The increasing utilization of domain-specific languages (DSL) underscores their importance in practical applications. Therefore, incorporating them into the curriculum of the Semantics of Programming Languages represents a notable departure from the traditional way of teaching the semantics of (mostly) imperative languages. Previously, we developed a practical way to visualize natural semantics calculations for a selected domain-specific language for motion control of a robot in an orthogonal grid. The main goal of this article is to present a tool designed and developed by us, which is intended for interactive visualization of the chosen semantic method and its calculations. In this article, we extend the previous visualization with an extended version of the selected DSL to give a robot a more compact movement by angle (which is multiple of 90 degrees) in the desired direction. In this way, we teach students the basics of formal semantics and how to extend DSL, i.e. to extend syntax by new commands and maximize students' learning eficiency. The findings of this paper would be of interest to educators and students.
To novice computer science students it is significant to comprehend how the program is performed
and what steps are taken. Accordingly, they must grasp the specific steps through which a program is
executed by the machine. The principles based on formal methods guarantee the correctness of the
designed and developed systems [
The structure of this paper is the following: the next section reviews related work. Further, we present the syntax and semantics of the extended robot language (Section 3). Section 4 then presents the application implementation and its graphical user interface. Lastly, Section 5 outlines the conclusion on the presented topic.
Numerous authors implement visual tools designed to aid students in mastering subjects. They employ visualization software or create tools to augment students’ learning experiences, aiming to bridge theoretical concepts with practical applications. This approach fosters a clearer comprehension of the applied procedures and principles taught in the course.
An example of a visualization tool for teaching compilers VCOCO (Visible COmpiler Compiler) is [17]. It depends on COCO/R [18, 19] that is responsible for creating analyzers, and it creates visual representations that can be manipulated by students.
Another use of DSL for robots, Mernik demonstrated in [20]. It shows how diferent language compositions can be realized using LISA and Robot DSL, another research area in Software Language Engineering.
The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms given in [14], and it supports full (first-order) predicate logic on top of a rich basis of types (integers, tuples, records, arrays, sets, recursive types) with corresponding operations. This educational tool includes the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Further, the usage and implementation of RISCAL, a model checker for mathematical theories and algorithms based on a variant of First-order logic within models, is reported in [21]. They reported enhancing education in computer science and mathematics, in particular in academic courses on logic, formal methods, and formal modeling (see [22]).
Tsimbolynets and Perháč present in [6, 11] a tool developed to visualize the translation process of a program written in a simple imperative programming language by structural operational semantics, also known as small-step operational semantics. It is OS-independent; therefore, it is implemented as a web application like our visualization tool.
The paper [12] introduces a language definition tool that utilizes a metamodel specification rather than grammar as the basis of the language definition. Inspired by the Java tool YAJCo, it employs typical object-oriented techniques, defining the metamodel as classes in Python. The parsing process results in a graph of objects, exemplified through a case study involving a basic imperative programming language.
The extended robot control language is a domain-specific language used for describing the movement of a robot in a defined orthogonal two-dimensional system. We note that the first idea about this robot language was presented in [23].
The language of the robot is very simple. It contains commands for controlling the robot’s rotation, and movement, returning to the initial state, skip command, and a pattern for the sequencing of commands. Therefore, the simplest way of defining syntax is using the Backus-Naur Form, for which two syntactic domains (categories) were defined: ∈ Num ∈ Statm — numerals, — statements.
The language of the robot uses concepts used in LOGO or Karel the Robot which makes this language closer to real languages. Then the syntax is as follows:
::= turn left | turn right | forward | forward | reset | skip | ; .
The statements turn left and turn right express a change in an angle of movement by 90 degrees to left or right, respectively. The statements forward and forward express the movement of the robot in a direction that is defined by the angle. Argument specifies the number of steps of the movement. The statement reset represents an instantaneous return to the initial position specified by the user at the beginning. The skip statement is an empty statement, and its role is mostly in proof of semantic equivalence. This syntax is now extended by new commands:
::= . . . turn left | turn right .
These statements change the angle of movement by · 90 degrees in the desired direction.
As semantic domains, we consider here standard numerical sets for naturals with zero (N0) and integers (Z) as given in [14, 24].
Here, the configuration in natural semantics shall be extended. Configuration must express the current position with the direction. Direction is given by an angle of movement in the orthogonal system. We consider the following directions (given as angles in degrees): • 0 represents the up, • 90 represents the right, • 180 represents the down, • 270 represents the left movement direction.
In this model, the robot can turn only by multiples of 90 degrees, and the values of angles we consider as elements of the set Angle = Z. A configuration is an element of the semantic domain defined as follows:
Config= Point ×
Angle.
Then elements of this semantic domain are tuples consisting of a point and actual angle: (, ). The semantic function is then defined as follows
S ′ : Statm → (Config⇀ Config) and the function for every statement is given by
S ′J K(, ) = ︂{ (′, ′), if ⟨, (, )⟩ → (′, ′),
⊥, otherwise.
Here, the tuple ⟨, (, )⟩ is a new configuration in natural semantics for the extended language,
and ⟨, (, )⟩ → (′, ′) is a new transition relation. The semantic rules for statements were defined
in [
) mod 360,
N J K for N J K
= N J K ⊕ 1, where N J K, N J K ∈ N0.
In the case of both commands, we can observe the following equivalences: if ∈ {0, 90, 180, 270}, then ⟨turn left , (, )⟩ ≡ ⟨ skip, (, )⟩, if ∈ {0, 90, 180, 270}, then ⟨turn right , (, )⟩ ≡ ⟨ skip, (, )⟩, where N J K
mod 4 = 0. We note that N J · K is a semantic function that sends numerals to naturals (or zero):
N : Num → N0.
The application Operics for visualizing the operational semantics of robot language is available online at [25]. Next.js framework and the NextUI library were used to design our GUI. The application Operics utilizes the microservices architecture. Visualization logic is split between the frontend, which provides an interface for a user to interact with the application, and the backend, which logic is separated into two modules, one for grammar processing and the other for subsequent interpretation of input and output generation.
The UI component (Figure 1) provides two ways of inputting code: through the text area and file upload. The robot grid (Figure 2) is the interpreter of possible states on the interface. At first, it is initialized with the creation of the whole grid and the robot on it.
The interpretation module simplified controller architecture is shown in Figure 3. The TreeBuilderService creates a derivation tree of the natural semantics in the form of an object Tree. Method applyNaturalSemantics is extended for the rule processing of extended robot control language. Methods of the GeneratorService which is run after TreeBuilderService use a constructed Tree object and generate the desired output format. The extended state of the robot inherits from the basic state of the robot and extends it by the rotation angle. Subsequently, state transitions, natural semantics in the form of LATEXcode, or graphic visualization in the form of a PDF file are generated based on the language version used. The endpoints were extended by adding/alternative postfix to the existing paths creating two new endpoints for extended robot control language.
As an important and (no less) interesting element of controlling the robot, we mention that the user can step the robot’s movement himself, or start automatic stepping (run-at-once) from any point, i.e. from the beginning of the program, and during stepping let the robot catch up to end of the program. After performing the program, user receives a visible output consisting of more information. First of all, the grid with the full path of robot is visualized (this is what the grid component provides, see Figure 2. Formally, the robot is in individual states during its run (its activity) until it reaches the end (result) state. The list of all reached states is provided as another result (Figure 4).
Last but not least, a tree of natural semantics is also provided as a result, in which individual transitional sessions (big steps) are expressed, with the help of which the robot gets from the initial state to the final state. An example of such tree is in Figure 5.
We note that the individual results from the Operics program as presented in Figures 2, 4 and 5 express the solution or the result of the interpretation of the program expressed in Figure 1.
The robot movement is visualized on the robot grid using the react-konva library. The initial state of the robot and the current state of the robot are shown under the grid. Depending on the language version used they are shown either as configuration of points and :
⟨, ⟩ or for an extended version with an angle of rotation
⟨, , ⟩.
The rotation of the robot is shown as an arrow that points to the direction described by the angle of the movement. Calling reset command and moving the robot through the same paths multiple times can be confusing. For that reason when reset command is used the the color of the path is changed enabling thus easier recognition of current and past paths.
In this paper, we focused on the formulation and definition of semantic methods for describing the meaning of programs in a simple domain-specific language for controlling a robot in an orthogonal system with extensions of the angle of movements. We presented a software tool for formulating semantic methods, serving as an educational aid to enhance its appeal. As mentioned in [14] regarding the previous version of this tool, our application also presents opportunities for further development. We also would like to take advantage of the flexibility of this DSL to extend it with loops, to define conditionals, and to introduce some kind of state machine so our DSL for controlling the robot could become closer to real languages.
This work was supported by national KEGA project 030TUKE-4/2023 – “Application of new principles in the education of IT specialists in the field of formal languages and compilers”, granted by the Cultural and Education Grant Agency of the Slovak Ministry of Education. An international cooperation was supported by CEEPUS Network CZ-1503-04-2324 (Umbrella) – “Development of Computational Thinking”. [5] W. Steingartner, V. Novitzká, Metódy formálnej sémantiky programovacích jazykov [Methods of
Formal Semantics of Programming Languages], Technical University of Košice, 2022. (in Slovak). [6] V. Tsimbolynets, J. Perháč, Visualization Tool for Structural Operational Semantics of Simple
Imperative Languages, IPSI Transactions on Internet Research 19 (2023) 66–74. [7] S. Szymoniak, Time Influence on Security Protocol, in: H. K. Raian Ali, L. Maciaszek (Eds.), Proceedings of the 16th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), ScoTePress, 2021, pp. 181–188. [8] W. Schreiner, F.-X. Reichl, Mathematical Model Checking Based on Semantics and SMT, IPSI
Transactions on Internet Research 16 (2020) 4–13. [9] G. Savić, M. Segedinac, M. Čeliković, I. Luković, A Meta-model for Key Performance Indicators in
Higher Education, IPSI Bgd Transactions on Internet Research 19 (2023) 76–91. [10] W. Schreiner, W. Steingartner, Visualizing Logic Formula Evaluation in RISCAL, Technical Report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, 2018. [11] V. Tsimbolynets, J. Perháč, Visualization of imperative programs translation with structural operational semantics, in: 2022 IEEE 16th International Scientific Conference on Informatics (Informatics), 2022, pp. 328–333. doi:10.1109/Informatics57926.2022.10083474. [12] S. Chodarev, S. Ilyas, Metamodel-based language definition with python, IPSI Transactions on
Internet Research 19 (2023) 32–38. [13] D. Mihályi, M. Peniašková, J. Perháč, J. Mihelič, Web-based Questionnaires for Type Theory
Course, Acta Electrotechnica et Informatica 17 (2017) 35–42. [14] W. Steingartner, D. Radaković, R. Zsiga, Some Aspects about Visualization of Natural Semantics for a Selected Domain-Specific Language, IPSI Transactions on Internet Research 19 (2023) 46–54. [15] J. Dostal, X. Wang, W. Steingartner, P. Nuangchalerm, Digital Intelligence – New Concept in Context of Future of School Education, in: L. Chova, A. Martinez, I. Torres (Eds.), 10th International Conference of Education, Research and Innovation (ICERI2017), ICERI Proceedings, 2017, pp. 3706– 3712. 10th Annual International Conference of Education, Research and Innovation (ICERI), Seville, SPAIN, NOV 16-18, 2017. [16] W. Steingartner, V. Novitzká, W. Schreiner, Proof of equivalence of semantic methods for a selected domain-specific language, Journal of Applied Mathematics and Computational Mechanics 23 (2024) 79–92. URL: https://doi.org/10.17512/jamcm.2024.2.07. doi:10.17512/jamcm.2024.2.07. [17] R. D. Resler, M. D. Deaver, VCOCO: A visualisation tool for teaching compilers, in: Annual Conference on Innovation and Technology in Computer Science Education, ser. ITiCSE ’98, 1998, pp. 199–202. [18] H. Mössenböck, The Compiler Generator Coco/R User Manual, Johannes Kepler University Linz,
Institute of System Software, 1990. [19] H. Mössenböck, A generator for production quality compilers, in: D. Hammer (Ed.), Compiler
Compilers, Springer, Berlin, Heidelberg, 1991, pp. 42–55. [20] M. Mernik, An object-oriented approach to language compositions for software language engineering, Journal of Systems and Software 86 (2013) 2451–2464. [21] W. Schreiner, Theorem and algorithm checking for courses on logic and formal methods, in: W. N. Pedro Quaresma (Ed.), Theorem Proving Components for Educational Software (ThEdu’18), volume 290 of EPTCS, Open Publishing Association, 2019, pp. 56–75. [22] W. Schreiner, Logic and semantic technologies for computer science education, in: 2019 IEEE 15th
International Scientific Conference on Informatics, IEEE, 2019, pp. 415–420. [23] M. Pereira, M. Mernik, D. Cruz, P. Rangel Henriques, Program comprehension for domain-specific languages, Comput. Sci. Inf. Syst. 5 (2008) 1–17. doi:10.2298/CSIS0802001P. [24] W. Steingartner, V. Novitzká, Operational semantics in a domain-specific robot control language:
A pedagogical use case, Computer Science and Information Systems 21 (2024) 1077–1095. [25] Operics, Operics: Online tool for natural semantics, n.d. URL: https:// operics-frontend-g7mvk5367q-od.a.run.app/en/natural, accessed: 2024-07-14.