Mining hints for fixing formal specifications

Universidade do Minho School of Engineering Henrique Gabriel dos Santos Neto Mining hints for fixing formal specifications October, 2023 Universidade do Minho School of Engineering Henrique Gabriel dos Santos Neto Mining hints for fixing formal specifications Master Thesis Master in Informatics Engineering Work developed under the supervision of: Manuel Alcino Pereira Cunha Nuno Filipe Moreira Macedo October, 2023 COPYRIGHT AND TERMS OF USE OF THIS WORK BY A THIRD PARTY This is academic work that can be used by third parties as long as internationally accepted rules and good practices regarding copyright and related rights are respected. Accordingly, this work may be used under the license provided below. If the user needs permission to make use of the work under conditions not provided for in the indicated licensing, they should contact the author through the RepositoriUM of Universidade do Minho. License granted to the users of this work Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International CC BY-NC-SA 4.0 https://creativecommons.org/licenses/by-nc-sa/4.0/deed.en ii Acknowledgements First and foremost, I would like to extend my heartfelt thanks to my advisors, Professor Manuel Alcino Cunha and Professor Nuno Moreira Macedo. Their expertise, patience, and unwavering support have been instrumental in shaping this work. Special thanks are also due to INESC TEC - Institute for Systems and Computer Engineering, Technology and Science, for granting me the scholarship that enabled me to pursue my studies. The financial support has been crucial in ensuring the successful completion of this thesis. Lastly, I would like to extend my sincere thanks to my family, friends and colleagues who have provided moral support and shared their valuable insights. This work is financed by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project EXPL/CCI-COM/1637/2021. iii STATEMENT OF INTEGRITY I hereby declare having conducted this academic work with integrity. I confirm that I have not used plagiarism or any form of undue use of information or falsification of results along the process leading to its elaboration. I further declare that I have fully acknowledged the Code of Ethical Conduct of the Universidade do Minho. Braga January 4, 2024 , (Place) (Date) (Henrique Gabriel dos Santos Neto) iv Assinado por: HENRIQUE GABRIEL DOS SANTOS NETO Num. de Identificação: 30302655 Data: 2024.01.04 18:11:46+00'00' “Simplicity is prerequisite for reliability.” (Edsger Dijkstra) v Resumo Mineração de sugestões para corrigir especificações formais O crescimento da complexidade de aplicações informáticas tornou falhas e erros de software uma inevitabilidade. Para ajudar a garantir que uma aplicação funciona como previsto, profissionais recorrem a modelos de software para detetar e corrigir problemas nas fases iniciais de desenvolvimento. Especificações formais são modelos de software que permitem a desenvolvedores especificar rigorosamente estruturas e comportamentos de software. Infelizmente, a sua complexidade inerente também pode impor problemas nos principiantes que as tentam aprender. Uma maneira possível de abordar este problema seria o emprego de práticas de reparação de especificações e geração automática de sugestões para ajudar os alunos a corrigir tentativas erradas. Alloy4Fun é uma plataforma online para a aprendizagem de Alloy, uma linguagem de especificação formal com capacidades de analise automática. Alloy4Fun permite a instrutores criar e partilhar desafios de especificação formal com avaliação automática. Recentemente, uma técnica de geração automática de sugestões for desenvolvida para esta plataforma, mas provou ser insatisfatória devido ao seu fraco desempenho. O objetivo desta tese foi explorar outras técnicas para geração de sugestões, nomeadamente técnicas de geração de sugestões baseadas em dados, que poderiam usar o conjunto de dados publico de submissões históricas de estudantes do Aloy4Fun para fornecer dicas de forma mais eficiente. O principal resultado desta tese, SpecAssistant, é um novo sistema de geração de dicas baseado em dados para Alloy. Este extrai informação do conjunto de dados do Alloy4Fun para construir grafos de submissões, dos quais são extraídas sugestões a partir de regras personalizadas pelos desenvolvedores de cada desafio. Para avaliar o SpecAssistant, realizamos uma série de experiências quantitativas, com o objetivo de avaliar a disponibilidade e o desempenho do nosso sistema. As nossas descobertas demostram que o SpecAssistant consegue fornecer dicas para uma porção significativa de submissões, apresentado um desempenho que supera o sistema de sugestões precedente. Palavras-chave: Alloy, Geração de Dicas Automáticas, Métodos Formais, Mineração de Dados vi Abstract Mining hints for fixing formal specifications The increasing complexity of software applications has made software bugs and errors an inevitability. To help ensure that software functions as intended, professionals rely on software models to detect and correct faults early in the development process. Formal specifications are software models that allow developers to precisely specify software structures and behaviors. Unfortunately, their inherent complexity can also pose problems to newcomers while learning them. One possible way to address this issue could be to employ automated hint and specification repair techniques to help students fix incorrect attempts. Alloy4Fun is an online platform for learning Alloy, a formal specification language with automated analysis features. Alloy4Fun allows educators to create and share specification challenges with automated assessment. Recently, a hint generation technique based on automated repair has been developed for this platform, but proved unsatisfactory due to its poor performance. The goal of this thesis was to explore other techniques for hint generation, namely data-driven hint generation techniques which could leverage the Alloy4Fun public data-set of past student submissions to provide hints more efficiently. The main outcome of this thesis, SpecAssistant, is a new data-driven hint generation system for Alloy. It mines the Alloy4Fun data-set to build submission graphs, from which hints are extracted using policy rules customized by the challenge developers. To evaluate SpecAssistant we performed a series of quantitative experiments, with the goal of assessing our system’s availability and performance. Our findings show that SpecAssistant can provide hints for a significant portion of invalid submissions with a performance that greatly surpasses that of the previous hint system. Keywords: Alloy, Automated Hint Generation, Data Mining, Formal Methods vii List of Algorithms 1 Policy Algorithm .................................. 50 xiv List of Listings 2.1 First model .................................... 5 2.2 The not self adjacent constraint specified in different styles ............. 7 2.3 Bidirectional adjacent constraint .......................... 7 2.4 Connected roads constraint ............................ 7 2.5 Road constraints ................................. 8 2.6 Road subtypes .................................. 8 2.7 Road type constraints ............................... 9 2.8 Vehicle specification ............................... 9 2.9 Circuit constraints ................................ 11 2.10 Empty run .................................... 12 2.11 Declaration of the variable location ........................ 17 2.12 Initial state fact .................................. 17 2.13 Move event .................................... 18 2.14 Stutter event ................................... 18 2.15 Traces fact .................................... 19 2.16 Liveness constraints ............................... 20 2.17 Bus safety .................................... 21 2.18 Car safety .................................... 22 2.19 Bus Liveness ................................... 22 2.20 Car Liveness ................................... 22 3.1 Constraint challenge 1 .............................. 28 3.2 Command of inv3 ................................ 28 5.1 Syntactical equivalence example .......................... 46 5.2 Semantic equivalence example .......................... 46 5.3 Examples of normalized quantifier formulas .................... 47 5.4 InstanceResponse facade ............................. 56 5.5 Normalizer facade ................................ 59 xv 5.6 Policy rule as a JSON object ............................ 64 5.7 Challenge repository ............................... 66 xvi Acronyms APTED All Path Tree Edit Distance (pp. 60,62) AST Abstract Syntax Tree (pp. xi,37,45–48,53,54,58,60–62,76) BFS Breadth-First Search (p. 62) BSON Binary Javascript Object Notation (p. 66) CRUD Create, Read, Update, Delete (pp. 57,65) DTO Data Transfer Object (pp. 56,57) HINTS Hint Iteration by Narrow-down and Transformation Steps (pp. 34–36) HTTP Hypertext Transfer Protocol (pp. xiii,29,30,55,56) ITAP Intelligent Teaching Assistant for Programming (pp. xi,40,41) JSON JavaScript Object Notation (pp. 29,31,56,63,64) MDP Markov Decision Process (p. 39) REST Representational State Transfer (pp. 29,54–57) RNN Recurrent Neural Network (p. 42) SAT Boolean Satisfiability Problem (pp. 46,72) TAR Temporal Alloy Repair (pp. xiii,36,37,51–53,69,73–75) TED Tree Edit Distance (pp. 49,51,62,63) xvii xviii 1 Introduction In the past decades there has been a rush in software growth as the world becomes more and more digitized. Applications are also becoming increasingly more complex. As complexity increases, bugs and errors become an inevitable problem. If not properly identified and solved, these errors can cause failures in the applications, which can be problematic and result in damages that vary according to the system in question. An error on a web-page will cause an inconvenience to a user attempting to use it. An error in a hospital’s equipment could cost someone’s life. Assuring that an application works as expected is essential in software development and has become a very important subject in computer science. 1.1 Contextualization The core of software development is the design of abstractions [17]. An abstraction is a model of the product itself, only a simple and pure representation of the structure and the core ideas, which are conceived before production. The quality of such abstractions is one of the major factors in the quality of the final product. A good abstraction will normally cause a natural flow in the software’s development, from its design to its production, resulting in simple and optimal components that can easily be modified or expanded without the need for extensive reorganization or changes. On the other hand, bad software abstractions tend to cause major problems in the production phase, where components will become clumsy and burdensome as they are forced to accommodate for unexpected problems, and even the simplest changes become problematic resulting in enormous development costs. In this case, the final product is usually composed of extremely complex components, that require developers to master a mass of superfluous details, while either developing workarounds or accepting the frequent and inexplicable failures. Abstractions are also important to the developers themselves, since they want simple and easy to understand models that don not compromise on factors such as robustness and scalability. With this in mind it is expected that with careful consideration of the problem and its future endeavors one could easily develop a fine product. Unfortunately, this is rarely the case due to a problem commonly referred as wishful thinking [30]. Developers come up with simple and robust abstractions which turn out to be incoherent and possibly inconsistent in production, resulting in the sort of nasty problems previously 1 CHAPTER 1. INTRODUCTION mentioned. These flaws are not directly derived from the developed abstractions, but from the environment imposed by programming, where compilers and tools admit no vagueness whatsoever and tests instantly revel errors and faults. There are several ways of combating this issue, the most interesting and effective ones rely on formal specifications . These abstractions are built using unambiguous notations based on mathematics, which enable automated verification and validation. Over the last few decades there have been several developments is this regard, resulting in the appearance of several advanced tools for developing formal specifications. One of these tools is Alloy [17], which is the main focus of this work. 1.2 Problem Even with their overwhelmingly advantages in software development, formal specifications are still not used by a significant portion of developers. This is because newcomers tend to have several difficulties in understanding and adopting the mathematical techniques and the inherent level of precision and rigor. Even with the most recent state-of-the-art tools, where these concepts keep getting simpler an simpler, this problem still endures. Alloy is a clear example of this issue. It relies on first-order logic extended with a few relational operators, and has a straightforward and minimal syntax and semantics. However a significant number of college students still found themselves confounded when using it [23]. A big part of this issue was the poor feedback of the Alloy tools, as the provided counter-examples were difficult to understand by the users. A possible and feasible way of mitigating this would be the introduction of automatic repair and hint generation techniques in these tools, to help newcomers learn the language. 1.3 Objective Automatic program repair and hint generation are very prominent and active topics in software engineering [44,27]. Currently, Alloy4Fun [23] is one of the few automated assessment platforms for learning formal specifications, and thanks to its support for specification challenges with autograding it has been used as learning platform for Alloy in graduate courses for a few years. Recently, this application has been the target of the development of a hint system based on automatic program repair techniques [10]. However, the developed system presents some shortcomings: besides its performance issues, it usually fails to provide hints on submissions which deviate a lot from a valid solution. Based on the success of recent data-driven hint generation systems on educational programming platforms [36,38], it became apparent that the existing data-set of submissions of Alloy4Fun [22] could be used to significantly upgrade its current hint generation mechanism, allowing not only to speed up the whole generation process but also to increase its availability. 2 1.4. ALLOY SPECIFICATION ASSISTANT The main objective of this dissertation is to explore several of the most recent and useful hint generation techniques for learning how to program [26], and develop a new technique for Alloy specifications. To guarantee the quality of experience of the user, the new technique should have some minimum performance requirements, i.e. the system should present the hints nearly instantly after reading the user’s current submission, otherwise it will most likely fall into disuse. The new technique should also be datadriven, i.e. a technique which will mine existent student submissions to isolate patterns and solution tactics. The reasoning behind this selection is that, by using the historical data from a diverse group of students, we expect the resulting technique to be able to provide hints for most of the erroneous submissions of new students, since they usually fall into the same erroneous patterns. Additionally, we expect an improved performance, since upon being prompted by a student for help, the system would only need to consult the stored information to produce a hint. The information required to start and maintain this system will originate from the historical data of Alloy4Fun [22] and also the new submissions that the system to be developed will receive overtime. 1.4 Alloy Specification Assistant The technique developed in this dissertation resulted in a tool named SpecAssistant, a hint generation system for Alloy which can be integrated within Alloy4Fun. It achieves its purpose by mining a vast repository of submissions obtained from multiple attempts at solving a few Alloy4Fun exercises. This data is organized into a submission graph, akin to a directed graph, from which hints can be computed. After creating the submission graph, our system allows the developer of a new challenge to customize the policy used to compute the hints. This customization is accomplished by defining value ranking rules based on pre-computed attributes of the submission graph. When SpecAssistant is presented with a user’s submission it attempts to match it to the historical submission graph. If a match is successful, it retrieves a submission that would make the user get closer to a solution, based on a customizable policy. Finally, using a simple text generation and code highlighting technique, the gathered information is transformed into a hint. We performed several benchmarks to evaluate our system, and we were able to confirm that the developed hint generation technique is capable of instantly providing hints for a significant amount of invalid submissions. As a result, our system may help students learn Alloy without the efficiency issues of the previously implemented hint system of Alloy4Fun [10]. Furthermore, there is an expectation that our system will enhance its performance over time, as the Alloy4Fun data-set of historical submissions grows. 1.5 Document Structure This thesis has the following structure. 3 CHAPTER 1. INTRODUCTION Chapter 2describes version 6 of the Alloy modeling language. The chapter presents an illustrative model which is used to describe every essential concept of the language, such as its static and dynamic modeling features. Chapter 3presents Alloy4Fun, the target application of this project. This chapter mainly explores this application’s features and architecture, alongside the structure of its database. Chapter 4explores the state-of-the-art in automated hint and repair systems. It begins by presenting an abstract framework which details the common concepts and processes of most hint generation systems. Afterwards, it explores and details several different hint generation techniques, discussing their features, advantages and disadvantages, and how they could be used in our system. Chapter 5describes the developed hint generation system, named SpecAssistant. The chapter starts by describing the fundamental principles and techniques within our system. Subsequently, we describe the implementation of these techniques in Alloy4Fun. Chapter 6presents the evaluation preformed on SpecAssistant. A series of data-mining validation techniques were used to answer a series of research questions, with the main purpose of quantifying our system’s availability and performance. Chapter 7presents some conclusions and perspectives on future work. 4 2 Alloy Alloy [17] is a popular formal specification language complemented by an analyzer capable of automated instance generation and validation. Just like any formal specification tool, it helps developers find issues and holes in their systems. Its biggest advantage over its competitors is the analyzer. Unlike most tools which require conventional analysis based on theorem proving (i.e. mathematical proofs), Alloy provides fully automatic analysis on its models which give instant feedback to the developers. This comes at a cost of not having a “complete” analysis, since it only examines a finite number of cases. However, thanks to its optimizations, the space of cases examined for each model can be immense, which makes this less of an issue. This chapter offers a presentation of Alloy’s essential and unique features, as well a basic understanding of model specification. 2.1 Static Modeling 2.1.1 A Basic Model Structural (or static) models form the basis for any formal specification. These define the structure as well as the rules which the respective instances should satisfy. To demonstrate Alloy’s structural modeling capabilities we have built a simple but descriptive example of a basic traffic system, composed of both a road network and the vehicles which traverse it. To begin, we will first model the roads of our network using two basic constructs: signatures and binary relations. The respective Alloy declarations are presented in Listing 2.1. sig Road { adjacent :set Road } Listing 2.1: First model 5 CHAPTER 2. ALLOY a simple empty run block. These blocks have a similar syntax to the fact block, allowing the user to optionally name them and also specify additional constraints for it to consider during instance generation. These constraints are not part of the model like facts, but simply allow for a more fine search within the generated instances. Our first run block, named Empty, is presented in Listing 2.10. run Empty {} Listing 2.10: Empty run 2.2.2 Visualization Types To visualize the generated instances we simply have to execute the specified command. This can be done through the button Execute on the editor or though the program’s execution context menu. If all the constraints are consistent, Alloy will present an instance which when accessed will launch a new window within the analyzer with its depiction. The first instance for our model is presented in Figure 1. Figure 1: Default visualization of an instance of the static model As we can see, by default the analyzer will display the instance as a graph while providing simple variations on the relations colors. This is not however the only type of instance visualization. The first four buttons off the window offer different styles of presenting the model. Viz corresponds to the default graph representation already presented, Txt lists each set and their atoms in a plain textual format, Table pretty prints each set as a table, and finally Tree displays an instance as an horizontal hierarchy based fork tree. These three options of visualization are presented in Figure 2. The most interesting view and the one that we will be using from now on is the graphical view. 12 2.2. STRUCTURAL MODEL ANALYSIS (a) Text View (b) Table View (c) Tree View Figure 2: Other visualization options 13 CHAPTER 2. ALLOY 2.2.3 Themes Themes are an essential part of the graphical view. They allow for the user to specify not only the shapes and color of atoms and relations, but most importantly the form in which these are represented, i.e. whether these should be present as atom attributes, as nodes of the graph, or if they are not relevant to be displayed at all. The default theme, presented in Figure 1displays all available information, where every atom is presented as a yellow rectangle and every relation as a different colored arc between its atoms. Some sub-signatures may be also displayed as attributes depending on their context. This is usually sufficient in small instances, however as these grow this style can become extremely difficult to understand. Besides the default, regarding Alloy generated themes there is also the magic layout . This functionally that can be called with the button labeled Magic Layout, and proceeds to assign different shapes and colors to the atoms, which can mitigate a few of the problems of the default layout. However, the resulting visualization can still be very difficult to understand. To exemplify this, we will execute the block run OneBus {one Bus} which will force the instance to contain a single bus. The resulting instance after applying the Magic Layout is presented in Figure 3. Figure 3: Magic layout example From this example we can observe that Alloy’s automatic themes do not provide much help in easing the instance’s comprehension, more precisely regarding the circuit relation, which can barely be distinguished from the area relation and requires us to search for the scattered labels in order to piece it together. If we were to add a second bus it would become even worse, as in addition to finding the labels we would also need to match them to the correct vehicle. The best way to visualize complex instances is to define a personalized theme. To do this, we must use the Theme button which will in return display a menu allowing us to customize the visualization. On this menu, our signatures and types will be displayed in a hierarchical form which corresponds to how they where defined in our model. As a result, in addition to the precise tuning of our signatures, changes regarding multiple extensions of the same signature can be defined solely within their parent signature. For example, if we choose to see all atoms corresponding 14 2.2. STRUCTURAL MODEL ANALYSIS to roads as hexagons, we simply need to change our Road signature’s shape, which will then cause all road types to inherit said change. Beyond both types and sets, the most relevant customization options concern relations, and the user can specify these to be either hidden or represented with arcs or atom attributes. An example of the theme customizer is presented in Figure 4. Figure 4: Theme customizer Since themes are burdensome to setup, Alloy allows for them to be saved as .thm files, which can later be loaded to visualize an instance. This not only prevents the user from wasting time on redefining themes, but also provides it with the ability to hot-swap between them and thus providing multiple perspectives on the same instance. Our personalized theme will display vehicles as different colored boxes and roads as different colored Hexagons. Additionally, both area and circuit will be hidden since their comprehension will be difficult with either arcs or attributes. Instead, we will rely on the evaluator to analyze these relations. 2.2.4 Evaluator The evaluator is a console like interpreter which allows the user to evaluate arbitrary expressions regarding the model. Although it is very useful for a precise analysis, it does not provide full access to the language, for example it is not possible to define new facts. Its utilities include listing the values of sets and evaluating predicate expressions. For our instances, we will mostly use it to consult the values for the buses areas and circuits. Exemplifying, asking for the circuit of the bus in the instance of Figure 3and Figure 4can be done with the expression Bus$0.circuit , as seen in Figure 5. 15 CHAPTER 2. ALLOY > Bus$0.circuit Local$0 Local$1 Local$1 Local$0 Figure 5: Prompt for the circuit of a Bus Since the expression already specifies the bus in the circuit’s relation, each of the tables line will simply pair a road in the first column with its respective successor in the second one. As such, we can visualize that the circuit of this bus follows the roads Local0 -> Local1 -> Local0 -> ... periodically. 2.2.5 Model Validation As previously mentioned, model validation involves the inspection of several automatically generated instances in order to detect potential model problems. In most model specifications, these examinations usually are not enough to completely validate the model. However, thanks to their automatic and arbitrary nature, these instances provide instant feedback to the user, empowering it with extremely useful knowledge of its model and the possible unwanted scenarios it allows. As a result, this forms a crucial step in any efficient model validation. As mentioned before, these instances are generated with run blocks. These blocks can optionally be named and are accompanied by a constraint were the user can optionally restrict the analyzer’s instance generator. When executing the run block, Alloy will generate a random instance in a new window. For the case of our empty run (Listing 2.10), the resulting instance was presented in Figure 1. What we have not explained yet is the fact that a run command is not restrained to this instance. By pressing the button New, the analyzer will attempt and possibly generate a new instance that also satisfies the specified constraint and model. This process can be repeated innumerous times so long as there are enough valid instances that satisfy the specified restrictions. In Figure 6two additional valid instances of the empty run are displayed. Figure 6: Additional instances of the empty run 16 2.3. DYNAMIC MODELING Additionally, run blocks also provide keywords to specify the size of the domain that will be analyzed. This can be done by using the keyword for after the block declaration, to specify the desired scope for executing the commands. For example, the command run {} for 6will generate instances with at most six atoms in each top-level signature (Road and Vehicle in our case). If we want to specify an exact scope we can add the keyword exactly resulting in run {} for exactly 6. It is also possible to precisely control the scope for each signature, for example, limiting the analysis for up to three roads and up to two vehicles can be made with the command run {} for 3 Road, 2 Vehicle. 2.3 Dynamic Modeling 2.3.1 Behavior Specification Dynamic models describe how systems can behave with the advancement of time. Typically, dynamic models are some sort of state transition systems. Alloy 6 introduced the ability to define said specifications, a feature which before was supported by the Electrum extension [21,11]. To demonstrate these dynamic modeling features we will expand our previous example. In particular, we will explore a traffic system with moving vehicles, which gradually traverse the road network. Every dynamic model should specify the events that can happen to any entity that belongs to the universe in question. Nevertheless, only some of these are actually useful to study in each model. First, the signatures and relations whose value will change over time should be declared as being variable with the keyword var. In our example, we plan only to vary each of the vehicle’s location and thus this relation must be declared as a variable relation. The new definition is presented in Listing 2.11. abstract sig Vehicle { var location :one Road } Listing 2.11: Declaration of the variable location After declaring the mutable structures that characterize the state, the first step to describe a dynamic model is to specify its initial states. This involves declaring constraints regarding our variable components using the logic constructs already used in static modeling. For our traffic system we will specify that initially the cars are located in any local road, while buses will be located in one of the roads of their itinerary. These constraints are declared in a fact named init as presented in Listing 2.12. fact init { all c:Car |c.location in Local all v:Bus |v.location in v.area } Listing 2.12: Initial state fact 17 CHAPTER 2. ALLOY After defining the initial states, the next step it to specify the model’s behavior and evolution using Alloy’s temporal logic. These can be solely implemented within facts, however the best common practice is to describe each possible event with a predicate. Predicates are very similar to facts and specify a list of constraints. The main difference is that they do not inherently declare any assumptions, and are instead evaluated only when called upon in other blocks. Additionally, entities can be shared in said calls, allowing for the abstraction of the constraint block themselves. The main event that can occur in our model is when a vehicle moves between roads. In the specification of this event, our predicate will have to dictate that the vehicle in question will only move to one of its adjacent roads. In addition, if said vehicle is a bus, the chosen road must correspond to the one specified in its circuit. A possible specification is presented in Listing 2.13. pred move[v:Vehicle] { some r:v.location.adjacent { location' =location ++ v->r vin Bus implies rin v.location.(v.circuit) }} Listing 2.13: Move event As we can see, the specified predicate move receives the vehicle in question and verifies that for one of its adjacent roads, the new locations (specified by using the prime operator in location') will be equal to the current locations overlapped (++) with the tuple relating the vehicle to its new road. In addition, if the vehicle is a bus, this road must also be specified as the circuit’s successor for the current location. This specification will allow for several types of movements between the vehicles and the roads, which, in conjunction with other vehicles and other possible actions, will allow each state to branch out into several valid new states. The second behavior that we must describe regards the changes caused by any other possible event. As previously mentioned, dynamic models must take into account all possible occurrences regarding their defined universe, otherwise their specifications will not be complete abstractions of their intended systems. As such, even without the ability to precisely identify or describe such events, we must disclose how they affect our model. In most dynamic models, these external events do not affect the declared mutable structures, and can intrinsically be viewed as stuttering steps. Specifying such stuttering is very simple, since we only need to specify that the value of any of our mutable structures remains the same. For our model, the stutter specification will state that the new value of the relation location will equal its current value. The resulting predicate is presented in Listing 2.14. pred stutter { location' =location } Listing 2.14: Stutter event 18 2.3. DYNAMIC MODELING With every possible event specified, the only thing left to specify is how these will be interleaved to form complete instance traces. For this, we must enforce that every state transition follows one of the specified events, i.e. some vehicle moves or the systems stutters. To enforce this in every state we simply need to enclose the resulting expression within the always temporal operator. The resulting fact is presented in Listing 2.15. fact Traces { always (stutter or some v:Vehicle |move[v]) } Listing 2.15: Traces fact With the valid traces specified, the only thing remaining in our model is to define the liveness rules it should satisfy. 2.3.2 Temporal Logic Dynamic model constraints can be specified through the use of temporal operators. These specify how the constrains will be checked throughout an instance trace, and can be distinguished between future or past operators. Regarding future operators, the most commonly used are the unary operators always,eventually , and after. As previously seen, always states that its enclosed expression is true in any possible state. On the other hand, eventually declares an expression as an inevitability, while after forces its enclosed expression to be valid in the next state. Additionally, these operators can be mixed to form more complex expressions. For example, if we want to specify an intermittent event we can use the combination always eventually 𝜙. Alloy also supports the binary temporal operators 𝜙until 𝜓 and 𝜓releases 𝜙, the former dictates that 𝜓will happen and 𝜙must be true until then, and the latter dictates that 𝜙can only stop being true after 𝜓. Past operators function mostly as counterparts for the future ones. The unary operators once, before, and historically, dictate that the enclosed expression was once true, was true in the previous statement, or was always true, respectively. It is also possible to use the binary operators 𝜙 since 𝜓and 𝜓triggered 𝜙, the former stating that 𝜙became true after𝜓occurred, and the latter that 𝜙was always true, or at least true after 𝜓. 2.3.3 Liveness Constraints With the previously presented operators we can complete our model and specify the final constraints to correct its behavior. The first regard buses, and how these vehicles must continuously move throughout their circuit in order to provide their public service. The second regards freeways and vehicles, and dictates that no vehicles are allowed to stop in freeways. This is to ensure the drivers safety in these high flow 19 CHAPTER 2. ALLOY roads, since stopped cars form obstacles which can easily cause traffic jams at best or traffic accidents at worst. The resulting constraints are presented in Listing 2.16. These are called liveness constraints because they force some “good” behaviors to happen, unlike safety constraints that only forbid some “bad” behaviors from happening. fact Liveness { all b:Bus |always eventually move[b] all v:Vehicle | always (v.location in Freeway implies eventually move[v]) } Listing 2.16: Liveness constraints As depicted, the first constraint dictates that every bus will always eventually move, and in conjunction with the definition of move will thus provide its intended service. The second constraint states that for every state if a vehicle is located in a freeway, then it will eventually move to an adjacent road. 2.4 Dynamic Model Analysis Similarly to what was described in our static model, our model analysis will be divided into two phases. In the first phase we will begin by validating our model, by inspecting arbitrary instances generated with arun block, to have a first glance of our model, and confirm that there are no evident mistakes. In the second phase, we will be resorting to check blocks to verify expected properties about our model. 2.4.1 Model Validation In order to validate our model we can start by executing the command: run Empty {} for 6but 1 Vehicle When opening the generated instance the result is the trace presented in figure 7. When compared to the static analyser, presented in Figure 1, we can see that the visualization now depicts two different states of the model as well as a depiction of the trace on top, highlighting which transition is currently being displayed. In addition, the New button is gone, and is now replaced by six buttons. The first one named New Config works in the same way as the old button, and thus will cause the analyzer to generate a new configuration with new values for the static signatures and relations. As the name suggest the next button, named New Trace, will generate a new trace for the same configuration, if possible. Following we have the New Init button which generates a new initial state on the current configuration. The New Fork button will attempt to branch the current displayed transition generating a different next state. Finally we have two arrow buttons which allow us to move forwards and backwards along the trace. 20 2.4. DYNAMIC MODEL ANALYSIS Figure 7: Dynamic model visualizer 2.4.2 Model Verification To verify our model we will be examining two different types of properties on both buses and cars, namely Safety and Liveness properties. 2.4.2.1 Safety Properties We will begin by studying some of the vehicles’ Safety properties, which specify the absence of unwanted behaviors on our system. These properties tend to be easier to model check, since these can in fact be refuted by exhibiting only a finite number of steps that leads to a “bad” state. These are typically specified using the pattern always 𝜙, where 𝜙specifies an invariant that all reachable states must satisfy. Starting with buses, we want to specify that a bus will never leave its area of operations. To specify this we can simply state that for every bus we will always have its location contained within its area. The resulting check is presented in Listing 2.17. check BusSafety { all v:Bus |always v.location in v.area }for 6but 1 Vehicle Listing 2.17: Bus safety When executed, Alloy will attempt to search for a counter-example within ten steps using a bounded model checking verification technique, where it will generate and test several possible examples. If it fails to find such a counter example it reports that the property may be valid for every case. A user has the flexibility to modify the verification behavior either by adjusting the scope of the bounded verification or by eliminating the restriction, thus performing an unbounded model checking verification. 21 CHAPTER 3. ALLOY4FUN pred inv1 { // A road cannot be adjacent to itself } //SECRET pred inv1o { no adjacent & iden } //SECRET check inv1{ inv1 iff inv1o } Listing 3.1: Constraint challenge 1 This approach allows the challenge developer to precisely control which constraints to verify in each challenge. However it also decouples all of the assumptions from the model, which can cause errors. For example, the connected constraint in Listing 2.4 is correct thanks to the previous assumption in Listing 2.3. To ensure the same correct behavior on our challenge we must declare our assumptions in the verification command. This is commonly done with an implication as seen in Listing 3.2, were we have two assumptions. Additionally, this tactic can also be used to filter irrelevant invalid states to better depict counter-examples to the users. //SECRET check inv3{ inv1o and inv2o implies (inv3 iff inv3o) } Listing 3.2: Command of inv3 When the developer finishes specifying an exercise containing one or more challenges it can then share it. Upon this, Alloy4Fun will generate two permalinks which correspond to the public and private views previously mentioned. The public link can then be distributed among competitors, while the private link allows the retrieval of the complete model and also the submissions which derived from it. The permalinks of our exercise can be accessed through Table 1. PUBLIC http://alloy4fun.inesctec.pt/BFrGk6AiedYr6Q46b PRIVATE http://alloy4fun.inesctec.pt/dJF3ab5vwCxTS4tAh Table 1: Permalinks to an exercise 28 3.3. ARCHITECTURE 3.3 Architecture The Alloy4Fun application is composed of three components. The core component is the web-service itself which provides the interfaces required to access the main web-page and thus the application’s services. Next, we have a component responsible for dealing with the Alloy language, labeled API. The final component is a NoSQL database implemented with MongoDB. A visualization of these components and their interactions is presented in Figure 13. Figure 13: Alloy4Fun architecture Web-Service The web-service is developed in JavaScript with the use of Meteor 1, a full-stack framework for web-based applications. Being a full stack application it can essentially be described as two modules, the front-end and the back-end. The front-end is responsible for defining and providing the user interface (i.e. the web-page) and maintaining the editors. The back-end is responsible for processing the user actions, which range from simple database reads and writes to more complex methods involving the external API component. API This component provides some of the Alloy Analyzer features as a simple Representational State Transfer (REST) service which formats its responses in JavaScript Object Notation (JSON). Just like Alloy, it is written in Java to ensure full compatibility. Its main function is to analyze models provided by the framework in order to provide results, namely counter-examples. One key fact about these requests is that they are session based, since it is desirable to keep an analyzer instance alive as long as the user has the web-service opened on a given model. A brief description of its HTTP interface is presented in Table 2. 1https://www.meteor.com/ 29 CHAPTER 3. ALLOY4FUN Method Parameters Description POST “/getInstances” • The session’s unique identifier • The parent session’s identifier • The Alloy model • The command to execute • The number of instances required This method parses and computes the provided Alloy model and generates its results in an internal temporary state (i.e. a session) recognizable by the provided unique identifier. Subsequently it will generate the requested number of Alloy instances from the session and serialize them within the method’s answer, along with any errors or warnings that came up. Future requests with the same identifier will skip the parsing and solving and provide the next set of instances. Sessions are deleted when they have been idle for 10 minutes or when they are identified as the parent of a new session. POST “/getProjection” • The session’s unique identifier • The target instance index • The required projection types This method provides Alloy’s projection feature, i.e. a method for changing and applying theme features on instances generated by the previous method. It requires the session’s identifier and the instance’s index in order to retrieve the instance, which will then be projected based on the types of atoms specified, serializing each projection in the method’s answer. POST “/validate ” • The Alloy model This method simply validates (syntax and type-checking) the provided Alloy model, returning either a success code or the serialized error thrown by the compiler. Table 2: API’s HTTP interface This state-based solution offers several performance benefits, since by maintaining the models in memory it is able to skip parsing and instance computations on several requests. However, it also introduces a set of major challenges on the deployment. One of the primary drawbacks is the inability to scale the application to a large amount of users and also to ensure its fault tolerance. This is essentially due to the difficulty of replicating state based applications, since to maintain the integrity of the sessions each user would have to be mapped to the exact same replica in every request. As a result, a replication of this component would require a sophisticated solution to maintain an efficient load balance of the replicas which would be made even more complex when accounting for failure resilience. Database The application’s database, implemented over MongoDB2, is mainly responsible for storing the data handled by the web-service, namely the saved models and their respective instances and counter-examples. It is comprised of the collections Link,Instance,Navigation, and Model, which are described in the dictionaries presented in Tables 3,4,5, and 6, respectively. Link Field Format Optional Example Description _id String NO 3cy7jaB4ESqdb2txK Unique identifier of the object private Boolean NO false Indicates whether the link is private or public model_id String NO 2Htt7FYT7dY9ETGRX Reference to the Model object. Table 3: Dictionary of the collection Link 2https://www.mongodb.com/ 30 3.3. ARCHITECTURE Instance Field Format Optional Example Description _id String NO 3cy7jaB4ESqdb2txK Unique identifier of the object model_id String NO 2Htt7FYT7dY9ETGRX Reference to the Model object cmd_i Int32 NO 4Index of the executed command graph JSON Object NO { "types":[...], "sets":[...], "rels":[...] } The serialized Alloy instance time String NO 2020-12-13 23:28:11 Serialized date of the instance Table 4: Dictionary of the collection Instance Navigation Field Format Optional Example Description _id String NO zKAYz8BCDmHKgNoSx Unique identifier of the object time String NO 2021-03-19 17:28:11 Serialized date of the saved instance operation Int32 NO 0Enumeration for the navigation action: 0for forward, 1for backward instIndex Int32 NO 6The index of the navigated instance model_id String NO 2Htt7FYT7dY9ETGRX Reference to the Model object Table 5: Dictionary of the collection Navigation Model Field Format Optional Example Description _id String NO zKAYz8BCDmHKgNoSx Unique identifier of the object time String NO 2020-12-13 23:28:11 Serialized date of the model code String NO var sig File{ var link : lone File ... The complete code of the saved model derivationOf String YES dvhCng5AdxC8MqjFy Reference to the parent model from which this one is a derivation original String YES 9jPK8KBWzjFmBx4Hb Reference to the root ancestor model sat Int32 YES 1 Status code which classifies the executed command as Satisfiable (1), Unsatisfiable (0) or Erroneous (−1) cmd_i Int32 YES 4Index of the executed command cmd_n String YES inv5 Name of the executed command cmd_c Boolean YES true Specifies if the command was a check (true) or a run (false) msg String YES The name ”Traash” cannot be found. The message presented to the user for the erroneous execution theme JSON Object YES {"generalSettings":{...}, "relationSettings":[...], ... } The customized visualization theme, if applicable Table 6: Dictionary of the collection Model 31 CHAPTER 3. ALLOY4FUN Although this database schema supports all of Alloy4Fun’s functionalities, it has two noteworthy flaws regarding some field formats. The first pertains to the choice of representing object identifiers as strings, as opposed to utilizing MongoDB ’s ObjectId types. As a result, the schema places the responsibility of generating and maintaining unique keys on the application instead of using the database’s automatic generation feature. This process can prove cumbersome and error-prone, especially in scenarios where multiple applications interact with the database. The second and more substantial flaw concerns the representation of the time fields as strings instead of MongoDB ’s Date , resulting in two different issues. Firstly, by forcing each program to work with strings it requires specialized string handlers which are error prone thanks to the second issue, which is the possible inconsistencies in date serialization. By using strings, to ensure consistency within the database, we are trusting that each database writer uses the same date serializing technique. Unfortunately, this is not necessarily the case for Alloy4Fun’s meteor web-service , as it uses the date formats of its host operating system, which can change between deployments. Currently Alloy4Fun’s public dataset [22] contains two date formats as result of this flaw, a ”month/day/year” pattern with a 12 hour clock (example: 2/12/2023, 8:23:47 PM) and a ”year-month-day” pattern with a 24 hour clock (example: 2020-12-13 23:28:11), which compromise the data consistency. The essential piece of the database is the Model collection. Each saved model (e.g. a submission to an exercise) pairs its source code with several context data such as the theme used, the command executed, the resulting state (i.e. whether the submission’s execution was valid, invalid or erroneous), a reference to the root ancestor model and, most importantly, a reference to the model it was derived from. Figure 14: Visualization of a derivation tree 32 3.3. ARCHITECTURE It should be noted that every time secrets are introduced in the public view of a model already containing secrets, a fresh derivation tree is created. This means that in each branch of a derivation tree there is at most one model with secrets. The root ancestor model is this model with secrets, if it exists, or the root of the tree if there are no models with secrets. With these references, the database effectively stores a derivation tree for each exercise, where each possible path from the root ancestor model to a leaf mostly consists of a student’s attempt in solving the problem. A simple visualization of one of these trees is presented in Figure 14, were we have three different branchs of submissions. The first two branches, composed of submissions 0 to 2 are likely to have been created from two different attempts at solving the original exercise. The last branch, composed of submissions 3 to 6 entails that a permalink was created on submission 5, which was accessed and modified at least one time, resulting in the observable branch. Due to the anonymous nature of the links, it is impossible to determine whether the branched submissions were created by the author of the permalink or if it was the result its distribution among other individuals. The system stores the permalinks for accessing each shared model in the Link database collection described in Table 3. These links are associated with privacy settings, distinguishing them as either private or public. This distinction determines whether the backend displays or conceals the secrets of the accessed model. 33 4 State of the Art Throughout this chapter we will present a variety of program hint and repair systems and their corresponding methodologies. We will begin by introducing an abstract hint generation framework which broadly describes the data flow across most recent automatic feedback systems. Afterwards, we will present several hint generation systems in the context of this framework, grouping them in four types of feedback methodologies: Fault Localization, Synthesis-Based, Curated, and Data-Driven. Each methodology is explained in relative detail with an extra focus on its strengths and compromises. We conclude by exploring the application of text generation in the context of hint generation systems. 4.1 The HINTS Framework In recent years, there has been a proliferation of diverse approaches for generating hints in programming languages [26]. These approaches encompass a wide spectrum of unique ideas and techniques, spanning various research domains, including behavioral and state repair [27], machine learning, data mining [2], among others. Consequently, the hints generated by these approaches exhibit several degrees of diversity, manifesting as error highlights, recommended actions, explanatory comments, and various other forms of support. Despite this, there is a consistent data flow pattern that underlies most methodologies. We always begin with a step where we analyze user submissions, which provide information that can be regarded as intermediate unprocessed hints. The program sequentially processes hint intermediaries through various components, which either reduce or transform the crude suggestions into useful hints for the user. This data flow commonality does not occur by chance; rather, it constitutes the fundamental underpinnings of any hint generation system. The Hint Iteration by Narrow-down and Transformation Steps (HINTS) Framework [26] is an architecture which abstractly depicts all of the common steps among many automated hint generation systems. A visualization of this framework is presented in Figure 15. The process starts with a pool of data as an input, which is commonly referred as hint data since it is either composed of or used to generate hints. These can include data-sets produced by peers, property based tests for the models, direct user submissions, or any other static feature that could be useful to the 34 4.1. THE HINTS FRAMEWORK Figure 15: The HINTS framework system. Once a data pool has been established, a hint system will then perform one or several processing steps to generate new hint data, which can be classified within two types of actions. • A transformation action as implied involves changing the way existing hints or data are represented. Some examples of this are partitioning hint data, restructuring an existing entry, standardization, or discarding duplicates. For example, an Alloy model can be broken down into its signatures, predicates and functions, over which some could be discarded while other could be modified to allow for custom evaluations. • A narrow down action involves selecting subsets of hint data from the original pool. These selections take into account two different factors: the first one is the relevance of the hints when applied to a student’s program; the second one is their overall quality for the situation, i.e. their capability to help the student produce a correct solution. Each time new hint data is produced it is added to the original pool. Finally a hint system delivers the student one or more subsets of hint data which represent the resulting hint’s information. The HINTS framework does not imply any order or restriction in which these steps must be taken. However most approaches need to make compromises in this regard, for example a system can become limited to its initial input data if it has a requirement to assure the integrity of their hints during their lifespan. Other examples include approaches that do not require any transformation to be made upon its data, being thus able to supply hints directly from the programs. 35 CHAPTER 4. STATE OF THE ART Over the following sections we will be discussing several examples of well developed hint generation systems. As previously implied, these systems can be abstracted and described within the HINTS framework and thus several of these concepts will be recurrent through out our presentation. 4.2 Fault Localization Hint Generation Fault localization systems stand on the boundary of what can be defined as a program hint or repair system. Their main focus is to identify defects in a program’s source code, classifying the detected faults and present the user with suggested actions, i.e. hints. The purpose of these suggestions is to present the user with options in achieving a state free of faults. This can be valuable in a debugging context but it does not necessarily aid in comprehending or resolving the underlying engineering issues [45]. Overall, their general processes are very similar: faulty models are put through a series of validating artifacts which isolate suspected faults within the original model; the suspicions faults are then presented directly to the user, along with predefined suggestions for solving them. The main distinction between Fault Localization systems is their fault identifying techniques. One of the oldest techniques is program slicing, a technique that abstracts a program into a reduced form by statically or dynamically deleting irrelevant parts from it. Numerous studies have explored this technique [48]. A few examples are eXVantage [46], a coverage-based testing system focused on minimizing performance overhead, and JSDiagnosis [47], an AI-based dynamic slicing system. Another common technique is spectrum-based fault localization, a technique which identifies faults by comparing the execution traces of failing and passing program executions, classifying each identified difference with a fault suspicion metric. A key challenge in these systems is ensuring their metrics achieve an effective balance between precision and coverage of their fault detection. Similar to the previous techniques, there are also numerous works on this topic [39], some examples include LAURA [1], a system that applies program transformations to validate the executions, and PROUST [18], which contains a set of predefined programming plans which are executed on the user input in order to generate a diagnostic of the bugs found in the code. 4.3 Synthesis-Based Hint Generation Synthesis-based tutoring systems rely on generating new programs or models from a user’s submission in order to provide their hints. These generation processes vary depending on the implementation, some might use unit or property-based tests, while others will exhaustively mutate the prompted models into new ones. In the specific case of Alloy there exists already several of these tools, such as ARepair [42], BeAFix [8,7], and TAR [10]. The techniques used by these tools are similar. Upon receiving a student’s model the system will then begin synthesizing new submissions from the wrong ones. The used tactic depicts the main difference between the mentioned implementations. 36 4.3. SYNTHESIS-BASED HINT GENERATION ARepair employs the fault localization tool AlloyFL [43] to identify a set of suspicious declarations. Following this, the declarations undergo systematic modifications through a predefined set of rules referred to as mutators , creating an array of mutated declarations. This procedure repeats until either the computed declarations passes the tool’s fault-localization tests or when it meets the limit of its search criteria. One issue with ARepair is that its fault localization tests may not always be enough to properly validate the synthesized model. Consequently, there is a risk of incorrect fixes being generated under the assumption that they are valid. BeAFix is similar to ARepair as it uses FLACK [50], a fault localization tool which benefits from Alloy’s counter-examples, to extract and mutate a set of suspicious declarations from an incorrect model. In contrast to ARepair, it leverages the oracles of the individual models to validate each synthesized model, which eliminates the potential for falsely validated models. Unfortunately, both ARepair and BeAFix only support the non-temporal version of Alloy. This issue was the main motivation to the development of the Temporal Alloy Repair (TAR) tool, which was the first technique for fixing Alloy 6 first-order temporal logic specifications. The technique employed is designed to exhaustively preform syntactical mutations until the tool either finds a solution or it reachs a limit imposed by the developer. When a new model is synthesized it is stored as an Abstract Syntax Tree (AST), a structure representing the core model as seen when parsed by Alloy’s compiler. After computing the repaired model, the resulting AST, along with the actions that produced it, can be employed to either rectify the original model or provide hints to the user. A visualization of the typical architecture of these systems is presented in Figure 16. Figure 16: Synthesis-based hint generation As we can see, there are two types of artifacts which influence the main processing steps. The validation metrics are mostly specified by the teacher, which generally consist of an oracle or unit tests that can be used to check the correctness of the synthesized models. Additionally, these may also include optimizations, such as TAR’s counter-example pruning techniques. Some quality metric is then used on the process of selecting a final hint in the form of a tree edit. This can be as trivial as selecting the first correct model found or more robust ones such as scoring each synthesized model based on the number of edits required to obtain it from the original incorrect one. 37 5 Alloy Specification Assistant In this chapter we will present a new hint system for Alloy4Fun, which we named SpecAssistant , that relies on existing data from the users in order to generate its output, being thus classified as data-driven. The overall process is similar to the Hint Factory [40] approach, as it starts by processing historical data into unique states, which are then assembled into a Submission Graph, upon which a traversal policy will be used to select the next state, and the respective hint. Upon receiving an invalid submission to a challenge, it will process the user’s formula and use it to match a state of the submission graph. The next state is then determined by the predefined policy rules which assess the quality of the candidate states. Finally, the state’s information is processed into a hint, composed of text highlights and custom messages. A graphical view of this architecture is presented in Figure 21. Figure 21: SpecAssistant architecture In this chapter, we delve into the intricacies of the developed hint generation system. We will begin by describing the fundamental concepts and processes used by the system, and how these can allow us to generate hints. We will then describe the implementation of these techniques on Alloy4Fun, elaborating on aspects such as the framework and libraries used, the data formats, and the user interface. 44 5.1. CORE TECHNIQUES 5.1 Core techniques This section aims to describe the core techniques of our system. We begin with a description of our formula comparison procedures and their impact in the system. Afterwards, we proceed to characterize how the peer data is stored in the system’s data model. Finally, we describe how the data model is processed into the final hints which are displayed to the user. 5.1.1 Formula Comparison Before presenting the core techniques we must first describe the data that these were designed to handle. Every process in our system revolves around Alloy formulas which were specified by the users in their attempts to solve challenges in a exercise. These formulas can be parsed into Abstract Syntax Trees (ASTs), which detail the hierarchical structure of the syntactical elements within the formulas. In Figure 22, we depict the AST of the formula all s:Student |sin Human , which asserts that every student is a human. It is composed of a quantifier that is described by a declaration and a body. The body is defined by applying the in operation to the variable sand the set Human. Figure 22: Example of an AST When handling formulas, we can compare them in three distinct ways: through their lexical representation, their syntactical representation, or their semantic meaning. Each approach comes with its set of benefits and compromises, usually involving a trade-off between the final hint’s availability and quality. These different approaches are described as follows. Lexical Comparison A lexical approach views and compares each formula directly as written by the user. As such it allows the system to precisely tailor each hint to each submission, for example the system can directly mention the user’s custom variable names or highlight portions of the text in order to draw the user’s attention to them. Unfortunately, this greatly decreases the availability of the hints, since providing the user with a hint requires the submission to exist in the database exactly as written by the user, which is very unlikely thanks to all the personal choices the users can instill on their submissions. 45 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT Syntactical Comparison A syntactical approach discards most of the user’s personal decisions, such as parameter names and order, by focusing only on the meaning conveyed by the arrangement and structure of keywords in the formula. Intrinsically, this abstracts multiple submissions under the same AST, which increases the chances of providing the user with a hint. This comes at a slight cost in the quality, as it results in the loss of certain contextual details within the formula elements. These details may include custom names, macros and other “syntactic sugar” constructs, file locations, among others which are valuable for providing more specific and customized hints. However, it is possible to build translations between lexical and syntactical formats, which allow for approaches with the best of both worlds. An example of two syntactically equivalent formulas can be found in Listing 5.1. some r1,r2 :Road |r1=r2 ≡some x,y :Road |y=x Listing 5.1: Syntactical equivalence example Semantic Comparison A semantic approach focuses solely on the meaning of the formula itself. This allows for an large degree of abstraction, which should increase the systems ability to generate hints. Regrettably, this semantic approach removes almost all of information that is traceable to the original submission, and thus it cannot be used to generate contextual hints, which severely degrades the system’s quality. Additionally, this approach also comes with some performance issues since semantic evaluations would require the use of Boolean Satisfiability Problem (SAT) solvers to check the equivalence, which are notoriously slow. An example of semantically equivalent formulas can be found in Listing 5.2. adjacent =~adjacent ≡all r:Road |rin r.adjacent Listing 5.2: Semantic equivalence example Our system mixes the lexical and the syntactical approach, by having each formula inspected and compared syntactically using lexical formats. This is achieved by normalizing the original formula to a predefined lexical standard, so that when compared directly only syntactical differences will be visible, allowing the system to take advantage of simple lexical comparisons without compromising the abstraction power of the syntactic approach. The used normalization technique can vary across implementations and generally dictates a trade-off between quality and availability. Our normalization technique implements three rules: Commutativity The sub-expressions of a commutative operation are arranged following some order. For example, in the expression Band A, if Aprecedes Bthen its normalized version would be Aand B. This rule is applied in formulas using the following operators: intersection (&), union (+), equal (=), different (≠), and (∧), or (∨), equivalent (iff), and disjoint (disj). When dealing with these operators, 46 5.1. CORE TECHNIQUES our normalization process organizes the arguments of each operation based on their lexicographic order. We have opted for the lexicographic order as it effortlessly ensures a consistent ordering across all formulas. Equivalence If two different operators are equivalent then only one should be used in the normalized version. For example, if we consider that >will be the inequality operator of choice, then any expression containing ≤would be rewritten with it. For example, A≤Bwould be normalized as not B<A. This rule is primarily focused on the transformation of inequality operators. When confronted with the operators ≥and ≤, our implementation replaces them with the operators <and >, respectively, while simultaneously switching the order of their arguments. Identifiability Identifiers (such as function parameters or quantified variables) must be normalized under the same naming scheme. For example, the syntactical equivalent formulas all x:A|x in Band all a:A|ain Bshould have the variables xand arewritten to the same name. The assigned names can be defined as wished by the developer, so long as it is an alphanumeric identifier which assures that syntactically equivalent formulas use the exact same names on their identifiable nodes. For our application, we only need to update identifiers specified by users. Specifications from default Alloy modules are equal across all environments, which as a result ensures their consistent naming scheme. Alloy formulas include four constructs that introduce identifiers: functions, predicates, let blocks, and quantifiers. Functions, predicates and let constructs introduce identifiers to denote one or several formulas. The simplest way to handle these cases is to expand these identifiers to their complete definition, effectively removing them from the AST. For quantifiers we rename each variable identifier with the concatenation of the prefix ref and the index of its declaration. Before this renaming, we also reorder variables according to the lexicographical order of the respective types, and refactor disjoint (disj) clauses into the quantified formula. This reordering process also involves merging sequential quantifiers that have the same operator. A few examples of this normalization process are depicted in Listing 5.3. all x:X|all n:x.next|n≠x {all ref0:X, ref1:ref0.next |ref0 ≠ref1 all u1:U|some u2:U|uin u.next {all ref0:U|some ref1:U|ref1 in ref0.next all disj n1,n2 :N|n1 in adj.n2 {all ref0:N, ref1:N|disj[ref0,ref1] =⇒(ref0 in adj.ref1) Listing 5.3: Examples of normalized quantifier formulas 47 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT An additional issue that is addressed by the normalization is the treatment of constant true formulas. Alloy lacks a dedicated syntax for expressing these constants directly, but they are equivalent to empty code blocks. When custom empty functions or predicates are invoked within formulas, expanding their definition can introduce these empty code blocks into an AST, which is syntactically incorrect. So we have implemented some rules to remove them. For example, in and operations we simply drop the empty block, and an expression if condition then xelse ywill be rewritten to its then branch when presented with an empty block as the condition, among others. 5.1.2 Submission Graph The data model is the main component of a data-driven system. In our case it is the direct byproduct of the peer data and it plays the pivotal role in the system’s output. Our system will process this historical data of each challenge into a model named Submission Graph, a structure which shares properties with Control Flow [3] and Decision Graphs [32]. This graph monitors the decision-making of multiple agents in their pursuit of solving a specified challenge, by aggregating the control flow that illustrates how their actions and choices helped them progress through their difficulties. An abstract depiction of this model is presented in Figure 23, which will be analyzed and explained throughout the following paragraphs. Figure 23: Example of a Submission Graph Similar to generic graph structures, the representation under consideration is depicted using nodes and edges. These correspond to the two essential components of our model, States and Transitions, which are described as follows: States 𝑆– States correspond to the Alloy formulas (ASTs) submitted by users while attempting to solve a challenge and processed by our previously described normalization technique. In our system, we also register a few key attributes of each state: the formula’s validity (i.e. indicating whether 48 5.1. CORE TECHNIQUES it solved the challenge), its anticipated truth table size (latter referred to as its complexity), the frequency the formula was submitted, and the frequency the formula was modified (i.e. the sum of the out-edge’s frequencies). Transitions 𝑇– Transitions capture the sequence of states users followed while solving challenges. Similarly to states, for each transition we register: the frequency, the minimum Tree Edit Distance (TED) between its states, the proportion of times that a transition was chosen over its competitors, i.e. the peer transitions that share the same source state. Our system creates a different submission graph for every challenge of every exercise. These graphs tend to have a similar shape to the graph of Figure 23, which steams from the format of the derivation tree structures that originate them. Typically, there is a central node, here colored blue, corresponding to the challenge’s initial formula, usually an empty block, which branches into several neighbor formulas. This node typically has a path to every node of the graph, making the submission graph weakly connected. As we progress outwards from the central node we traverse several paths of invalid nodes, here colored white. Occasionally, these paths can branch to or join other paths or return back to the central node. Each path can be a dead end, when a student interrupted a session without solving the challenge, or reaches a valid submission, the nodes colored green. Solution nodes tend to have a higher-than-average in-degree, because many student sessions converge into the same valid submission. 5.1.3 Hint Model The submission graph encompasses all the potential decisions made by students, rendering it a nondeterministic graph. In order to use it to generate hints for users, it is essential to select a specific path Figure 24: Example of a Hint Model 49 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT for each state, essentially narrowing the submission graph into a deterministic one. This procedure is referred to as applying a traversal policy on the submission graph. It reduces the submission graph into a forest of state trees, each rooted at a solution, which we have labeled as the hint model. Additionally it discards the states that cannot reach a solution. An example of a hint model from our previous example is displayed in Figure 24. To create an effective hint model, we need to develop a policy algorithm capable of extracting it from the original submission graph. However, there are some caveats to consider. Depending on the nature of the challenge and its designer’s intentions, certain policies may be more successful at generating superior hint models compared to others. Since we cannot forecast the challenge designers’ preferences, our primary focus has been on developing a modular algorithm, designed to provide designers with the flexibility to customize it to their policy needs. 5.1.4 Policy Algorithm The basis of our policy algorithm is Dijkstra’s shortest path algorithm for weighted graphs. The algorithm operates by maintaining a score on a set of tentative states, which starts as the set of all valid states, i.e. the set of states that correctly solve the challenge. It will iteratively select the state with the best score from this set and use it to update the scores of states that transition to it. After each selection, the algorithm Algorithm 1: Policy Algorithm Input: (𝑆,𝑇 ): Submission Graph Data: 𝑂Objective, 𝑁: Neutral Value, 𝑅: Policy Rule Output: 𝑚𝑜𝑑𝑒𝑙: The hint model begin Initialize 𝑞𝑢𝑒𝑢𝑒,𝑝𝑟𝑒𝑣𝑖𝑜𝑢𝑠,𝑠𝑐𝑜𝑟𝑒 and 𝑚𝑜𝑑𝑒𝑙 as empty sets; for every valid state 𝑠in 𝑆do 𝑞𝑢𝑒𝑢𝑒 ←𝑞𝑢𝑒𝑢𝑒 +𝑠; 𝑠𝑐𝑜𝑟𝑒[𝑠] ← 𝑁; end while 𝑞𝑢𝑒𝑢𝑒 is not empty do 𝑠′←state in the 𝑞𝑢𝑒𝑢𝑒 with the best 𝑠𝑐𝑜𝑟𝑒 according to 𝑂; 𝑞𝑢𝑒𝑢𝑒 ←𝑞𝑢𝑒𝑢𝑒 −𝑠′; 𝑚𝑜𝑑𝑒𝑙 [𝑠′] ← 𝑝𝑟𝑒𝑣𝑖𝑜𝑢𝑠[𝑠′]; forall transitions 𝑡 that leads a state 𝑠 into 𝑠′do if 𝑠∉𝑚𝑜𝑑𝑒𝑙 ∧𝑠𝑐𝑜𝑟𝑒[𝑠] is worse then 𝑅(𝑠, 𝑡, 𝑠′) according to 𝑂then 𝑠𝑐𝑜𝑟𝑒[𝑠] ← 𝑅(𝑠, 𝑡, 𝑠′); 𝑝𝑟𝑒𝑣𝑖𝑜𝑢𝑠[𝑠] ← 𝑠′; 𝑞𝑢𝑒𝑢𝑒 ←𝑞𝑢𝑒𝑢𝑒 +𝑠; end end end end 50 5.1. CORE TECHNIQUES designates the chosen state and the transition from which the highest score was computed as part of the hint model and subsequently excludes them from any potential operations in its future iterations. Once there are no more states to be evaluated the algorithm ends. With this framework we allow the designer to customize three parameters. The first parameter is the objective of the algorithm, i.e. whether the goal is to minimize or maximize the node’s scores. The second parameter is the neutral score value, which represents the score assigned to the algorithm’s initial set of states (the set of valid states). Finally we allow the designer to customize the rule used to compute the new score of a state given a transition. In this rule the user has access to all of the attributes registered in the submission graph for the transition and the two states involved, and can use their normalized values to define a custom score formula. The pseudo-code representation of this process is presented in Algorithm 1. In Table 7, we provide an overview of several policy options that we have experimented with. The policy rules in this table will refer to some of the attributes registered in states and transitions, and already discussed in Section 5.1.2. These attributes include the Tree Edit Distance (TED), the state’s complexity (𝐶𝑂𝑀𝑃𝑋) and the state’s submission frequency (𝐹𝑅𝐸𝑄). Furthermore, the policy can mention algorithm specific attributes, such as the current 𝑆𝐶𝑂𝑅𝐸 associated with the source node. Name Objective Neutral Value Policy Rule Shortest Tree Edit Distance (TED) MIN 0𝑇𝐸𝐷 +𝑆𝐶𝑂𝑅𝐸 MinMax Tree Edit Distance (TED) MIN 0𝑚𝑎𝑥 (𝑇 𝐸𝐷, 𝑆𝐶𝑂𝑅𝐸) Balanced TED and Complexity MIN 00.5𝑇𝐸𝐷 +0.5𝐶𝑂𝑀𝑃𝑋 +𝑆𝐶𝑂𝑅𝐸 Proportional Complexity MIN 0(1−𝑃𝑟𝑜𝑝𝑜𝑟𝑡𝑖𝑜𝑛) × 𝐶𝑂𝑀𝑃𝑋 +𝑆𝐶𝑂𝑅𝐸 One MIN 01+𝑆𝐶𝑂𝑅𝐸 MaxiMin Frequency MAX 0𝑚𝑖𝑛(𝐹𝑅𝐸𝑄, 𝑆𝐶𝑂𝑅𝐸) Popularity MAX 1𝑃𝑟𝑜𝑝𝑜𝑟𝑡𝑖𝑜𝑛 ×𝑆𝐶𝑂𝑅𝐸 Table 7: Examples of policy parameters 5.1.5 Policy Execution When processing the users current submission, SpecAssistant will normalize it with the same technique used on the peer data. Subsequently, the obtained formula will then be prompted on the hint model which will give the best next state to guide the user. This procedure is restricted to the pre-existing data and consequently, when a hint is solicited with an unknown submission, the system will be incapable of providing a hint. This problem can be mitigated by querying the hint model with variants derived from the submission’s formula, from which we could extract relevant hints. The implemented approach for expanding the overhaul scope of each query consists in querying the hint model with a set of mutated formulas derived from the submission. The variant formulas are built from a combination of procedures named mutators which have the goal of transforming the original formula based on a predefined rule. In our system, we utilize the mutators conceived in TAR [10] which are presented in Table 8. When a submission is not in the submission graph, this method employs an 51 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT exhaustive procedure where each mutator is systematically applied to the submission’s sub-formulas, generating a variety of mutated formulas of which we retain in a set those that are contained in the hint model. Finally, the mutated formula with the best score according to the selected policy rule is then used to infer the hint. Since the transitions corresponding to the mutators do not exist in the graph, this technique can only be used with policy rules that rely on attributes that are independent of the submission data. For example, it cannot be used with policy rules that rely on the frequency or the proportion. Mutator Rule Mutation Example RemoveBinary A[bop] B{A A or B{A A[bop] B{B A - B {B ReplaceBinary A[bop] B{A[bop'] B Aand B{Aor B A&B{A-B ExtendOrReduce A{A[bop] B A{A+B InsertJoin A{A.B RemoveUnary [uop] A{Aonce no A{no A ~ A {A ReplaceUnary [uop] A{[uop'] Aonce no A{always no A ~ A {A' InsertUnary A{[uop] A no A{always no A InsertPrime A{A' RelationToUnary A{^A ReplaceSet [uop] A{[uop] Bno A{no B BinaryToUnary A[bop] B{[uop](A [bop'] B) A in B{no (A + B) QuantifierToUnary [qtop] a:A|B{[uop] Ano a:A|inv[a] {no A ReplaceQuantifier [qtop] a:A|B{[qtop'] a:A|Bno a:A|B{some a:A|B RelationToBinary A{A[bop] B A {Aand B ReplaceRelation A{B A {B Table 8: TAR’s mutators Each rule presented in Table 8depicts the mutator’s effect with a set of arbitrary expressions and operators, where the former is represented by capitalized letters and the latter by the keywords: [uop] [bop] and [qtop], denoting unary, binary and quantifier operators, respectively. 5.1.6 Hint Generation After successfully computing the best next state, the system needs to present this information to the user in the form of a hint. For automated repair systems whose goal is to perform auto-corrections, this can be achieved by simply presenting to the user the fixed submission. In hint generation however, this is more complicated since the goal is not to solve the problem but to provide an educational scaffold to the user, i.e. provide just enough information to help a learner overcome its obstacles, without completely solving the problem and miss the educational objective. This is made even more difficult by the fact the 52 5.1. CORE TECHNIQUES interpretation of each hint is very likely to vary between users, so to ensure the desired effect on the user, our system should present concise information which can also be adapted to the different situations. Taking into account these limitations, we chose to implement our hints as code highlights. This stemmed from the fact that these serve as a visual focal point to the user and thus allowed us to precisely guide the user to the submissions fault. Alongside the highlight, the system will also provide a text message with further help, generated from the original state and action. The absence of any sufficiently large repository of Alloy hints prevented us from using machine learning methodologies for text generation. As a result our current text generation relies on a rudimentary rule-based approach. This approach generates textual prompts based on the transition that led to the selected next state. For actions that were computed based only on historical data (that is, the wrong submission was seen before), our system first employs a tree difference algorithm [34] to categorize the overall transition as list of changes, specifying them as deletions , as insertions , or as replacements . Subsequently, it will retrieve the closest change to the AST’s root, matching its category either the phrase “Try adding something to this declaration” for insertions or the phrase “Try to change this declaration” for the remaining categories. The chosen change is also used to determine the faulty expression to highlight. Conversely, when transitions result from mutations (that is, the wrong submission was not seen before), the displayed hint is drawn from the definition within the mutator’s class, resulting in the messages found in Table 9. Mutator Hint RemoveBinary ReplaceBinary InsertJoin Binary operator has to be changed or removed. InsertUnary InsertPrime Insert an operator. RemoveUnary ReplaceUnary Unary operator has to be changed or removed. BinaryToUnary Transform into a unary expression. QuantifierToUnary ReplaceQuantifier Quantifier has to be changed. ExtendOrReduce ReplaceRelation A different relation is required. InsertJoin RelationToBinary RelationToUnary Add a binary or unary operator. RemoveUnary ReplaceUnary Unary operator has to be changed or removed. ReplaceSet Expression under unary operator has to be changed. Table 9: Hints for TAR’s mutators 53 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT ExprQt objects describe quantifier declarations. These are composed of a quantifier operator, a list of variable declarations, and the quantified sub-expression. As previously explained in Section 5.1.1, to comply with our identifier normalization clause, we must reorder each of the identifiers in order to rename each using the index of its declaration. Although conceptually simple, the implementation of this renaming poses some challenges. Depending on how the user has written their formula, the identifiers intended for reordering may or may not be separated into multiple ExprQt objects, chained by their sub-formula instances. Thus, our process begins by collecting all sequential variable declarations that share the same quantifier operator. Each declaration is an instance of the class Decl, which is composed of a list of identifiers, the declared type, and an optional disjoint clause. After collecting all declarations we then proceed to assign each the minimum 𝑑𝑒𝑝𝑡ℎ within the quantifiers AST. This 𝑑𝑒𝑝𝑡ℎ field allows us to determine the partial order induced by dependent identifiers, such as, for example, the variable zof the formula all x,y :X, z :x.next which must always be declared after x. In this case 𝑥and 𝑦would have a minimum depth of 0while 𝑧 would have a depth of 1. If a new variable was declared that depends on 𝑧it would subsequently have a depth of 2, and so on. Upon computing the 𝑑𝑒𝑝𝑡ℎ for each declaration, our normalization will start deconstructing each Decl object. Each identifier is ordered and subsequently renamed according to its declaration’s 𝑑𝑒𝑝𝑡ℎ and the lexical order of the normalized type. Simultaneously, every disjunct clause is normalized by combining it with the quantified sub-formula through the utilization either the operation and or implies. The final output of the normalization is a new ExprQt object, with the original quantifier, the renamed identifiers, and the updated sub-formula. When normalizing an AST, our system maintains a mapping between the original tree and the normalized one, in other to allow our system to trace both variable names and most importantly the file positions required for marking down a hint’s code highlight. After its normalization an AST can be further processed in two different ways. The first is string serialization, which is used in interactions with the database, and when ordering identifiers. The second is a difference algorithm, were the system is comparing two ASTs in other to determine their changes. To accomplish this, our system uses the All Path Tree Edit Distance (APTED)3[33,34] algorithm, which computes the smallest edit maps and distances between two trees. To use the algorithm we simply must define a match relation between each node and a cost model for its three possible edit operations (𝑖𝑛𝑠𝑒𝑟𝑡, 𝑑𝑒𝑙𝑒𝑡𝑒,𝑟𝑒𝑛𝑎𝑚𝑒). Subsequently, the system can compute the minimum edit distance and mapping between two ASTs. Meanwhile, the edit mapping denoting the relation that matches identical nodes between each tree is translated into a sequence of edit operations that are used by the hint generation procedures. 3github.com/DatabaseGroup/apted 60 5.2. ALLOY4FUN IMPLEMENTATION 5.2.4 Hint Model Computation With the previously defined processes for handling the submissions and the Alloy ASTs we can finally start parsing our historical data into our data models. This process is divided between three steps: firstly, we have the model ingestion were we scan and process each submission tree from the database, and add it to the respective submission graph; secondly, we have a classification step where we pre-compute a series of attributes needed throughout the model’s lifetime; and, finally, we have the policy computation step, where we narrow down the submission graph to a hint model. Model Ingestion As previously mentioned in Section 3.3, Alloy4Fun’s submission data is structured as derivation trees rooted at the exercise’s original submission. Within each exercise we have a series of challenges for the user that will have to be processed separately. Additionally, since Alloy4Fun records every execution the students’ issued, in each of these derivation trees we can differentiate every attempt at solving a exercise as a path of submissions from the tree’s root to its leaves. This data can be overwhelming, since a tree may also include syntactically incorrect submissions, submissions for different exercises in different order, executions of commands not present in the original exercise, and duplicate submission issued by the users on their explorations. Some of these behaviors are visible in Figure 27, were we depict a tree highlighting different commands with different colors. In the example, we have four different paths corresponding to four different attempts at solving three challenges (inv1,inv2, and inv3) in a exercise containing two signatures: A, which declares relation next:set A, and B, which is an extension of signature A. In this Figure 27: Exercise derivation tree 61 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT example the students inconsistently alternated between three challenges and also executed commands not present in the original exercise and not corresponding to any challenge (namely run $1). The goal of this step is to process this data by isolating each challenge from every path of the tree, and aggregating the respective submissions in the challenge submission graph. To achieve this we must simply divide the set of submissions by each targeted challenge, and subsequently relating the submissions of each resulting set by the order defined within the root exercise. Upon finishing this process we simply need to amalgamate the submissions with duplicate formulas and transitions into an initial submission graph where we only record the frequency of each transition, as exemplified in Figure 28. Figure 28: Amalgamated Submission Graphs This ingestion process is implemented in a specialized Breadth-First Search (BFS) algorithm with the CompletableFuture class, a Java class that allows for a simple specification of multi-threaded tasks. The advantage of using a multi-threaded approach is the possible performance boost obtained from parsing multiple models in parallel. Attribute Computation After populating each graph, the subsequent step is to compute each attribute needed for the policy rule computation. One of these attributes is the proportion of times each edge was traversed, which is calculated directly by determining the ratio between the number of times the edge was traversed and the number of times a user submitted its source state. Another attribute is the complexity of each formula, which is defined as the expected size of the formulas truth table. To compute this value we must count the number of nodes in the AST 𝑚and the number of independent variables 𝑛. With these properties we can obtain the truth table’s size with the value of 𝑛𝑚. The final attribute we need to compute is the Tree Edit Distance (TED) between the ASTs at the ends of each transition. For this we use the All Path Tree Edit Distance (APTED) [33,34] library. When given two distinct trees, the algorithm initiates a process of comparing and pairing identical nodes in an effort to discover the most extensive node matching. Subsequently, after computing a mapping, the algorithm highlights the nodes in each tree that remain unmatched. If there is a discrepancy in the source tree, its token is categorized as deleted. Conversely, if a discrepancy arises in the target tree, it is labeled as an 62 5.2. ALLOY4FUN IMPLEMENTATION addition. A visual representation of the resultant mapping is illustrated in Figure 29, with deleted nodes indicated in red and added nodes in green. The TED corresponds to the number of nodes that have been added or deleted between the two trees. In our example, this value is 3. Figure 29: Visualization of a tree difference mapping Policy Computation In this step, our program utilizes the configured policy parameters, which are included with the computation request, to calculate the desired hint model for the challenge. The algorithm itself is a translation of the Algorithm 1into Java, which is designed to process every data point from Java Typed objects. As such, our neutral value and objective parameters are defined using a double and an enumeration, respectively. The policy rule, on the other hand, is defined by a class hierarchy, implementing a Composite Design Pattern. It consists of a super-class named PolicyRule, which has three sub-classes: Constant,Var, and Binary. The super-class defines two abstract methods. The first method, normalizeByGraph, is designed to standardize the rule’s parameters according to a specified graph. The second method, apply, plays a crucial role in executing the defined rule on the provided edge and states. While the PolicyRule defines how to handle the specified rule, its actual behavior is implemented by its sub-classes. The Constant class represents a constant numerical value that cannot be normalized and simply provides its value upon application. Next, the Var class is defined by an attribute reference. When invoked for normalization, this object retrieves the maximum and minimum values of its target. Consequently, when the object is applied to a state or edge, it returns the value of the attribute normalized between 0 and 1 by the considering these limits. Finally, we have the Binary object, which can apply one of six types of binary operations (+,−,×,/,𝑚𝑖𝑛,𝑚𝑎𝑥) to its two sub-rules. Its normalization process is defined by the normalization of its sub-formulas. Each one of these classes can be serialized and deserialized as a JSON, with the use of a discriminator field named "type" created using the Jackson project. Therefore, front-end services like Meteor can effortlessly communicate each rule using 63 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT these objects. An example of this object in JSON format is shown in Listing 5.6, which depicts the rule 1+𝑆𝐶𝑂𝑅𝐸. 1{ 2"type":"binary", 3"operator":"+", 4"left": {"type":"constant","value":1.0}, 5"right":{"type":"var","var":"SCORE"} 6} Listing 5.6: Policy rule as a JSON object 5.2.5 Updated Database Schema As result of our development, we have expanded the original MongoDB database schema, resulting in the creation of four new collections that store the data described in the previous sections. In this section, our primary focus is to provide a detailed description of the scheme and data formats of these new collections, described in Tables 10,11,12, and 13. Graph Field Format Optional Example Description _id ObjectId NO 64b9433022472102a170f762 Object Identifier name String YES Instagram-inv2 Name of graph, (usually the exercise and challenge names) policy Object YES { "count": 658 "time": 2.4176935 } A performance summary of the policy computation, including its final submission count and computation time parsing Object YES { "dkZH6HJNQNLLDX6Aj":{ "count": 659 "time": 45.6081762 } } A performance summary of the ingestion process, associating each exercise with its submission count and parsing time Table 10: Dictionary of the collection Graph Challenge Field Format Optional Example Description _id ObjectId NO 64b9433022472102a170f76a Object Identifier model_id String NO dkZH6HJNQNLLDX6Aj Reference to the model exercise graph_id ObjectId NO 64b9433022472102a170f762 Reference to the submission graph end_offset Int32 NO 8Maximum offset the command can have from the end of the model cmd_n String NO inv1Ok Name of the challenge’s command targetFunctions Array NO ["inv1"] List of functions of the challenge Table 11: Dictionary of the collection Challenge 64 5.2. ALLOY4FUN IMPLEMENTATION Node Field Format Optional Example Description _id ObjectId NO 64b9433022472102a170f762 Object Identifier graph_id ObjectId NO 64b9433022472102a170f831 Reference to the submission graph formula Object NO { "inv1" : "no Trash" } Mapping from each managed function to the respective formula valid Boolean NO false Whether the formula was correct visits Int32 NO 52 Number of submissions which specified this formula leaves Int32 NO 45 Number of modifications applied to the formula (out-edge count) hopDistance Int32 YES 4Minimum distance to a solution complexity Double YES 120 Complexity of the formula score Double YES 97.568779 Computed policy score of the node witness String YES nuWnon2d7N7N7ZFvw Reference to a model specifying this node’s formula Table 12: Dictionary of the collection Node Edge Field Format Optional Example Description _id ObjectId NO 64c14e95129a556f2555df88 Object Identifier graph_id ObjectId NO 64c14e91129a556f2555dcdf Reference to the submission graph origin ObjectId NO 64c14e95129a556f2555df6b Origin node reference destination ObjectId NO 64c14e95129a556f2555df83 Destination node reference count Int32 NO 3Number of edge crossings editDistance Double YES 13.0Edit distance between the origin and destination formulas policy Boolean YES true Whether the edge is a part of the hint model Table 13: Dictionary of the collection Edge To communicate with the new data we have defined a CRUD repository for each collection with the use of Quarkus ’s Panache library for MongoDB. This package simplifies the development process by providing an intuitive querying system without the processes associated with managing the MongoDB client. To take advantage of this tool we must first define our data models as inheritors of the PanacheMongoEntity or one of its parent classes. As a result, each model will be presented with a series of methods used to issue queries alongside the required processes used to manage the model’s _id field. Afterwards the user can declare each query within the model’s respective repository, defined by the interface PanacheMongoRepository. A simple example of this construct can be found in Listing 5.7, were we present a snippet of the Challenge repository containing two queries. Both of these queries use the find method of Panache to declare a MongoDB match query, which has the purpose of retrieving Challenge objects based on the conditions provided within its body. The first query (findByModelIdAndCmdN) has the purpose of restricting the retrieved Challenge by their "model_id" and "cmd_n" fields. It implements its body using a query language implemented 65 CHAPTER 5. ALLOY SPECIFICATION ASSISTANT by Panache. It is a simple language to read and process, but it does not support the complete array of features of MongoDB. These unmet features can still be called upon with objects that can format to Binary Javascript Object Notation (BSON) such as the Document object. This is the case for the second query (streamByModelIdIn), where the provided object declares the body {"model_id":{$in:[...] }}, that has the purpose of retrieving any object where the field "model_id" is contained within the provided collection. After specifying the query and its respective body, we finish by declaring how we want the information delivered to our application. We can choose to retrieve only the first object found (firstResult()), have it packaged as a Java Stream or List (stream(), list()), have it delivered across pages (page()), among others. 1@ApplicationScoped � 2public class ChallengeRepository implements PanacheMongoRepository<Challenge> { 3 4public Challenge findByModelIdAndCmdN(String model_id, String cmd_n) { 5return find("model_id = ?1 and cmd_n = ?2", model_id, cmd_n).firstResult(); 6 } 7 8public Stream<Challenge> streamByModelIdIn(List<String> model_ids) { 9return find(new Document("model_id",new Document("$in", model_ids))).stream(); 10 } 11 ... 12 } Listing 5.7: Challenge repository 66 6 Evaluation The primary objective of any hint generating system is to provide valuable and contextually relevant clues or suggestions to assist individuals in solving problems, overcoming challenges, or improving their performance in various tasks. Our data-driven system fulfills this task by mining hint suggestions from historical data that describes the decisions taken by multiple users. As explained throughout the previous chapter, this process has some compromises between the system capability for presenting hints (availability) and the effectiveness of hints in helping the user understand and solve the problem at hand (quality). As a result, to evaluate our system we must evaluate both these aspects. We can use a broad range of quantitative and qualitative assessments in order to precisely measure both the availability and quality of our system. Due to its complexity, the qualitative assessment was not planned to be conducted during the thesis and is expected to be performed in future work. As a result, our current evaluation focus mostly on the quantitative aspects. More specifically, our evaluation aimed at answering the following research questions: RQ1 Is SpecAssistant viable for hint generation? RQ2 Is it viable to frequently update the submission graphs of SpecAssistant? RQ3 To what extent does the incorporation of mutated formulas affects the performance? RQ4 How does SpecAssistant performance stacks up against other alternatives? To answer these questions, we employed a range of data-mining validation and testing techniques. These techniques encompassed data pre-processing, data-set splitting, cross-validation across various models, as well as a superficial overfitting and underfitting examination of ours models. 6.1 Data-set Partitioning The first step in our evaluation was to divide the existing submission data into two distinct subsets: the training data-set, which was used to build the hint models, and the testing data-set, which was used to 67 CHAPTER 6. EVALUATION measure their effectiveness. To obtain meaningful results, it is imperative that these samples generalize the entire system’s behavior. If we fail to generalize the training data, the biased model will likely perform worse. Conversely, if we fail to generalize the testing data, our results may overlook some user behaviors, which would result in biased results. The Alloy4Fun data-set [22], our targeted data-set, primarily consists of derivation trees where each sub-tree of the root corresponds to a distinct user attempt. These were generated by university students as direct result of their participation in academic courses teaching Alloy at the University of Minho (UM) and University of Porto (UP), and include nearly 70000 syntactically correct submissions. In particular, the Alloy4Fun data-set encompasses four academic years spanning from the fall of 2019 to the summer of 2023. For the academic years of 2019/2020 and 2020/2021, the data originated from a course that introduced a variety of challenges to two classes of around 20 students, including “Trash FOL”, “Classroom FOL”, “Trash RL”, “Classroom RL”, “Graphs”, ”LTS”, “Production Line v1”, and “CV”. In contrast, during the academic years 2021/2022 and 2022/2023, the data resulted from a different course that exposed two classes of around 210 students to new challenges, namely “Production Line v2/v3”, “Train Station”, “Courses”, and “Social Network”. Despite the population size in the latter years being nearly 11 times larger than in the former years, the number of submissions was only the double, because in the latter course Alloy was taught for a short period only. One noteworthy aspect of the exercises is that it that they are publicly available. Therefore, it is possible that a small number of submissions could have also come from external users. This could potentially explain the data we have for older exercises, with submissions beyond their original class time-frames. The distribution of submissions can be observed in Figure 30. Figure 30: Number of syntactically correct submissions in each exercise We focused on randomly splitting the user attempts, i.e. the direct sub-trees of the root of each derivation tree, based on the number of valid submissions each one can contribute to each submission 68 6.2. BENCHMARKING graph. The partitioning process begins by calculating the number of valid submissions per challenge in each sub-tree of an exercise. Then, it randomly selects sub-trees for the smallest partition (in our case, the testing data-set), continuing this selection process until the sum of its valid submissions surpasses the predefined split ratio. In our implementation, we designated 70% of data for training and 30% for testing. Because each sample is inherently random, we believe that our results will be less biased and can be generalized. 6.2 Benchmarking After establishing each partition, every challenge of the training data-set was put through our hint model computation process. As a result, our system generated a hint model for every challenge defined across each exercise. Subsequently, we individually tested each invalid submission within the testing data-set against our hint generation technique and TAR, the previous hint generation system of Alloy4Fun. Each result was stored separately in a database collection named “Test” described in Table 14. This collection outlines specifications on each tested submission based on the type of test performed, which is described by the respective tool (SpecAssistant, TAR), policy rules and potential augmentations, such as the incorporation of mutated formulas. The specifications themselves include a number of useful data points, such as the test’s success, the elapsed time, the chosen state, among others. After the benchmarking it accommodated more than 200000 distinct entries. This procedure to handle benchmark data gave us flexibility in conducting the evaluation. From an execution standpoint, it allowed us to consistently validate and possibly repeat tests without compromising the remaining data, and from an analytical standpoint, it allows us to precisely tailor our data view to each research question without losses of information. Field Format Optional Example Description _id.model_id String NO uCFT6ci2br98QhWF7 Identification of the request’s model _id.type String NO "TED-SPEC" Type of benchmark preformed data.success Boolean NO true Whether the benchmark generated a hint data.time Double NO 0.2409658 Elapsed Time in seconds data.match ObjectId Yes 64c14e91129a556f2555d0023 Reference for the matched state data.next ObjectId Yes 64c14e91129a556f25558450 Reference for the next state data.edge ObjectId Yes 64c14e91129a556f25551182 Reference for the corresponding transition object between the 𝑚𝑎𝑡𝑐ℎ and 𝑛𝑒𝑥𝑡 graphId ObjectId Yes 65043b32364fce46dcb96123 The benchmark’s submission model Table 14: Dictionary of the collection Test Each individual test was given a timeout of one minute. The rationale behind this decision was based on the expectation that any hint generation technique exceeding this time would severely compromise the 69 CHAPTER 7. CONCLUSIONS AND FUTURE WORK least 33% of invalid submissions in the testing data-set, a ratio that can be improved to 50% through the integration of formula mutation techniques into the process. In conclusion, we believe SpecAssistant has fulfilled the objectives for this thesis. We leveraged data-driven methods to create a hint generation system that is capable of instantly and effectively offer assistance to users by leveraging data collected from peers in the past. This development of SpecAssistant was challenging, mostly because of the nature of the available historical data. The primary objective of a hint system is to offer suggestions that indeed help users reach valid solutions and have a positive impact on learning. However, there is no guaranty that historical peer data is the best source of hints for that. We attempted to mitigate this by allowing challenge developers to customize the policy selection rules, however the problem may still persist. On a more technical perspective, Alloy’s Analyzer also proved difficult to work with, as its compiler and AST formats are not specially suited for our normalization and parsing procedures. 7.2 Future Work We have identified three aspects in which our work can be improved: the evaluation process, the implementation, and the hint computation and delivery technique. In order to improve our evaluation, it is essential that we undertake user studies in the future. While these studies were not included in the thesis plan, they can offer invaluable insights into user behaviors when exposed to our hints. This information is essential for a comprehensive assessment of the hints’ quality, i.e. their ability to aid users in solving challenges and improve their learning. To improve SpecAssistant’s implementation, we should start by improving the underlying AST structures. As mentioned earlier, the use of Alloy Analyzer has presented us with a series of problems during the normalization process, particularly in dealing with invalid AST nodes, which led to some undesirable workarounds. A redevelopment of this structure could remove all these issues, consequently enhancing the outcomes of our AST normalization and differencing algorithms. It would also streamline other needed system improvements, such as the implementation of an Alloy parser suited for our model parsing procedures. Another possible improvement would be enhancing the way the system computes and delivers hints. Improving hint computation requires improving our current data-models. This can be achieved by either adding new attributes to be used in policy rules or by shifting from our state-based data-model to a sessionbased one (i.e. a model that generate hints from the full array submissions of a session). Improving hint deliver, requires improving the text messages that are provided with the hints. To do this we could improve our text generation technique using the rapidly evolving deep learning language models. 76 Bibliography [1] Anne Adam and Jean-Pierre H. Laurent. “LAURA, A System to Debug Student Programs”. In: Artif. Intell. 15.1-2 (1980), pp. 75–122 (cit. on p. 36). [2] Elena N. Akimova, Alexander Yu. Bersenev, Artem A. Deikov, Konstantin S. Kobylkin, Anton V. Konygin, Ilya P. Mezentsev, and Vladimir E. Misilov. “A survey on software defect prediction using deep learning”. In: Mathematics 9.11 (2021), p. 1180 (cit. on p. 34). [3] Frances E. Allen. “Control flow analysis”. In: Symposium on Compiler Optimization, UrbanaChampaign, Illinois, USA, July 27-28, 1970 . Ed. by Robert S. Northcote. ACM, 1970, pp. 1–19 (cit. on p. 48). [4] Paolo Antonucci, H.-Christian Estler, Durica Nikolic, Marco Piccioni, and Bertrand Meyer. “An Incremental Hint System For Automated Programming Assignments”. In: ACM Conference on Innovation and Technology in Computer Science Education . Ed. by Valentina Dagiene, Carsten Schulte, and Tatjana Jevsikova. ACM, 2015, pp. 320–325 (cit. on p. 38). [5] Tiffany Barnes and John C. Stamper. “Toward Automatic Hint Generation for Logic Proof Tutoring Using Historical Student Data”. In: Intelligent Tutoring Systems, 9th International Conference . Ed. by Beverly Park Woolf, Esma Aı �meur, Roger Nkambou, and Susanne P. Lajoie. Vol. 5091. Lecture Notes in Computer Science. Springer, 2008, pp. 373–382 (cit. on p. 39). [6] Sahil Bhatia and Rishabh Singh. “Automated Correction for Syntax Errors in Programming Assignments using Recurrent Neural Networks”. In: CoRR (2016) (cit. on p. 42). [7] Simón Gutiérrez Brida, Germán Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias. “BeAFix: An Automated Repair Tool for Faulty Alloy Models”. In: 36th IEEE/ACM International Conference on Automated Software Engineering . IEEE, 2021, pp. 1213– 1217 (cit. on p. 36). [8] Simón Gutiérrez Brida, Germán Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo F. Frias. “Bounded Exhaustive Search of Alloy Specification Repairs”. In: 43rd 77 BIBLIOGRAPHY IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021 . IEEE, 2021, pp. 1135–1147 (cit. on pp. 36,75). [9] Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel HerbertVoss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. “Language Models are Few-Shot Learners”. In: Advances in Neural Information Processing Systems 33 . Ed. by Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin. 2020 (cit. on p. 43). [10] Jorge Cerqueira, Alcino Cunha, and Nuno Macedo. “Timely Specification Repair for Alloy 6”. In: Software Engineering and Formal Methods - 20th International Conference . Ed. by BerndHolger Schlingloff and Ming Chai. Vol. 13550. Lecture Notes in Computer Science. Springer, 2022, pp. 288–303 (cit. on pp. 2,3,36,38,51,75). [11] Rui Couto, José Creissac Campos, Nuno Macedo, and Alcino Cunha. “Improving the Visualization of Alloy Instances”. In: 4th Workshop on Formal Integrated Development Environment . Ed. by Paolo Masci, Rosemary Monahan, and Virgile Prevosto. Vol. 284. EPTCS. 2018, pp. 37–52 (cit. on p. 17). [12] Alex Gerdes, Bastiaan Heeren, Johan Jeuring, and L. Thomas van Binsbergen. “Ask-Elle: an Adaptable Programming Tutor for Haskell Giving Automated Feedback”. In: Int. J. Artif. Intell. Educ. 27.1 (2017), pp. 65–100 (cit. on p. 38). [13] Alex Gerdes, Johan Jeuring, and Bastiaan Heeren. “Using strategies for assessment of programming exercises”. In: 41st ACM technical symposium on Computer science education . Ed. by Gary Lewandowski, Steven A. Wolfman, Thomas J. Cortina, and Ellen Lowenfeld Walker. ACM, 2010, pp. 441–445 (cit. on p. 38). [14] Rahul Gupta, Aditya Kanade, and Shirish K. Shevade. “Deep Reinforcement Learning for Programming Language Correction”. In: CoRR (2018) (cit. on p. 42). [15] Andrew Head, Elena L. Glassman, Gustavo Soares, Ryo Suzuki, Lucas Figueredo, Loris D’Antoni, and Björn Hartmann. “Writing Reusable Code Feedback at Scale with Mixed-Initiative Program Synthesis”. In: 4th ACM Conference on Learning @ Scale . Ed. by Claudia Urrea, Justin Reich, and Candace Thille. ACM, 2017, pp. 89–98 (cit. on p. 38). [16] Mark D. Hill and Michael R. Marty. “Retrospective on Amdahl’s Law in the Multicore Era”. In: Computer 50.6 (2017), pp. 12–14 (cit. on p. 72). [17] Daniel Jackson. Software Abstractions - Logic, Language, and Analysis . MIT Press, 2012 (cit. on pp. 1,2,5). 78 BIBLIOGRAPHY [32] Finn V. Jensen and Thomas D. Nielsen. “Bayesian Networks and Decision Graphs”. In: Knowl. Eng. Rev. 23.4 (2008), p. 413 (cit. on p. 48). [18] W. Lewis Johnson and Elliot Soloway. “PROUST: Knowledge-Based Program Understanding”. In: IEEE Trans. Software Eng. 11.3 (1985), pp. 267–275 (cit. on p. 36). [19] Shalini Kaleeswaran, Anirudh Santhiar, Aditya Kanade, and Sumit Gulwani. “Semi-supervised verified feedback generation”. In: 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering . Ed. by Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su. ACM, 2016, pp. 739–750 (cit. on p. 38). [20] Chao Liu, Ryen W. White, and Susan T. Dumais. “Understanding web browsing behaviors through Weibull analysis of dwell time”. In: 33rd International ACM SIGIR Conference on Research and Development in Information Retrieval . Ed. by Fabio Crestani, Stéphane Marchand-Maillet, Hsin-Hsi Chen, Efthimis N. Efthimiadis, and Jacques Savoy. ACM, 2010, pp. 379–386 (cit. on p. 70). [21] Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. “Lightweight specification and analysis of dynamic systems with rich configurations”. In: 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering . Ed. by Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su. ACM, 2016, pp. 373–383 (cit. on p. 17). [22] Nuno Macedo, Alcino Cunha, and Ana C. R. Paiva. Alloy4Fun Dataset for 2022/23 . Version EM 2022/23. Zenodo, 2023-07 (cit. on pp. 2,3,32,68,75). [23] Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, and Daniel Castro Silva. “Experiences on teaching Alloy with an automated assessment platform”. In: Sci. Comput. Program. 211 (2021), p. 102690 (cit. on pp. 2,25). [24] Mehak Maniktala, Christa Cody, Amy Isvik, Nicholas Lytle, Min Chi, and Tiffany Barnes. “Extending the Hint Factory for the assistance dilemma: A novel, data-driven HelpNeed Predictor for proactive problem-solving help”. In: CoRR (2020) (cit. on p. 40). [25] Michael L. Mauldin. “Semantic Rule Based Text Generation”. In: 10th International Conference on Computational Linguistics and 22nd Annual Meeting of the Association for Computational Linguistics . Ed. by Yorick Wilks. ACL, 1984, pp. 376–380 (cit. on p. 43). [26] Jessica McBroom, Irena Koprinska, and Kalina Yacef. “A Survey of Automated Programming Hint Generation: The HINTS Framework”. In: ACM Comput. Surv. 54.8 (2022), 172:1–172:27 (cit. on pp. 3,34). [27] Martin Monperrus. “Automatic Software Repair: A Bibliography”. In: ACM Comput. Surv. 51.1 (2018), 17:1–17:24 (cit. on pp. 2,34). [28] H. Hernan Moraldo. “An Approach for Text Steganography Based on Markov Chains”. In: CoRR (2014) (cit. on p. 43). 79 BIBLIOGRAPHY [29] Weili Nie, Nina Narodytska, and Ankit Patel. “RelGAN: Relational Generative Adversarial Networks for Text Generation”. In: 7th International Conference on Learning Representations . OpenReview.net, 2019 (cit. on p. 43). [30] Andy Oram and Greg Wilson, eds. Making Software - What Really Works, and Why We Believe It . Theory in practice. O’Reilly, 2011 (cit. on p. 1). [31] Benjamin Paaßen, Barbara Hammer, Thomas William Price, Tiffany Barnes, Sebastian Gross, and Niels Pinkwart. “The Continuous Hint Factory - Providing Hints in Vast and Sparsely Populated Edit Distance Spaces”. In: CoRR (2017) (cit. on p. 40). [33] Mateusz Pawlik and Nikolaus Augsten. “Efficient Computation of the Tree Edit Distance”. In: ACM Trans. Database Syst. 40.1 (2015), 3:1–3:40 (cit. on pp. 60,62). [34] Mateusz Pawlik and Nikolaus Augsten. “Tree edit distance: Robust and memory-efficient”. In: Inf. Syst. 56 (2016), pp. 157–173 (cit. on pp. 53,60,62). [35] Chris Piech, Mehran Sahami, Jonathan Huang, and Leonidas J. Guibas. “Autonomously Generating Hints by Inferring Problem Solving Policies”. In: 2nd Second ACM Conference on Learning @ Scale . Ed. by Gregor Kiczales, Daniel M. Russell, and Beverly P. Woolf. ACM, 2015, pp. 195–204 (cit. on p. 39). [36] Thomas W. Price, Yihuan Dong, Rui Zhi, Benjamin Paaßen, Nicholas Lytle, Veronica Cateté, and Tiffany Barnes. “A Comparison of the Quality of Data-Driven Programming Hint Generation Algorithms”. In: Int. J. Artif. Intell. Educ. 29.3 (2019), pp. 368–395 (cit. on p. 2). [37] Thomas W. Price, Rui Zhi, and Tiffany Barnes. “Hint Generation Under Uncertainty: The Effect of Hint Quality on Help-Seeking Behavior”. In: Artificial Intelligence in Education - 18th International Conference . Ed. by Elisabeth André, Ryan S. Baker, Xiangen Hu, Ma. Mercedes T. Rodrigo, and Benedict du Boulay. Vol. 10331. Lecture Notes in Computer Science. Springer, 2017, pp. 311–322 (cit. on p. 39). [38] Kelly Rivers and Kenneth R. Koedinger. “Data-Driven Hint Generation in Vast Solution Spaces: a Self-Improving Python Programming Tutor”. In: Int. J. Artif. Intell. Educ. 27.1 (2017), pp. 37–64 (cit. on pp. 2,40). [39] Higor Amario de Souza, Marcos Lordello Chaim, and Fabio Kon. “Spectrum-based Software Fault Localization: A Survey of Techniques, Advances, and Challenges”. In: CoRR (2016) (cit. on p. 36). [40] John Stamper, Tiffany Barnes, Lorrie Lehmann, and Marvin Croy. “The hint factory: Automatic generation of contextualized help for existing computer aided instruction”. In: 9th International Conference on Intelligent Tutoring Systems Young Researchers Track . 2008, pp. 71–78 (cit. on pp. 39,44). 80 BIBLIOGRAPHY [41] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. “Attention is All you Need”. In: Advances in Neural Information Processing Systems 30 . Ed. by Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett. 2017, pp. 5998–6008 (cit. on p. 43). [42] Kaiyuan Wang, Allison Sullivan, and Sarfraz Khurshid. “Automated model repair for Alloy”. In: 33rd ACM/IEEE International Conference on Automated Software Engineering . Ed. by Marianne Huchard, Christian Kästner, and Gordon Fraser. ACM, 2018, pp. 577–588 (cit. on p. 36). [43] Kaiyuan Wang, Allison Sullivan, Darko Marinov, and Sarfraz Khurshid. “Fault Localization for Declarative Models in Alloy”. In: 31st IEEE International Symposium on Software Reliability Engineering . Ed. by Marco Vieira, Henrique Madeira, Nuno Antunes, and Zheng Zheng. IEEE, 2020, pp. 391– 402 (cit. on p. 37). [44] Westley Weimer, Stephanie Forrest, Claire Le Goues, and ThanhVu Nguyen. “Automatic program repair with evolutionary computation”. In: Commun. ACM 53.5 (2010), pp. 109–116 (cit. on p. 2). [45] W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and Franz Wotawa. “A Survey on Software Fault Localization”. In: IEEE Trans. Software Eng. 42.8 (2016), pp. 707–740 (cit. on p. 36). [46] W. Eric Wong and J. Jenny Li. “An Integrated Solution for Testing and Analyzing Java Applications in an Industrial Setting”. In: 12th Asia-Pacific Software Engineering Conference . IEEE Computer Society, 2005, pp. 576–583 (cit. on p. 36). [47] Franz Wotawa. “Fault Localization Based on Dynamic Slicing and Hitting-Set Computation”. In: 10th International Conference on Quality Software . Ed. by Ji Wang, W. K. Chan, and Fei-Ching Kuo. IEEE Computer Society, 2010, pp. 161–170 (cit. on p. 36). [48] Baowen Xu, Ju Qian, Xiaofang Zhang, Zhongqiang Wu, and Lin Chen. “A brief survey of program slicing”. In: ACM SIGSOFT Softw. Eng. Notes 30.2 (2005), pp. 1–36 (cit. on p. 36). [49] Michihiro Yasunaga and Percy Liang. “Break-It-Fix-It: Unsupervised Learning for Program Repair”. In: 38th International Conference on Machine Learning . Ed. by Marina Meila and Tong Zhang. Vol. 139. Machine Learning Research. PMLR, 2021, pp. 11941–11952 (cit. on p. 42). [50] Guolong Zheng, ThanhVu Nguyen, Simón Gutiérrez Brida, Germán Regis, Marcelo F. Frias, Nazareno Aguirre, and Hamid Bagheri. “FLACK: Counterexample-Guided Fault Localization for Alloy Models”. In: 43rd IEEE/ACM International Conference on Software Engineering . IEEE, 2021, pp. 637–648 (cit. on pp. 37,75). [51] Wanrong Zhu, Zhiting Hu, and Eric P. Xing. “Text Infilling”. In: CoRR (2019) (cit. on p. 43). Thisdocumentwascreatedwiththe(pdf/Xe/Lua)L A T E XprocessorandtheNOVAthesistemplate(v6.10.5)[1].12cc90221730b8ba41bb3b1f8b517acd [1] (Cit.onp.81). 81 UMinho |2023 Henrique Neto Mining hints for fixing formal specifications