Computers cause an impact in almost every single aspect of our lives, however, unfortunately, schools have not been able to keep up with this irreversible evolution. The simple use of technological apparatuses in the classroom does not guarantee the improvement of the learning process, however it can be the medium through which the students find the alternatives for the solution of complex problems. The Computational Thinking is an approach of teaching that uses a diverse range of techniques derived from computers for the resolution of these problems combined with the new competencies of the 21st century (critical thinking, collaboration, etc.). The adoption of the notion of Computing within the basic education schools is a concern in many countries, where the implementation occurs in a strict way. Admittedly, it grows the idea that the Computing discipline is very distinct from the computer classes and that the use of skills from Computing possesses educational (reflection and problem solving, the comprehension that the world is ingrained with the digital technology) and economic (high demand of professionals with good training) benefits. This article, through the vast bibliographic review, describes an international landscape of countries of all Americas, in order to contextualize the reader in respect to the adoption of Computational Thinking within the basic education schools.
Keywords: Companies;Computers;Economics;Electronic mail;Problem-solving;Training;Basic Education;Computational Thinking;Computing at Schools
The verification of safety requirements becomes crucial in critical systems where human lives depend on their correct functioning. Formal methods have often been advocated as necessary to ensure the reliability of software systems, albeit with a considerable effort. In any case, such an effort is cost-effective when verifying safety-critical systems. Often, safety requirements are expressed using safety contracts, in terms of assumptions and guarantees.To facilitate the adoption of formal methods in the safety-critical software industry, we propose a methodology based on well-known modelling languages such as the unified modelling language and object constraint language. The unified modelling language is used to model the software system while object constraint language is used to express the system safety contracts within the unified modelling language. In the proposed methodology a unified modelling language model enriched with object constraint language constraints is transformed to a Petri net model that enables us to formally verify such safety contracts. The methodology is evaluated on an industrial case study. The proposed approach allows an early safety verification to be performed, which increases the confidence of software engineers while designing the system.
Abstract Dynamic slicing is a technique to extract the part of the program (called slice) that influences or is influenced, in a particular execution, by a given point of interest in the source code (called slicing criterion). Since a single execution is considered, the technique often uses a trace of this execution to analyze data and control dependencies. In this work we present the first formulation and implementation of dynamic slicing in the context of CSP. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. We base our technique on a new data structure to represent {CSP} computations called track. A track is a data structure which represents the sequence of expressions that have been evaluated during the computation, and moreover, it is labeled with the location of these expressions in the specification. The implementation of a dynamic slicer for {CSP} is useful for debugging, program comprehension, and program specialization, and it is also interesting from a theoretical perspective because {CSP} introduces difficulties such as heavy concurrency and non-determinism, synchronizations, frequent absence of data dependence, etc.
Keywords: Concurrent programming, CSP, Slicing
In the lambda calculus a term is solvable iff it is operationally relevant. Solvable terms are a superset of the terms that convert to a final result called normal form. Unsolvable terms are operationally irrelevant and can be equated without loss of consistency. There is a definition of solvability for the lambda-value calculus, called v-solvability, but it is not synonymous with operational relevance, some lambda-value normal forms are unsolvable, and unsolvables cannot be consistently equated. We provide a definition of solvability for the lambda-value calculus that does capture operational relevance and such that a consistent proof-theory can be constructed where unsolvables are equated attending to the number of arguments they take (their `order' in the jargon). The intuition is that in lambda-value the different sequentialisations of a computation can be distinguished operationally. We prove a version of the Genericity Lemma stating that unsolvable terms are generic and can be replaced by arbitrary terms of equal or greater order.
This file was generated by bibtex2html 1.98.