{'fraction_non_alphanumeric': 0.04562654236358651, 'fraction_numerical': 0.012119550315327667, 'mean_word_length': 4.458246034121521, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Synthesizing Imperative Programs for Introductory Programming Assignments

We present a novel algorithm that synthesizes imperative programs for introductory programming courses. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our key idea is to combine enumerative program synthesis and static analysis, which aggressively prunes out a large search space while guaranteeing to find, if any, a correct solution. We have implemented our algorithm in a tool, called SIMPL, and evaluated it on 30 problems used in introductory programming courses. The results show that SIMPL is able to solve the benchmark problems in 6.6 seconds on average.


Introduction
Our long-term goal is to build an intelligent tutoring system that helps students to improve their programming skills. Our experience in introductory programming courses is that students, who learn programming for the first time, often struggle with solving programming problems for themselves. Manually providing guidance simply does not scale for the increasingly large number of students. To make matters worse, we found that even instructors sometimes make mistake and shy students are reluctant to ask questions. Motivated by this experience, we aim to build an automatic system that helps students to improve their skills without human teachers.
In this paper, we present a key component of the system, which automatically generates complete programs from students' incomplete programs. The inputs of the algorithm are a partial program with constraints on variables and constants, and input-output examples that specify the program's behavior. The output is a complete program whose behavior matches all of the given input-output examples.
The key novelty of our algorithm is to combine enumerative program synthesis and program analysis techniques. It basically enumerates every possible candidate program in increasing size until it finds a solution. This algorithm, however, is too slow to be interactively used with students due to the huge search space of programs. Our key idea to accelerate the speed is to perform static analysis alongside the enumerative search, in order to "statically" identify and prune out interim programs that eventually fail to be a solution. We formalize our pruning technique and its safety property.
The experimental results show that our algorithm is remarkably effective to synthesize introductory imperative programs. We have implemented the algorithm in a tool, SIMPL, and evaluated its performance on 30 programming tasks used in introductory courses. With our pruning technique, SIMPL is fast enough to solve each problem in 6.6 seconds on average. However, without the pruning, the baseline algorithm, which already adopts well-known optimization techniques, takes 165.5 seconds (25x slowdown) on average.
We summarize our contributions below: • We present a new algorithm for synthesizing imperative programs from examples. To our knowledge, our work is the first to combine enumerative program synthesis and static analysis technologies.
• We prove the effectiveness of our algorithm on 30 real programming problems used in introductory courses.
The results show that our algorithm quickly solves the problems, including ones that most beginner-level students have hard times to solve.
• We provide a tool, SIMPL, which is publicly available and open-sourced. 1

Showcase
In this section, we showcase SIMPL with four programming problems that most beginners feel difficult to solve. To use SIMPL, students need to provide (1) a partial program, (2) a set of input-output examples, and (3) resources that SIMPL can use. The resources consist of a set of integers, a set of integer-type variables, and a set of array-type variables. The goal of SIMPL is to complete the partial program w.r.t. the input-output examples, using only the given resources.
Problem 1 (Reversing integer) The first problem is to write a function that reverses a given integer. For example, given integer 12, the function should return 21. Suppose a partial program is given as Problem 2 (Counting) The next problem is to write a function that counts the number of each digit in an integer. The program takes an integer and an array as inputs, where each element of the array is initially 0. As output, the program returns that array but now each array element at index i stores the number of is that occur in the given integer. For example, when a tuple (220, 0, 0, 0 ) is given, the function should output 1, 0, 2 ; 0 occurs once, 1 does not occur, and 2 occurs twice in '220'. Suppose the partial program is given as For this problem, SIMPL produces the program in Figure 1(b) in 0.2 seconds. Note that SIMPL uses a minimal set of resources; i is not used though it is given as usable.
Then, SIMPL produces the program in Figure 1(c) in 37.6 seconds. Note that SIMPL newly introduced a nested loop, which is absent in the partial program.
Problem 4 (Absolute sum) The last problem is to sum the absolute values of all the elements in a given array. We provide the partial program:

Problem Definition
Language We designed an imperative language that is small yet expressive enough to deal with various programming problems in introductory courses. The syntax of the language is defined by the following grammar:
A program P = (x, c, y) is a command with input and output variables, where x is the input variable, c is the command, and y is the output variable. The input and output variables x and y can be either of integer or array types. For presentation brevity, we assume that the program takes a single input, but our implementation supports multiple input variables as well.
An unusual feature of the language is that it allows to write incomplete programs. Whenever uncertain, any arithmetic expressions, boolean expressions, and commands can be left out with holes (♦, △, ). The goal of our synthesis algorithm is to automatically complete such partial programs.
The semantics of the language is defined for programs without holes. Let X be the set of program variables, which is partitioned into integer and array types, i.e., X = X i ⊎ X a . A memory state is a partial function from variables to values (V). A value is either an integer or an array of integers. An array a ∈ Z * is a sequence of integers. For instance, we write 1, 2, 3 for the array of integers 1, 2, and 3. We write |a|, a i , and a k i for the length of a, the element at index i, and the array a 0 . . . a i−1 ka i+1 . . . a |a|−1 , respectively.
The semantics of the language is defined by the functions: ] denote the semantics of arithmetic expressions, boolean expressions, and commands, respectively. Figure 2 presents the denotational semantics, where fix is a fixed point operator. Note that the semantics for holes is undefined. Synthesis Problem A synthesis task is defined by the five components: is a set of integer-type variables, and X a is a set of array-type variables. The goal of our synthesis algorithm is to produce a complete command c without holes such that • c uses constants and variables in Γ and X i ∪ X a , and • c is consistent with every input-output example:

Synthesis Algorithm
In this section, we present our synthesis algorithm that combines enumerative search with static analysis.

Synthesis as State-Search
We first reduce the synthesis task into a state-search problem. Consider a synthesis task ((x, c, y), E, Γ, X i , X a ). The corresponding search problem is defined by the transition system (S, →, s 0 , F ) where S is a set of states, (→) ⊆ S × S is a transition relation, s 0 ∈ S is an initial state, and F ⊆ S is a set of solution states. if ¬prune(s) then W ← W ∪ next(s) 8: until W = ∅ • States : A state s ∈ S is a command possibly with holes, which is defined by the grammar in Section 3. • Initial state : An initial state s 0 is a partial command c 0 .
• Transition relation : Transition relation (→) ⊆ S × S determines the state that is immediately reachable from a state. The relation is defined as a set of inference rules in Figure 3. Intuitively, a hole can be replaced by an arbitrary expression (or command) of the same type. Given a state s, we write next(s) for the set of all immediate next states, i.e., next(s) = {s ′ | s → s ′ }. We write s → for terminal states, i.e., states with no holes. • Solution states : A state s is a solution iff s is a terminal state and it is consistent with all input-output examples:

Baseline Search Algorithm
Algorithm 1 shows the basic architecture of our enumerative search algorithm. The algorithm initializes the workset W with c 0 (line 1). Then, it picks a state s with the smallest size and removes the state from the workset (line 3). If s is a solution state, the algorithm terminates and s is returned (line 5). For a non-terminal state, the algorithm attempts to prune the state by invoking the function prune (line 7). If pruning fails, the next states of s are added into the workset and the loop repeats. The details of our pruning technique is described in Section 4.3. At the moment, assume prune always fails. The baseline algorithm implicitly performs two wellknown optimization techniques. First, it maintains previously explored states and never reconsider them. Second, more importantly, it normalizes states so that semantically-equivalent programs are also syntactically the same. For instance, suppose (r := 0; r := x * 0; ) is the current state. Before pushing it to the workset, we first normalize it to (r := 0; ).
To do so, we use four code optimization techniques: constant propagation, copy propagation, dead code elimination, and expression simplification [Aho et al., 1986]. These two techniques significantly improve the speed of enumerative search.
In addition, the algorithm considers terminating programs only. Our language has unrestricted loops, so the basic algorithm may synthesize non-terminating programs. To exclude them from the search space, we use syntactic heuristics to detect potentially non-terminating loops. The heuristics are: 1)

Pruning with Static Analysis
Now we present the main contribution of this paper, pruning with static analysis. Static analysis allows to safely identify states that eventually fail to be a solution. We first define the notion of failure states. Definition 1. A state s is a failure state, denoted fail(s), iff every terminal state s ′ reachable from s is not a solution, i.e., fail(s) ⇐⇒ ((s → * s ′ ) ∧ s ′ → =⇒ ¬solution(s ′ )).
Our goal is to detect as many failure states as possible. We observed two typical cases of failure states that often show up during the baseline search algorithm. Example 1. Consider the program in Figure 4(a) and inputoutput example (1, 1). When the program is executed with n = 1, no matter how the hole (♦) gets instantiated, the output value r is no less than 2 at the return statement. Therefore, the program cannot but fail to satisfy the example (1, 1). Example 2. Consider the program in Figure 4(b) and inputoutput example (1, 1). Here, we do not know the exact values of x and r, but we know that 10 * x = 1 must hold at the end of the program. However, there exists no such integer x, and we conclude the partial program is a failure state. Static Analysis We designed a static analysis that aims to effectively identify these two types of failure states. To do so, our analysis combines numeric and symbolic analyses; the numeric analysis is designed to detect the cases of Example 1 and the symbolic analysis for the cases of Example 2. The abstract domain of the analysis is defined as follows: An abstract memory state m maps variables to abstract values ( V). An abstract value is a pair of intervals (I) and symbolic values (S). The domain of intervals is standard [Cousot and Cousot, 1977]: For symbolic analysis, we define the following flat domain: , or a binary operation with symbolic expressions. We introduce symbols one for each integer-type variable in the program. The symbolic domain is flat and has the partial order: s 1 ⊑ S s 2 ⇐⇒ (s 1 = ⊥) ∨ (s 1 = s 2 ) ∨ (s 2 = ⊤). We define the abstraction function α : V → V that transforms concrete values to abstract values: α(n) = ([n, n], n) α(n 1 . . . n k ) = ([min{n 1 , . . . , n k }, max{n 1 , . . . , n k }], ⊤).
The abstract semantics is defined in Figure 5  For while-loops, the analysis performs a sound fixed point computation. If the computation does not reach a fixed point after a fixed number of iterations, we apply widening for infinite interval domain, in order to guarantee the termination of the analysis. We use the standard widening operator in [Cousot and Cousot, 1977]. The function fix and cond in Figure 5 denote a post-fixed point operator and a sound abstraction of cond, respectively. Pruning Next we describe how we do pruning with the static analysis. Suppose we are given examples E ⊆ V × V and a state s with input (x) and output (y) variables. For each example (v i , v o ) ∈ E, we first run the static analysis with the input α(v i ) and obtain the analysis result (itv s , se s ) : We only consider the case when itv s = [l s , u s ] (when itv s = ⊥, the program is semantically ill-formed and therefore we just prune out the state). Then, we obtain the interval abstrac- The first (resp., second) conjunct means that the interval (resp., symbolic) analysis result must over-approximate the output example. We prune out a state s iff C s (vi,vo) is unsatisfiable for some example (v i , v o ) ∈ E: Definition 2. The predicate prune is defined as follows: prune(s) ⇐⇒ C s (vi,vo) is unsatisfiable for some (v i , v o ) ∈ E. The unsatisfiability can be easily checked, for instance, with an off-the-shelf SMT solver. Our pruning is safe: Theorem 1 (Safety). ∀s ∈ S. prune(s) =⇒ fail(s).
That is, we prune out a state only when it is a failure state, which formally guarantees that the search algorithm with our pruning finds a solution if and only if the baseline algorithm (Section 4.2) does so.

Evaluation
Experimental setup To evaluate our synthesis algorithm, we gathered 30 introductory level problems from several online forums (Table 1). 2 The problems consist of tasks manipulating integers and arrays. Some problems are non-trivial for novice students to solve; they require students to come up with various control structures such as nested loops and combinations of loops and conditional statements. The partial programs we used are similar to those shown in Section 2; they have one boolean expression hole (△), and one or two command holes ( ). For each benchmark, we report the number of integer variables (IVars), array variables (AVars), integer constants (Ints), and examples (Exs) provided, respectively. All benchmark problems are publicly available with our tool. Experiments were conducted on MacBook Pro with Intel Core i7 and 16GB of memory. Baseline Algorithm Table 1 shows the performance of our algorithm. The column "Base" shows the running time of our baseline algorithm that performs enumerative search without state normalization. In that case, the average runtime was longer than 616 seconds, and three of the benchmarks timed out (> 1 hour). The column "Base+Opt" reports the performance of the baseline with normalization. It shows that normalizing states succeeds to solve all benchmark problems and improves the speed by more than 3.7 times on average, although it degrades the speed for some cases due to runtime normalization overhead. Pruning Effectiveness On top of "Base+Opt", we applied our static-analysis-guided pruning technique (the column "Ours"). The results show that our pruning technique is remarkably effective. It reduces the average time to 6.6 seconds, improving the speed of "Base+Opt" by 25 times. Note that SIMPL is able to synthesize the desired programs from a few examples (Exs), requiring up to 4 examples.

Related Work
Computer-aided education Recently, program synthesis technology has revolutionized computer-aided education. For instance, the technology has been used in automatic problem generation [Singh et al., 2012;Ahmed et al., 2013;Alvin et al., 2014;Polozov et al., 2015], automatic grading [Alur et al., 2013], and automatic solution generation .
Our work is to use program synthesis for automated programming education system.
primarily on providing feedback on students' programming submissions. Our system, SIMPL, has the following advantages over prior works: • Feedback on incomplete programs: Existing systems produce feedback only for complete programs; they cannot help students who do not know how to proceed further. In this case, SIMPL can help by automatically generating solutions starting from incomplete solutions. • No burden on instructor: Existing systems require instructor's manual effort. For example, the system in [Singh et al., 2013] needs a correct implementation and a set of correction rules manually designed by the instructor. On the other hand, SIMPL does not require anything from the instructor. An exception is [Farrell et al., 1984], where an automatic LISP feedback system is presented. However, the system produces feedback by relying on ad-hoc rules. Programming by example Our work differs from prior programming-by-example (PBE) techniques in two ways. First, to our knowledge, our work is the first to synthesize imperative programs with loops. Most of the PBE approaches focus on domain-specific languages for string transformation Raza et al., 2015;Manshadi et al., 2013;Wu and Knoblock, 2015], number transformation [Singh and Gulwani, 2012], XML transformation [Raza et al., 2014], and extracting relational data [Le and Gulwani, 2014], etc. Several others have studied synthesis of functional programs [Albarghouthi et al., 2013;Osera and Zdancewic, 2015;Frankle et al., 2016]. Second, our algorithm differs from prior work in that we combine semantic-based static analysis technology with enumerative program synthesis. Existing enumerative synthesis technology used pruning techniques such as type systems [Osera and Zdancewic, 2015;Frankle et al., 2016] and deductions [Feser et al., 2015], which are not applicable to our setting.