Abstract
Gamification has been growing at a meteoric rate. Such growth is because this is a valid mechanism to add desirable behaviors in an organizational process or even in an educational process. In fact, these are the two major contexts where gamification has been applied. In organizations, gamification is applied in various business contexts from recruitment, through onboarding, training, talent retention, customer service, sales, and marketing. In education, gamification is used essentially in contexts of promoting student involvement in existing training offers. This chapter presents a gamification design framework called GAFRHE aimed to be used in all domains, but with extensive facets for the healthcare domain. Unlike other frameworks, it is a concrete framework that not only presents the basic concepts that must be followed by the gamified strategy, but also presents a system architecture that must be instantiated, and a set of components already coded and that can be used. The framework is mostly based on existing standards promoting reusability and interoperability.

Abstract
Learning programming boils down to the practice of solving exercises. However, although there are good and diversified exercises, these are held in proprietary systems hindering their interoperability. This article presents a simple scraping tool, called ScraPE, which through a navigation, interaction and data extraction script, materialized in a domain-specific language, allows extracting the data necessary from Web pages – typically online judges – to compose programming exercises in a standard language. The tool is validated by extracting exercises from a specific online judge. This tool is part of a larger project where the main objective is to provide programming exercises through a simple GraphQL API. © Ricardo Queirós.

Abstract
Computer science is a skill that will continue to be in high demand in the foreseeable future. Despite this trend, automated assessment in computer science is often hampered by the lack of systems supporting a wide range of topics. While there is a number of open software systems and programming exercise collections supporting automated assessment, up to this date, there are few systems that offer a diversity of exercises ranging from computer programming exercises to markup and databases languages. At the same time, most of the best-of-breed solutions force teachers and students to alternate between the Learning Management System - a pivotal piece of the e-learning ecosystem - and the tool providing the exercises. This issue is addressed by JuezLTI, an international project whose goal is to create an innovative tool to allow the automatic assessment of exercises in a wide range of computer science topics. These topics include different languages used in computer science for programming, markup, and database management. JuezLTI borrows part of its name from the IMS Learning Tools Interoperability (IMS LTI) standard. With this standard, the tool will interoperate with reference systems such as Moodle, Sakai, Canvas, or Blackboard, among many others. Another contribution of JuezLTI will be a pool of exercises. Interoperability and content are expected to foster the adoption of JuezLTI by many institutions. This paper presents the JuezLTI project, its architecture, and its main components. © Carrillo, Juan V.; Sierra, Alberto; Leal, Jose Paulo; Queirs, Ricardo; Pellicer, Salvador; Primo, Marco; licensed under Creative Commons License CC-BY 4.0

Abstract
Alloy is a popular language and tool for formal software design. A key factor to this popularity is its relational logic, an elegant specification language with a minimal syntax and semantics. However, many software problems nowadays involve both structural and quantitative requirements, and Alloy's relational logic is not well suited to reason about the latter. This paper introduces QAlloy, an extension of Alloy with quantitative relations that add integer quantities to associations between domain elements. Having integers internalised in relations, instead of being explicit domain elements like in standard Alloy, allows quantitative requirements to be specified in QAlloy with a similar elegance to structural requirements, with the side-effect of providing basic dimensional analysis support via the type system. The QAlloy Analyzer also implements an SMT-based engine that enables quantities to be unbounded, thus avoiding many problems that may arise with the current bounded integer semantics of Alloy.

Abstract

Abstract
Often referred to as ‘the mathematics of dynamical, state-based systems’, Coalgebra claims to provide a compositional and uniform framework to specify, analyse and reason about state and behaviour in computing. This paper addresses this claim by discussing why Coalgebra matters for the design of models and logics for computational phenomena. To a great extent, in this domain one is interested in properties that are preserved along the system’s evolution, the so-called ‘business rules’ or system’s invariants, as well as in liveness requirements, stating that e.g. some desirable outcome will be eventually produced. Both classes are examples of modal assertions, i.e. properties that are to be interpreted across a transition system capturing the system’s dynamics. The relevance of modal reasoning in computing is witnessed by the fact that most university syllabi in the area include some incursion into modal logic, in particular in its temporal variants. The novelty is that, as it happens with the notions of transition, behaviour, or observational equivalence, modalities in Coalgebra acquire a shape. That is, they become parametric on whatever type of behaviour, and corresponding coinduction scheme, seems appropriate for addressing the problem at hand. In this context, the paper revisits Coalgebra from a computational perspective, focussing on three topics central to software design: how systems are modelled, how models are composed, and finally, how properties of their behaviours can be expressed and verified. © 2022, College Publications. All rights reserved.