-Creating learning or examination assignments is a re-occurring activity in the context of teaching. In particular new examination assignments are often desired for each season of teaching a course. In our teaching, we have observed that our creation of assignments for software engineering formalisms uses certain intuitive constraints to obtain assignments at a designated level of difficulty and, e.g., with particular properties to be analysed in the assignment. In this work, we present an approach where we formalise our (formerly intuitive) constraints and use constraint solving tools to automatically synthesise learning assignments that satisfy these constraints. In our approach we leverage the fact that our software engineering course teaches the majority of software description languages fully formal. That is, an artefact using such a software description language is then a mathematical object for which we can give precise constraints. We demonstrate our approach on the example of learning and examination assignments for the notion of determinism on decision table and discuss applications of our assignments synthesis procedure.
Learning assignments are, following Seel [
The question what makes a learning assignment a good
learning assignment in general and how to use certain learning
assignments in teaching is in our perception still actively
researched in didactics. A requirement for most learning
assignments will be that they are solvable. Another requirement is
that learning assignments match the knowledge and experience
of the learners. Advanced learners hardly benefit from easy
learning assignments on the competence level ‘remember’ [
In this work, we consider the problem of creating learning
assignments with the purpose of practising analysis procedures
(competence level ‘apply’) for formal software specification
languages in the context of our undergraduate introduction to
software engineering [
When creating new assignments, e.g., to not have the same tasks in each seasons or for exams, we observed that we can identify different levels of difficulty within the same class of learning assignments. Furthermore, we gained the impression that we can precisely characterise those classes of difficulty using properties of the (formal) artefacts.
We propose to develop an approach to (a) formalise our understandings of didactical aspects of learning assignments on software description languages (like solvability, learning goals, and level of difficulty) and (b) use existing procedures and tools to automatically generate learning assignments with desired properties. In this article, we report on an investigation of the feasibility of this approach. To this end, we have developed, implemented, and evaluated a synthesis procedure for the formalism of decision tables.
The article is structured as follows. In Section II, we illustrate our approach on the example of learning assignment for basic calculus. Section III recalls decision tables and gives an example of an exam task that we would like to automatically generate. Sections IV and V describe our synthesis procedure and preliminary empirical results, Sections VI and VII discuss our results and related work, and Section VIII concludes.
II. AN ANALOGY: LEARNING ASSIGNMENTS FOR
ADDITION WITH CARRY
In this section, we want to illustrate the proposed approach on an example of learning assignments for elementary school arithmetic, namely ‘paper & pencil’ addition with carry of two positive decimal numbers. As a teacher, one may want to present learning assignments with an increasing level of 1 2 3 4 + 6 2 5 1 8 5 9 (a) difficulty to let pupils practice the routine of ‘paper & pencil’ addition without carry before moving to the general case, and possibly in between having some learning assignment with exactly one carry. So the teacher may have identified the following three levels of difficulty: Easy tasks where no carry is needed (cf. Table Ia), intermediate level tasks where exactly one carry is needed (cf. Table Ib), and the general case where one carry may cause a subsequent carry (cf. Table Ic).
To create new learning assignments for addition, e.g., in an e-learning tool, the teacher could firstly formalise the addition of two n-digit decimal numbers as shown in Table Id. The task of adding two numbers in decimal representation consists of two numbers x and y with their decimal representation xn, . . . , x0 and yn, . . . , y0. The first carry, caused by adding the least significant digits x0 and y0, is c1, which has value 1 if and only if x0 + y0 > 10, and value 0 otherwise.
Viewing addition tasks as mathematical objects, the teacher could secondly precisely characterise the sets of addition tasks corresponding to the levels of difficulty described above. An easy addition task is one where all carries ci, 1 ≤ i ≤ n, have value 0. Intermediate level and general case tasks can be characterised similarly. With this formalisation of learning assignments and the level of difficulty, the teacher could finally use any integer constraint solver that supports addition and comparison to obtain tasks that are, e.g., in the class of easy tasks: We are asking for a solution to the constraint solving problem that the open symbols xi and yi are assigned values between 0 and 9 (decimal digits) such that the valuation satisfies the constraint that all carries remain 0. Note that the number of digits n is a parameter of the constraint solving problem with which the teacher can control, e.g., the time it takes to solve a task as an additional teaching aspect.
That is, we propose to formalise didactical intents on learning assignments that involve mathematical objects (such as addition tasks) in form of constraints and to use appropriate constraint solving techniques to automatically generate learning assignments for a given intent.
Decision tables are a simple software engineering formalism
that can, e.g., be used to formalise requirements [
Fig. 1: Concrete syntax of decision tables. of the set {−, ×, ∗}, and the bottom k entries of a rule (the effect) w1,i, . . . , wk,i are from the set {−, ×}. That is, ‘∗’ may not occur in an effect of a well-formed decision table.
The semantics of decision tables is given by a function
F that assigns to each rule r in T a propositional logic
formula over C and A. Given premise (v1, . . . , vm) and effect
(w1, . . . , wk ) of r, the semantics function is defined as
F (r) := V1≤i≤m F (vi, ci) ∧ V1≤j≤k F (wj , aj )
| {z } | {z }
=:Fpre (r) =:Feff (r)
(1)
where F := {(×, x) 7→ x, (−, x) 7→ ¬x, (∗, x) 7→ true}.
For a discussion of the use of this semantics in requirements
engineering we refer the reader to [
We can formally define different properties of decision tables that are useful in requirements engineering such as completeness, consistency, existence of useless rules, etc.. For the purpose of this article it is sufficient to provide the definition of (non-)determinism. A decision table T is called deterministic, if and only if for all different rules r1 and r2 in T , their premise formulae are (logically) disjoint, i.e. if ∀ r1 6= r2 ∈ T • |= ¬(Fpre (r1) ∧ Fpre (r2)). (2) Intuitively, a decision table is deterministic if and only if there is no valuation of the conditions in C that satisfies the premise formulae of two different rules.
To practice the analysis of decision tables for determinism, learning assignments can start on the competence level of ‘apply’. In the course, we present a truth table-based approach to decide determinism for a given decision table: For each valuation of the observables in C note down which rules’ premises are satisfied. The table is deterministic if and only if no valuation satisfies more than one rules’ premises.
A proof of determinism needs an argument on the rules’ premise formulae (e.g., the truth table), while a proof of non-determinism strictly speaking only needs one valuation and the argument that this valuation satisfies the premise formulae of two different rules. Hence the workload for a given deterministic table can be higher (construction of truth table) than for a given non-deterministic table (give a counterexample as explained above). Thus in the role of a teacher, we often want to control whether the decision table given as a learning assignment is deterministic or non-deterministic.
Figure 2 shows a simplified example of an exam task on decision tables. The Subtask (1) tests that students are able r1 × × − × − r2 × − × − × r3 − ∗ ∗ − − 1) Give the rule formulae for r1, r2, r3. 2) It is claimed that T is deterministic.
Prove this claim. 3) Does T have a useless rule?
Prove your claim. to use the semantics function (competence level ‘apply’). This kind of task is obviously solvable for each well-formed decision table, yet to be most useful, one may wish to provide a table that comprises all possible entries. Subtask (2) tests competences in applying a particular proof strategy for a particular decision table property. This subtask is only solvable (or at least not strongly confusing) if the considered decision table has the claimed property. Subtask (3) tests competences on analysing a decision table for whether it has a certain property such as useless rules (hence touching the competence level ‘analyse’). Depending on the correct answer, different proof strategies apply that may need a significantly different amount of time to solve. One may aim at a decision table for which Subtasks (2) and (3) need different proof strategies so to test both and to limit the necessary effort. Note that using only one decision table lowers the cognitive load for the learners since only one artefact needs to be read and the learners can concentrate on the analysis tasks as such.
Creating learning assignments as shown in Figure 2 is difficult because multiple constraints need to be considered together. A change in one cell of the decision table may unintentionally render the table non-deterministic, or make the analysis for determinism too easy (for example by having two identical rules). To simplify the process of creating learning assignments or exam tasks on decision tables, we propose to exploit the fact that decision tables are introduced as mathematical objects in our course. Properties of decision tables, such as determinism, are formally defined and thus can be used as constraints in a synthesis procedure. In addition, we propose to formalise our didactical understanding of classes of learning assignments on decision tables. For example, that an analysis for non-determinism is trivial if there are two identical rules in the table. Other examples aim at the corner cases of the definition of determinism from the course and we may want to leave out these cases in beginner’s exercises. The task to create, e.g., a complete decision table of a particular size then reduces to a mathematical constraint solving problem.
DETERMINISTIC DECISION TABLES
In the following, we outline a procedure to generate deterministic decision tables of a specified size. We focus on deterministic decision tables. Non-deterministic decision tables are the dual case (we negate one of the learning assignment creation constraints), yet to be useful learning assignments, non-deterministic decision tables need further didactic constraints, e.g., on the level of difficulty. We discuss learning assignment specification
(1) constants formulae (2) decision table (3) model some of these further constraints at the end of this section. The basic idea of our procedure to generate deterministic decision tables is to reduce the generation problem to an SMT-problem. SAT modulo theory (SMT) is a natural problem domain due to the logical nature of the decision table semantics.
Finite sets C and A of conditions and actions and a number n ∈ N0 of rules constitute the learning assignment specification (cf. Figure 3). In Step (1), we define the signature of the SMT-problem as a set of constants, one constant per decision table cell. Over this signature, we generate formulae that, e.g., specify the allowed content of decision table cells and also the determinism property. In Step (2), an SMT-solver generates a model, i.e., an interpretation of the signature such that the considered formulae hold under this interpretation (if and only if a deterministic decision table of the desired size exists). In Step (3), we interpret the model as a decision table. To obtain a second, different deterministic decision table, the model from the previous run can be encoded as an additional formula. Then, taking Step (1) again, we obtain a model that encodes a different deterministic decision table (if and only if a second decision table of the desired form exists).
The idea of the encoding is as follows: For each premise cell of the desired decision table, there is one constant in the signature that can take values ‘×’, ‘−’, or ‘∗’, and similarly for each effect cell, then with possible values ‘×’ or ‘−’. So to obtain a table over m conditions and k actions with n rules (cf. Figure 1), we would have constants v1,1, . . . , vm,n and w1,1, . . . , wk,n. Now any model of the trivial formula ‘true’ as returned by an SMT-solver is already an encoding of a wellformed decision table: The entry of cell, e.g., vi,j takes the interpretation of the constant vi,j , which is ‘×’, ‘−’, or ‘∗’.
Providing a constraint that corresponds to determinism is a bit more involved. Firstly, the definition of determinism (cf. (2)) refers to a fixed decision table with fixed premise formulae. For decision table generation, we need a formula that refers to the decision table as encoded by the constants vi,j and wi,j . Secondly, the definition of determinism refers to validity of propositional formulae by using the validity operator ‘|=’ (read: for each valuation of the conditions in C, the negation of two different rules’ premise formula evaluates to true). Such a validity operator is usually not directly available in SMT-solvers.
We observe that the premise formula of a rule r in a decision table is obtained using the helper function F . Function F basically says, that a given valuation σ : C → {0, 1} of the conditions in C is enabling the i-th cell (in the row of condition ci) of the j-th rule if and only if this cell holds symbol ‘×’ and 300 t/s 250 200 150 100 50 σ(ci) = 1, or this cell holds symbol ‘−’ and σ(ci) = 0, or this cell holds symbol ‘∗’ (“don’t care”). In the SMT-encoding, the symbol in “this cell” is given by the value of constant vi,j , hence the equivalence stated above corresponds to the formula
Gi,j := (vi,j = × ∧ ci) ∨ (vi,j = − ∧ ¬ci) ∨ (vi,j = ∗) (3) over a logical variable ci. Formula (3) holds if and only if the current value of ci enables the currently considered entry of the decision table cell as given by the interpretation of constant 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 all cells that constitute the premise of r. Hence the formula Gj := G1,j ∧ · · · ∧ Gm,j corresponds to the enabledness of rule rj (where the rule is given by the current interpretation of the vi,j ). So to obtain a deterministic decision table, we conjoin the overall formula
G := ∀ 1 ≤ j1 6= j2 ≤ n ∀ c1, . . . , cm • ¬(Gj1 ∧ Gj2 )
(4)
to the SMT-problem. The particular SMT-problem is now to
provide an interpretation of the signature (i.e., the constants
vi,j and wi,j ) such that G is satisfied. For details of the
encoding, we refer the reader to [
We have implemented our approach using the API of the
SMT-solver SMTInterpol [
Figure 4 shows the runtime of decision table generation using our implementation. The practically most relevant graph is elapsed time (blue); the total user time (yellow) grows faster because the underlying solver effectively uses multi-core systems. The top graph shows the time needed to generate one decision table of size (n+n)×n (n conditions and actions, and n rules). For values of n up to 10, the runtime is in the order of seconds. Hence generating decision tables for our exercises and exams is well feasible, because our tasks usually have 3 to 5 conditions, about 3 actions, and not more than 7 rules. Working on larger decision tables in ‘paper & pencil’ style is in our opinion not supporting the learning but just tedious.
One use case that we envision for our procedure is to generate bunches of decision tables as task candidates for 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 inspection of the bunches shows that using SMTInterpol has the effect that the tables in the bunches do not feel too regular (i.e., not like a mere enumeration of decision tables) and that we do not get too many symmetric decision tables. Still, we plan to give teachers the possibility to refine the specification, e.g., to limit the number of ‘∗’ symbols (the fewer ‘∗’ symbols a decision table has, the more obvious the determinism).
The previous sections show that it is possible to synthesise learning assignments for software description formalisms (viewed as mathematical objects) that satisfy certain precisely stated constraints. These constraints can be very generic, in our case the full power of logic over some theory is available. Here we see a strong potential of our approach: We formalise conditions that make learning assignments good learning assignments, relative to the teacher’s intention and the students’ situation in the same way as sketched for addition tasks in the introduction.
In the case of decision tables, we have for example observed that the tasks that we create anew each season for the exercises and the exam follow certain principles. One is of course the size of the tables (as already considered in our generation procedure). With non-deterministic decision tables, we do consider more aspects. For example, a table where two rules are just copies of each other could be too easy to analyse. We can immediately formalise that there are no two identical rules and add that constraint to the learning assignment specification. Then, our definition of determinism has the particularity that actions are not considered. So if two rules can be enabled by one valuation of the conditions and have the same effect, they are still (by definition) nondeterministic. A table with all different effects could be a good choice when starting with non-deterministic tables, yet the corner-case of overlapping premise and equivalent effect should be presented to the advanced learner. Again, we can formalise both cases as constraints. Furthermore, an analysis for non-determinism could be too easy if there are too many ‘∗’ symbols in the table, so we may want to add a constraint that limits the number of ‘∗’ symbols overall, or just per rule. The same applies to other properties of decision tables, such as completeness, consistency, presence of useless rules, etc..
Once we have established a set of constraints that can be added to learning assignment generation runs, there are manifold applications. The most obvious application is to generate exercises or exam tasks tailored to a particular teaching or testing goal (cf. Figure 2). It is easy to embed our decision table synthesis procedure into a tool where a teacher only selects the kind of task to obtain a task statement and a matching decision table. We envision a tool that presents a selection of tasks to teachers. We feel that the teacher needs to decide and should not blindly rely on a tool. The experience from our experiments is that a set of 10 (or even 100) decision tables usually includes many examples of good exercises.
Having decision tables available in machine readable form allows us to generate much of the necessary material automatically, including correction schemes and slides for tutorial sessions. In tutorials that discuss non-determinism, there could be overlays for the case with disjoint effects and the corner-case with equivalent effects. Further applications could be to offer an e-learning tool, e.g., a website or a mobile application, that generates new learning assignments for a student-controlled or heuristically adapted level of difficulty. Note that we want to address learning activities that focus on the formalisms and analysis procedures as such. To this end, it is perfectly adequate that the generated decision tables do not model an existing system. In our opinion, students should not firstly assess the pragmatics of a decision table model, or try to look out for non-determinism in their imagination of the modelled system, but they should learn to rely on the purely abstract application of analysis procedures.
From our experience with exercises for our software engineering course, we anticipate that our approach can be extended to class diagrams, object diagrams, OCL constraints together with class diagrams, and even Statechart-like formalisms. It is an open research question which synthesis procedure is adequate for which formalism.
The idea to generate learning assignments is not new.
worksheets for elementary school arithmetic are generated
randomly (e.g., [
Our approach can be seen to take one step back since we feel that teaching of software description languages is not yet as well-researched as, e.g., geometry or algebra. We put the teachers’ understanding of learning assignments first and want to provide problem encodings such that teachers can formalise their understanding of problem classes and have complete control over generated problems.
We have presented a logic-based approach to characterise and synthesise learning assignments for a subset of the formal software description language of decision tables. A first evaluation shows that our procedure quickly generates problems of the size needed for ‘paper & pencil’ tasks. We argue to put computer science teachers into a prominent position when generating learning assignments: A formalisation of software engineering problems allows us teachers to formalise and investigate our understanding of good learning assignments.
Future research includes to extend the set of supported learning assignments (also for different formalisms), and further research into the nature of instructionally good learning assignments and their formal characterisation.