Automatic Generation of Learning Assignments for Software Engineering Formalisms Michael Steinle Bernd Westphal Department of Computer Science Department of Computer Science Albert-Ludwigs-Universität Freiburg Albert-Ludwigs-Universität Freiburg Freiburg, Germany Freiburg, Germany steinlem@informatik.uni-freiburg.de westphal@informatik.uni-freiburg.de Abstract—Creating learning or examination assignments is a languages in the context of our undergraduate introduction to re-occurring activity in the context of teaching. In particular software engineering [4]–[6]. Creating learning assignments in new examination assignments are often desired for each season this context is challenging because it is not always completely of teaching a course. In our teaching, we have observed that our creation of assignments for software engineering formalisms uses obvious that a proposed assignment is solvable. To lower certain intuitive constraints to obtain assignments at a designated the student’s cognitive load, we also prefer to use learning level of difficulty and, e.g., with particular properties to be assignments where a single artefact is supposed to, e.g., be analysed in the assignment. analysed for multiple aspects. Therefore, the artefacts for our In this work, we present an approach where we formalise learning assignments need not only be solvable but they need our (formerly intuitive) constraints and use constraint solving tools to automatically synthesise learning assignments that satisfy to equally well support multiple learning goals. Hence, simple these constraints. In our approach we leverage the fact that our mutations of existing artefacts does not provide a reliable software engineering course teaches the majority of software procedure to create new learning assignment. description languages fully formal. That is, an artefact using When creating new assignments, e.g., to not have the same such a software description language is then a mathematical tasks in each seasons or for exams, we observed that we can object for which we can give precise constraints. We demonstrate our approach on the example of learning and examination identify different levels of difficulty within the same class of assignments for the notion of determinism on decision table and learning assignments. Furthermore, we gained the impression discuss applications of our assignments synthesis procedure. that we can precisely characterise those classes of difficulty using properties of the (formal) artefacts. I. I NTRODUCTION We propose to develop an approach to (a) formalise our Learning assignments are, following Seel [1], selected and understandings of didactical aspects of learning assignments prepared learning objects with the aim to initiate, control, on software description languages (like solvability, learning and organise learning processes. Following Renkl [2], learning goals, and level of difficulty) and (b) use existing procedures assignments in this sense are used to learn and practice knowl- and tools to automatically generate learning assignments with edge and capabilities. Renkl observes that different learning desired properties. In this article, we report on an investigation assignments can lead to comparable acquisition of knowledge of the feasibility of this approach. To this end, we have and that ‘well meant but badly done’ stimulations for thought developed, implemented, and evaluated a synthesis procedure and embeddings of learning assignment into teaching contexts for the formalism of decision tables. can disturb the learning process. Learning assignments have thus to focus on the knowledge or capability to learn, and be The article is structured as follows. In Section II, we illus- designed for and embedded into the teaching context. trate our approach on the example of learning assignment for The question what makes a learning assignment a good basic calculus. Section III recalls decision tables and gives an learning assignment in general and how to use certain learning example of an exam task that we would like to automatically assignments in teaching is in our perception still actively re- generate. Sections IV and V describe our synthesis procedure searched in didactics. A requirement for most learning assign- and preliminary empirical results, Sections VI and VII discuss ments will be that they are solvable. Another requirement is our results and related work, and Section VIII concludes. that learning assignments match the knowledge and experience of the learners. Advanced learners hardly benefit from easy II. A N A NALOGY: L EARNING A SSIGNMENTS FOR learning assignments on the competence level ‘remember’ [3] A DDITION WITH C ARRY while beginners may be frustrated by difficult assignments on In this section, we want to illustrate the proposed approach the competence level ‘create’ [3]. on an example of learning assignments for elementary school In this work, we consider the problem of creating learning arithmetic, namely ‘paper & pencil’ addition with carry of assignments with the purpose of practising analysis procedures two positive decimal numbers. As a teacher, one may want (competence level ‘apply’) for formal software specification to present learning assignments with an increasing level of S. Krusche, S. Wagner (Hrsg.): SEUH 2020 61 Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). T : decision table r1 ··· rn 1234 123 4 12 3 4 xn · · · x1 x0 c1 description of condition c1 v1,1 ··· v1,n + 625 + 6 216 +1 81716 +cn+1 yncn · · · c2 y1c1 y0 1859 186 0 21 1 0 zn+1 zn · · · z1 z0 ... ... .. . .. . .. . (a) (b) (c) (d) cm description of condition cm vm,1 ··· vm,n a1 description of action a1 w1,1 ··· w1,n TABLE I: Addition with carry can be simple, e.g. (a), inter- . .. . .. . .. .. . .. . mediate, e.g. (b), or advanced, e.g. (c). Case (d) provides an ak description of action ak wk,1 ··· wk,n abstract formal view on the task of adding two numbers. Fig. 1: Concrete syntax of decision tables. difficulty to let pupils practice the routine of ‘paper & pencil’ addition without carry before moving to the general case, and of the set {−, ×, ∗}, and the bottom k entries of a rule (the possibly in between having some learning assignment with effect) w1,i , . . . , wk,i are from the set {−, ×}. That is, ‘∗’ may exactly one carry. So the teacher may have identified the not occur in an effect of a well-formed decision table. following three levels of difficulty: Easy tasks where no carry The semantics of decision tables is given by a function is needed (cf. Table Ia), intermediate level tasks where exactly F that assigns to each rule r in T a propositional logic one carry is needed (cf. Table Ib), and the general case where formula over C and A. Given premise (v1 , . . . , vm ) and effect one carry may cause a subsequent carry (cf. Table Ic). (w1 , . . . , wk ) of r, the semantics function is defined as To create new learning assignments for addition, e.g., in an V V F (r) := 1≤i≤m F (vi , ci ) ∧ 1≤j≤k F (wj , aj ) (1) e-learning tool, the teacher could firstly formalise the addition | {z } | {z } of two n-digit decimal numbers as shown in Table Id. The =:Fpre (r) =:Feff (r) task of adding two numbers in decimal representation consists where F := {(×, x) 7→ x, (−, x) 7→ ¬x, (∗, x) 7→ true}. of two numbers x and y with their decimal representation For a discussion of the use of this semantics in requirements xn , . . . , x0 and yn , . . . , y0 . The first carry, caused by adding engineering we refer the reader to [4], [5]. the least significant digits x0 and y0 , is c1 , which has value 1 We can formally define different properties of decision if and only if x0 + y0 > 10, and value 0 otherwise. tables that are useful in requirements engineering such as Viewing addition tasks as mathematical objects, the teacher completeness, consistency, existence of useless rules, etc.. could secondly precisely characterise the sets of addition tasks For the purpose of this article it is sufficient to provide the corresponding to the levels of difficulty described above. An definition of (non-)determinism. A decision table T is called easy addition task is one where all carries ci , 1 ≤ i ≤ n, deterministic, if and only if for all different rules r1 and r2 in have value 0. Intermediate level and general case tasks can T , their premise formulae are (logically) disjoint, i.e. if be characterised similarly. With this formalisation of learning assignments and the level of difficulty, the teacher could finally ∀ r1 6= r2 ∈ T • |= ¬(Fpre (r1 ) ∧ Fpre (r2 )). (2) use any integer constraint solver that supports addition and comparison to obtain tasks that are, e.g., in the class of easy Intuitively, a decision table is deterministic if and only if there tasks: We are asking for a solution to the constraint solving is no valuation of the conditions in C that satisfies the premise problem that the open symbols xi and yi are assigned values formulae of two different rules. between 0 and 9 (decimal digits) such that the valuation To practice the analysis of decision tables for determinism, satisfies the constraint that all carries remain 0. Note that the learning assignments can start on the competence level of number of digits n is a parameter of the constraint solving ‘apply’. In the course, we present a truth table-based approach problem with which the teacher can control, e.g., the time it to decide determinism for a given decision table: For each takes to solve a task as an additional teaching aspect. valuation of the observables in C note down which rules’ That is, we propose to formalise didactical intents on premises are satisfied. The table is deterministic if and only if learning assignments that involve mathematical objects (such no valuation satisfies more than one rules’ premises. as addition tasks) in form of constraints and to use appro- A proof of determinism needs an argument on the rules’ priate constraint solving techniques to automatically generate premise formulae (e.g., the truth table), while a proof of learning assignments for a given intent. non-determinism strictly speaking only needs one valuation III. D ECISION TABLES and the argument that this valuation satisfies the premise formulae of two different rules. Hence the workload for a Decision tables are a simple software engineering formalism given deterministic table can be higher (construction of truth that can, e.g., be used to formalise requirements [7], [8]. table) than for a given non-deterministic table (give a counter- Formally, a decision table T is an (m + k) × n matrix with example as explained above). Thus in the role of a teacher, entries from the set {−, ×, ∗}. The top m rows correspond to we often want to control whether the decision table given as conditions c1 , . . . , cm from the set of conditions C, and the a learning assignment is deterministic or non-deterministic. bottom k rows to actions a1 , . . . , ak from the set of actions A, which is disjoint from C. Columns are called rules. The top Figure 2 shows a simplified example of an exam task on m entries of a rule (the premise) v1,i , . . . , vm,i are elements decision tables. The Subtask (1) tests that students are able S. Krusche, S. Wagner (Hrsg.): SEUH 2020 62 T r1 r2 r3 1) Give the rule formulae for r1 , r2 , r3 . learning assignment decision table c1 × × − specification 2) It is claimed that T is deterministic. c2 × − ∗ (1) Prove this claim. c3 − × ∗ (3) constants formulae a1 × − − 3) Does T have a useless rule? a2 − × − Prove your claim. (2) model Fig. 2: Example exercise task on decision tables. Fig. 3: Intermediate artefacts of decision table task generation. to use the semantics function (competence level ‘apply’). some of these further constraints at the end of this section. The This kind of task is obviously solvable for each well-formed basic idea of our procedure to generate deterministic decision decision table, yet to be most useful, one may wish to provide tables is to reduce the generation problem to an SMT-problem. a table that comprises all possible entries. Subtask (2) tests SAT modulo theory (SMT) is a natural problem domain due competences in applying a particular proof strategy for a to the logical nature of the decision table semantics. particular decision table property. This subtask is only solvable Finite sets C and A of conditions and actions and a (or at least not strongly confusing) if the considered decision number n ∈ N0 of rules constitute the learning assignment table has the claimed property. Subtask (3) tests competences specification (cf. Figure 3). In Step (1), we define the signature on analysing a decision table for whether it has a certain of the SMT-problem as a set of constants, one constant per property such as useless rules (hence touching the competence decision table cell. Over this signature, we generate formulae level ‘analyse’). Depending on the correct answer, different that, e.g., specify the allowed content of decision table cells proof strategies apply that may need a significantly different and also the determinism property. In Step (2), an SMT-solver amount of time to solve. One may aim at a decision table for generates a model, i.e., an interpretation of the signature such which Subtasks (2) and (3) need different proof strategies so to that the considered formulae hold under this interpretation (if test both and to limit the necessary effort. Note that using only and only if a deterministic decision table of the desired size one decision table lowers the cognitive load for the learners exists). In Step (3), we interpret the model as a decision table. since only one artefact needs to be read and the learners can To obtain a second, different deterministic decision table, the concentrate on the analysis tasks as such. model from the previous run can be encoded as an additional Creating learning assignments as shown in Figure 2 is formula. Then, taking Step (1) again, we obtain a model that difficult because multiple constraints need to be considered encodes a different deterministic decision table (if and only if together. A change in one cell of the decision table may a second decision table of the desired form exists). unintentionally render the table non-deterministic, or make the The idea of the encoding is as follows: For each premise analysis for determinism too easy (for example by having two cell of the desired decision table, there is one constant in the identical rules). To simplify the process of creating learning signature that can take values ‘×’, ‘−’, or ‘∗’, and similarly assignments or exam tasks on decision tables, we propose for each effect cell, then with possible values ‘×’ or ‘−’. So to exploit the fact that decision tables are introduced as to obtain a table over m conditions and k actions with n rules mathematical objects in our course. Properties of decision (cf. Figure 1), we would have constants v1,1 , . . . , vm,n and tables, such as determinism, are formally defined and thus can w1,1 , . . . , wk,n . Now any model of the trivial formula ‘true’ be used as constraints in a synthesis procedure. In addition, we as returned by an SMT-solver is already an encoding of a well- propose to formalise our didactical understanding of classes of formed decision table: The entry of cell, e.g., vi,j takes the learning assignments on decision tables. For example, that an interpretation of the constant vi,j , which is ‘×’, ‘−’, or ‘∗’. analysis for non-determinism is trivial if there are two identical Providing a constraint that corresponds to determinism is rules in the table. Other examples aim at the corner cases of a bit more involved. Firstly, the definition of determinism the definition of determinism from the course and we may (cf. (2)) refers to a fixed decision table with fixed premise want to leave out these cases in beginner’s exercises. The task formulae. For decision table generation, we need a formula to create, e.g., a complete decision table of a particular size that refers to the decision table as encoded by the constants then reduces to a mathematical constraint solving problem. vi,j and wi,j . Secondly, the definition of determinism refers to validity of propositional formulae by using the validity IV. G ENERATING L EARNING A SSIGNMENTS ON operator ‘|=’ (read: for each valuation of the conditions in C, D ETERMINISTIC D ECISION TABLES the negation of two different rules’ premise formula evaluates In the following, we outline a procedure to generate de- to true). Such a validity operator is usually not directly terministic decision tables of a specified size. We focus available in SMT-solvers. on deterministic decision tables. Non-deterministic decision We observe that the premise formula of a rule r in a decision tables are the dual case (we negate one of the learning table is obtained using the helper function F . Function F assignment creation constraints), yet to be useful learning basically says, that a given valuation σ : C → {0, 1} of the assignments, non-deterministic decision tables need further conditions in C is enabling the i-th cell (in the row of condition didactic constraints, e.g., on the level of difficulty. We discuss ci ) of the j-th rule if and only if this cell holds symbol ‘×’ and S. Krusche, S. Wagner (Hrsg.): SEUH 2020 63 is elapsed time (blue); the total user time (yellow) grows 300 30 t/s t/s faster because the underlying solver effectively uses multi-core 250 25 systems. The top graph shows the time needed to generate one 200 20 decision table of size (n+n)×n (n conditions and actions, and 150 15 n rules). For values of n up to 10, the runtime is in the order 100 9 of seconds. Hence generating decision tables for our exercises 50 5 and exams is well feasible, because our tasks usually have 3 to 5 conditions, about 3 actions, and not more than 7 rules. 2 3 4 5 6 7 8 9 10 11 12 13 n 1 5 10 15 20 N Working on larger decision tables in ‘paper & pencil’ style is (a) Generation of one decision (b) Generation of a new bunch of 100 table of size (n + n) × n. decision tables of size (3 + 3) × 3. in our opinion not supporting the learning but just tedious. One use case that we envision for our procedure is to Fig. 4: Runtimes for two kinds of decision table generation generate bunches of decision tables as task candidates for tasks (: user time, : elapsed time, : kernel time). the teacher to choose from. The bottom graph in Figure 4 shows that the time needed for generating bunches of 100 decision tables for n = 3 is in average about half a second. An σ(ci ) = 1, or this cell holds symbol ‘−’ and σ(ci ) = 0, or this inspection of the bunches shows that using SMTInterpol has cell holds symbol ‘∗’ (“don’t care”). In the SMT-encoding, the the effect that the tables in the bunches do not feel too regular symbol in “this cell” is given by the value of constant vi,j , (i.e., not like a mere enumeration of decision tables) and that hence the equivalence stated above corresponds to the formula we do not get too many symmetric decision tables. Still, we Gi,j := (vi,j = × ∧ ci ) ∨ (vi,j = − ∧ ¬ci ) ∨ (vi,j = ∗) (3) plan to give teachers the possibility to refine the specification, e.g., to limit the number of ‘∗’ symbols (the fewer ‘∗’ symbols over a logical variable ci . Formula (3) holds if and only if the a decision table has, the more obvious the determinism). current value of ci enables the currently considered entry of the decision table cell as given by the interpretation of constant VI. D ISCUSSION vi,j . A rule r is enabled by a valuation σ if and only if σ satisfies Fpre (r), which is the case if and only if σ enables The previous sections show that it is possible to synthe- all cells that constitute the premise of r. Hence the formula sise learning assignments for software description formalisms Gj := G1,j ∧ · · · ∧ Gm,j corresponds to the enabledness of (viewed as mathematical objects) that satisfy certain precisely rule rj (where the rule is given by the current interpretation stated constraints. These constraints can be very generic, of the vi,j ). So to obtain a deterministic decision table, we in our case the full power of logic over some theory is conjoin the overall formula available. Here we see a strong potential of our approach: We formalise conditions that make learning assignments good G := ∀ 1 ≤ j1 6= j2 ≤ n ∀ c1 , . . . , cm • ¬(Gj1 ∧ Gj2 ) (4) learning assignments, relative to the teacher’s intention and the to the SMT-problem. The particular SMT-problem is now to students’ situation in the same way as sketched for addition provide an interpretation of the signature (i.e., the constants tasks in the introduction. vi,j and wi,j ) such that G is satisfied. For details of the In the case of decision tables, we have for example ob- encoding, we refer the reader to [9]. Note that all quantifiers served that the tasks that we create anew each season for the in G (cf. (4)) range over finite domains and can hence be exercises and the exam follow certain principles. One is of expanded into a finite conjunction. The expanded formula course the size of the tables (as already considered in our is then treatable by efficient SMT-solvers for quantifier-free generation procedure). With non-deterministic decision tables, theories. The unfolding grows in the number of conditions we do consider more aspects. For example, a table where and desired rules. Yet, since we aim to create decision tables two rules are just copies of each other could be too easy that are supposed to be solved by humans, we expect that the to analyse. We can immediately formalise that there are no unfolding of G into a quantifier-free formula is usually still two identical rules and add that constraint to the learning well-treatable by today’s SMT-solvers. Prelimary evaluation assignment specification. Then, our definition of determinism results as reported below confirm our expectation. has the particularity that actions are not considered. So if two rules can be enabled by one valuation of the conditions V. E VALUATION and have the same effect, they are still (by definition) non- We have implemented our approach using the API of the deterministic. A table with all different effects could be a SMT-solver SMTInterpol [10]. We imagine to offer to teachers good choice when starting with non-deterministic tables, yet a choice of decision tables for a given learning assignment the corner-case of overlapping premise and equivalent effect specification, and the possibility to refine the specification, should be presented to the advanced learner. Again, we can e.g., to limit the number of ‘∗’ symbols (the fewer ‘∗’ symbols formalise both cases as constraints. Furthermore, an analysis a decision table has, the more obvious the determinism). for non-determinism could be too easy if there are too many Figure 4 shows the runtime of decision table generation ‘∗’ symbols in the table, so we may want to add a constraint using our implementation. The practically most relevant graph that limits the number of ‘∗’ symbols overall, or just per rule. S. Krusche, S. Wagner (Hrsg.): SEUH 2020 64 The same applies to other properties of decision tables, such provide a procedure to generate problems that ask to construct as completeness, consistency, presence of useless rules, etc.. a DFA that accepts a certain language from a set of so-called Once we have established a set of constraints that can be seed problems. They propose a metric of difficulty based on added to learning assignment generation runs, there are mani- number of states, depth, and number of counter-examples used fold applications. The most obvious application is to generate by a learning algorithm. exercises or exam tasks tailored to a particular teaching or Our approach can be seen to take one step back since we testing goal (cf. Figure 2). It is easy to embed our decision feel that teaching of software description languages is not yet table synthesis procedure into a tool where a teacher only as well-researched as, e.g., geometry or algebra. We put the selects the kind of task to obtain a task statement and a teachers’ understanding of learning assignments first and want matching decision table. We envision a tool that presents a to provide problem encodings such that teachers can formalise selection of tasks to teachers. We feel that the teacher needs their understanding of problem classes and have complete to decide and should not blindly rely on a tool. The experience control over generated problems. from our experiments is that a set of 10 (or even 100) decision VIII. C ONCLUSION tables usually includes many examples of good exercises. Having decision tables available in machine readable form We have presented a logic-based approach to characterise allows us to generate much of the necessary material automat- and synthesise learning assignments for a subset of the formal ically, including correction schemes and slides for tutorial ses- software description language of decision tables. A first eval- sions. In tutorials that discuss non-determinism, there could be uation shows that our procedure quickly generates problems overlays for the case with disjoint effects and the corner-case of the size needed for ‘paper & pencil’ tasks. We argue to with equivalent effects. Further applications could be to offer put computer science teachers into a prominent position when an e-learning tool, e.g., a website or a mobile application, that generating learning assignments: A formalisation of software generates new learning assignments for a student-controlled engineering problems allows us teachers to formalise and or heuristically adapted level of difficulty. Note that we want investigate our understanding of good learning assignments. to address learning activities that focus on the formalisms Future research includes to extend the set of supported and analysis procedures as such. To this end, it is perfectly learning assignments (also for different formalisms), and fur- adequate that the generated decision tables do not model an ther research into the nature of instructionally good learning existing system. In our opinion, students should not firstly assignments and their formal characterisation. assess the pragmatics of a decision table model, or try to look R EFERENCES out for non-determinism in their imagination of the modelled [1] N. M. Seel, Lernaufgaben und Lernprozesse, ser. Studienbuch system, but they should learn to rely on the purely abstract Pädagogik. Stuttgart: W. Kohlhammer, 1981. application of analysis procedures. [2] A. Renkl, “Lernaufgaben zum Erwerb prinzipienbasierter Fertigkeiten,” From our experience with exercises for our software en- in Lernaufgaben entwickeln, bearbeiten und überprüfen, ser. Fachdidak- tische Forschungen, vol. 6, 2014, pp. 12–22. gineering course, we anticipate that our approach can be [3] L. W. Anderson, D. R. Krathwohl et al., Eds., A Revision of Bloom’s extended to class diagrams, object diagrams, OCL constraints Taxonomy of Educational Objectives. Longman, 2001. together with class diagrams, and even Statechart-like for- [4] B. Westphal, “An undergraduate requirements engineering curriculum with formal methods,” in REET@RE, M. Moshirpour, M. Moussavi, malisms. It is an open research question which synthesis A. M. Grubb, S. Gregory, and B. Far, Eds. IEEE, 2018, pp. 1–10. procedure is adequate for which formalism. [5] ——, “Formale methoden in der Softwaretechnik-Vorlesung,” in SEUH, V. Thurner et al., Eds., vol. 2358. CEUR-WS.org, 2019, pp. 21–33. VII. R ELATED W ORK [6] ——, “Teaching software modelling in an undergraduate introduction to software engineering,” in EduSymp. IEEE, 2019, pp. 0–0. The idea to generate learning assignments is not new. [7] H. Balzert, Lehrbuch der Softwaretechnik: Basiskonzepte und Require- worksheets for elementary school arithmetic are generated ments Engineering, 3rd ed. Spektrum, 2009. [8] ——, Lehrbuch der Softwaretechnik: Entwurf, Implementierung, Instal- randomly (e.g., [11]) and, e.g., [12] use mutations of templates lation, Betrieb, 3rd ed. Spektrum, 2011. for state-machine problems. Singh et al. [13] infer a set of [9] M. Steinle, “Automatische Generierung von Lernaufgaben für Entschei- similar problems on algebraic equivalence proofs from an dungstabellen,” 2019, B. Sc. thesis, Universität Freiburg. [10] J. Christ, J. Hoenicke, and A. Nutz, “SMTInterpol: An Interpolating abstraction of a given problem into a so-called query, where SMT Solver,” in SPIN, ser. LNCS, A. F. Donaldson and D. Parker, queries can also serve to give learning assignment specifica- Eds., vol. 7385. Springer, 2012, pp. 248–254. tions. Similarly, Ahmed et al. [14] propose to abstract natural [11] mathworksheetwizard.com. (2019) [12] D. Sadigh, S. A. Seshia, and M. Gupta, “Automating exercise generation: deduction proofs and to then generate comparable problems. a step towards meeting the MOOC challenge for embedded systems,” Alvin et al. [15] targets the synthesis of geometry problems in WESE, P. Marwedel, Ed. ACM, 2012, p. 2. from an example with a set of properties to be preserved. [13] R. Singh, S. Gulwani, and S. K. Rajamani, “Automatically generating algebra problems,” in AAAI, 2012. They suggest that proof width and length, and the number [14] U. Z. Ahmed, S. Gulwani et al., “Automatically generating problems of deductive steps are useful metrics to control the synthesis. and solutions for natural deduction,” in IJCAI, 2013, pp. 1968–1975. Andersen et al. [16] propose to characterise the difficulty of [15] C. Alvin, S. Gulwani, R. Majumdar, and S. Mukhopadhyay, “Automatic synthesis of geometry problems for an intelligent tutoring system,” problems by the execution trace of a procedure that solves the CoRR, vol. abs/1510.08525, 2015. problem, and to synthesise problems along such a procedure [16] E. Andersen et al., “A trace-based framework for analyzing and synthe- to obtain a controlled learning progression. Sadigh et al. [12] sizing educational progressions,” in SIGCHI. ACM, 2013, pp. 773–782. S. Krusche, S. Wagner (Hrsg.): SEUH 2020 65