Formal Methods (FMs) radically improve the quality of the code artefacts they help to produce. They are simple, probably accessible to first-year undergraduate students and certainly to second-year students and beyond. Nevertheless, in many cases, they are not part of a general recommendation for course curricula, i.e., they are not taught — and yet they are valuable. One reason for this is that teaching “Formal Methods” is often confused with teaching logic and theory. This article advocates what we call FM thinking : the application of ideas from Formal Methods applied in informal, lightweight, practical and accessible ways. We will argue here that FM thinking should be part of the recommended curriculum for every Computer Science student, for even students who train only in that “thinking” will become much better programmers. However, there will be others who, exposed to those ideas, will be ideally positioned to go further into the more theoretical background: why the techniques work, how they can be automated, and how new ones can be developed. Those students would follow subsequently a specialised, more theoretical stream, including topics such as semantics, logics, verification and proof-automation techniques.

In the last decade many countries have introduced Computing in school curricula, most including at least basic concepts as mandatory topics. In 2017/2018 a new National Standard for School Curricula was approved in Brazil, but Computing foundations were not included. In 2022 the Brazilian National Education Council approved an appendix to the standard containing guidelines regarding Computing which define abilities that must be developed in all schools in Brazil from pre-school to high school. These guidelines were ratified by the Brazilian Ministry of Education and implementation should start in 2023. The aim of this paper is to provide an overview and analysis of these approved guidelines for Computing in schools in Brazil, as well as a comparison with standards from other countries.

Motivation : Enrollments in Brazilian computing degrees are at an all-time high, but graduation numbers have not increased at the same rate. Moreover, enrollment growth has mainly attracted male students, steadily expanding the gender gap in Brazilian computing programs. Such high attrition rates have a great economic impact and may disproportionately affect women and students of color. Previous works investigated reasons for student drop-out and retention in specific courses or barriers to entrance in computing programs in narrower contexts or in a single institution. Objectives : We investigate potential actionable factors for intent to drop out in computing programs and what factors might lead students to remain in a computing program in several Brazilian institutions. We investigated how such factors may be affected by students’ race/ethnicity, gender, and socioeconomic status. Method : We analyzed Likert-style answers from an online survey with 3,193 students currently enrolled in Brazilian computing programs. Results : The results show that students value salary/job-related factors as the most important factors to potentially remain in a computing program. The excess of theoretical courses and the difficulty of programming and mathematics courses are the top-ranked factors by students to potentially abandon a computing degree. However, while there is little effect of gender, race/ethnicity, or socioeconomic status in retention factors, potential drop out factors such as a the fact that it is a male-dominated field, harassment, and the difficulty of courses were rated as more important by women. Also, costs and the difficulty of courses are relevant factors for the intent to drop out when analyzing students’ race/ethnicity and socioeconomic status. Discussion : We explore the implications of our findings for Computing programs, particularly (but not restricted to) the Brazilian context. We conjecture reasons for such students’ perspectives regarding intent to drop out and retention factors and provide recommendations of actions for instructional designers, curriculum developers, and other key stakeholders to address issues related to gender, students’ wellness, perceived authenticity of courses, and other relevant factors. Since we only observed small interactions between race/ethnicity and retention and intent to drop out factors, which may indicate a lack of sensitivity from the instrument, we present suggestions to address such limitations in future work.

The concept of algebraic high-level net transformation systems combines two important lines of research recently introduced in the literature:algebraic high-level nets(AHL-nets for short) andhigh-level replacement systems(HLR-systems for short). In both cases a categorical formulation of the corresponding theory has turned out to be highly important and is also a good basis for the integration of these concepts in this paper. AHL-nets combine Petri nets with algebraic specifications and provide a powerful specification technique for distributed systems including data types and processes. HLR-systems are transformation systems for high-level structures such as graphs, hypergraphs, algebraic specifications and different kinds of Petri nets. The theory of HLRsystems - formulated already in a categorical framework - is applied in this paper to AHLnets. Thus we obtain AHL-net transformation systems as an instantiation of HLR-systems to AHL-nets. This allows us to build up AHL-nets from basic components and to transform the net structure using rules or productions in the sense of graph grammars. This concept is illustrated by extending the well-known example of ‘dining philosophers’. We are able to show that AHL-net-transformation systems satisfy several important compatibility properties. On the one hand we obtain a local Church-Rosser and Parallelism Theorem, which is well-known for graph grammars and has recently been generalized to HLR-systems. This allows us to analyse concurrency in AHL-nets not only on the token level but also on the level of transformations of the net structure. On the other hand, we consider the ‘fusion’ and ‘union’ constructions for high-level structures, motivated by corresponding concepts for high-level Petri nets in the literature, and we show compatibility of these constructions with derivations of HLR-systems in general and AHL-nettransformations in particular. This means compatibility of vertical and horizontal structuring in terms of software development.