Korat is a tool for automatic testing of Java program. The tool brings us a
very interesting method to generate test case. The rest of the tool is
somewhere less interesting, since it consists simply of running the tests and
verifying that they do not violate the specifications.

The very interesting part of Korat, is the generation of test cases. Korat use a
Finitization object, that is an object that describes all possible objects up to
a certain size. Then, Korat can constructs the state space and starts to
explore it. The basic idea is to put an ordering on every field and value, and
to have a vector that describes a possible valuation (a possible object). The
second thing that Korat needs is a predicate (which is usually a repOk) on the
object. Korat then explores the state space, and on each object runs the
predicate. Korat monitors the predicate, to check which field of the object is
accessed. Then it can prune a whole part of the state space if the predicate
return true or false without checking certain field. The search algorithm uses
backtracking on the last variable accessed.

To test a method, one can use JML to annotate the method with a post and pre
condition. Then Korat translates these JML into real java code, and combine the
pre condition with the repOk to get a predicate. It can then generate all inputs
that verify this predicate, using the above method. The post condition is
transformed into runtime assertion. Then Korat can just run the method to test
on each input, and catch the exception of the assertion and, in case of an
assertion violation, output the example input that caused the exception.

The experimental results are very impressive. Korat can explore space as big as
$2^{100}$ in a few second. It shows that the idea of testing every possible
input up to a certain value is applicable in practice. But one problem is that
it can only test until a reasonable size, like 10 nodes for a binary tree,
because after this level, the running time continues to grow exponentially and
becomes too big. Although it does not ensure a complete correctness of the
tested method, I think it is still quite good, because most of the bugs will be
found if you test every possible inputs of small size. Of course, some bug could
only appear with bigger input, but I think it is already a quite robust testing
method that is far better than hand testing.

Régis Blanc

The authors present an approach for automatic test case generation for methods in Java programs, with the ability to include preconditions, postconditions and class invariants in testing, expressed in JML. Given an upper bound for the input, Korat generates exactly one input per isomorphic class to test, and thus proves that the method behaves correctly within the specified bounds.

The framework generates a finitization description by inspecting the class invariant and method precondition, and the programmer can modify this skeleton to precisely determine the domain for each field. Only the relevant parts of the search space are explored by the means of a lexicographic order that takes into account which fields are accessed during the execution of the class invariant; large portions of the space are pruned based on this strategy. The fields in the candidate vector are incremented in a way to ensure that only the lexicographically smallest input in an isomorphism class is considered.

The use of JML for describing specifications fits well with the programming environment as it adopts Java syntax and semantics, and can call Java methods; this could be considered an advantage compared to modeling the program in the Alloy language, the translation between the Java code and the relational logic of Alloy not being very straightforward. The benchmarks comparing Korat and the Alloy Analyzer for the test case generation show that the latter performs relatively worse, possibly because it cannot eliminate all isomorphic inputs by symmetry breaking, and may not be doing an efficient translation into boolean formulas.

Korat is very useful to generate test cases of small size for methods manipulating linked data structures, providing coverage that couldn't be ensured by manually providing test inputs. Meanwhile, it doesn't achieve a high degree of reliability as it is still infeasible to generate test cases for structures of relatively average size within the framework.

Korat is a framework for automated generation of test inputs for Java Programs. To generate test structures, it needs a predicate repOK that checks if the structure generated during the search in the input space satisfies all class invariants and the Finitization method that tells Korat how to bound the input space. It then outputs all structures where predicate returns true.

Some of the significant features of Korat:
* Allows generation of structurally complex test inputs.
* It efficiently generates "all" non-isomorphic valid structures with given bounds; monitors dynamically what predicate accesses and prunes the search based on the fields accessed.

An important thing to be noted is that the efficiency also depends to a large extent on how repOK is written. Also, I am not sure of its performance in case of larger input size, though from a video of Google tech talk by Darko Marinov, it seems that Microsoft have used a variant of it that takes XML documents as inputs which I assume would be an example of such inputs. Also, I would like to know, if it can be used for more than unit testing.

Korat is a framework which generates automated test cases for Java programs. Given a certain program (a class hierarchy), it generates a finitization and a candidate input space (depending on a certain predicate), and runs each candidate through a given set of tests. Following are short descriptions of each of the above.
* A finitization is a Korat-friendly representation of the Java program : it is dependent on the various fields in the the hierarchy of the source code. This is generated by Korat.
* The user is required to specify, in his source program, a <code>repOk</code> method, which describes whether a generated candidate is valid. For Korat, the input space is a combination of all possible values for each field in the finitization. This list can be very large, and therefore is pruned dynamically to contain only candidates validated by the <code>repOk</code>, and only one candidate per isomorphic set. This pruning is done while exploring the state space, and by eliminating certain possibilities when backtracking.
* to test properties on certain methods, preconditions and postconditions can be given as JML annotations just above a method.
* the results are relatively efficient with Java Collections and other data structures (surpassing the previous Alloy generator), and have the advantage of being easily usable for Java programmers. The problem, however, remains scaling, as the number of candidates tend to increase exponentially with the size of a data structure. Some static heuristics can probably be used to prune data beforehand.

Summary:
In this paper, the authors presented an automated software testing technique with its implementation in a tool called Korat to handle Java programs. Korat requires formal specifications (preconditions, class-invariants, postconditions) from the user for a method to be tested. Its working can be disintegrated into three broad steps:
a) Firstly, it automatically generates all nonisomorphic test cases from the given preconditions of that method.
b) Then, it runs each test case on the method.
c) Finally, it checks the correctness of the output based on the given postconditions. (It implicitly adds class-invariants assertions to both preconditions and postconditions of the method)

The core of Korat lies in the generation of all nonisomorphic test cases. Korat's search algorithm makes use of the finitization method which defines the number and potential values that a class and field can take i.e. bounds on the inputs. It generates a skeleton of finitization from the preconditions and the user can further refine it. Korat orders all the elements in every class and field domain. Also, the ordering of elements of the same class in a field is consistent with the ordering in class domain. Korat's searching strategy involves two key steps:
1) It prunes the search space by tracking only the fields that are reachable in the predicate method. It does so by continuously building the field-ordering in the order of fields encountered by predicate method. It then generates next candidate input by incrementing the last field-element and when it reaches its maximum value, it resets it to 0 and starts incrementing its left field-element. This process of exploring state space is termed as backtracking on the field-ordering.
2) It avoids isomorphic test cases by incrementing a field in a field-ordering more than one during backtracking. It decides the increment of a field in such a way that only lexicographically smallest input is generated for each isomorphic class.

Korat is a testing framework for Java programs. It tests Java methods for correctness by generating all non-isomorphic inputs of bounded size that meet the method's pre-conditions. It then tests that the output of the method when run on each test case meets the method's post-condition. It requires a formal specification be given for each method under test that includes the pre-conditions and post-conditions.

The key contribution of Korat is the method for generating valid test cases. Korat generates a candidate test case and then passes it to a Java predicate method that returns true if the test case meets the method-under-test's pre-condition and false otherwise. Korat tracks which fields are accessed when determining whether a candidate test case is valid and uses this information to prune away large portions of the state space that would produce invalid test cases. In addition, it will generate only one test case of an isomorphism partition. The specifications and the parameters of the testing are written in JML and Java, making them easy for Java programmers to create and modify them as necessary.

Korat is able to efficiently test all valid inputs for small bounds on input size. However, it's hard to make sense of just how useful this is. On the one hand, a maximum input size of eight nodes for HeapArray sounds pretty small, on the other hand, that does correspond to a state space of 1/2 billion. The authors do give some context when they tell us that six nodes are the minimum required for complete statement coverage of the extractMax method. More information along these lines would have been helpful.

Critique:
The technique presented is not scalable w.r.t. the size of the inputs. e.g. In case of binary trees, the test cases grow exponentially w.r.t. the number of nodes and so, it may not be a good testing solution even in case of moderate input-size. But is very useful in automatically detecting bugs that can appear in small input-size. One of the key features of Korat is its ability to generate test cases for abstract data structures.

Apart from the improved timing performance in comparison to Alloy Analyzer, the thing that I liked most about Korat is its guarantee of generating all nonisomorphic test cases, which is not present in Alloy Analyzer. The other thing is the usability of the tool. Since it uses JML for users' specifications of the methods, users can use Korat without much difficulty as JML is close to Java.

Korat provides a way for programmers to generate exhaustive test cases to check correctness of data structures. As input, Korat takes in a data structure and invariants for the data structure. It also requires the programmer to finitize the class, aka give a bound to the possible elements in the fields of the class. This causes the data structure to be valid for only a finite number of inputs, but the number of possible states may be exceedingly large. Korat generates nonisomorphic structures by examining which fields are accessed in the previous test case run.

Korat is a simple way for programmars to test their data structures on small inputs. The extra information the programmar is required to provide is both minimal and intuitive, and seems to be easily implementable. Korat is limited by large inputs, as this would require it to exhaustively explore an enormous input space. I found the key insight of the paper to be the work on nonismorphisms, as this allows Korat to skip large chunks of the state space.

The most interesting contribution of the paper seem to be the method of searching for test cases. The authors show how to create a ordering on all the test cases as well as how to go through that ordering in a efficient way , ignoring irrelevant groups of inputs. The system also uses this ordering to ensure that only non isomorphic test cases are generated. The combination of these two tricks make the system really fast. The system requires the programmar to create "contract" like pre-condition and post-condition and invariant for each function/class. I think the system can take the place of other practices like unit testing and protect against regression bugs. By making the user create a 'contract', the system also encourages higher level thought of the class/function. The paper ends with evaluation of performance and it is seen that the system performs exceptionally well -- infact even better than the author's expectations in it beating Alloy.

My summary was too large for this comment field, so I have placed it at:

http://fa09.pbworks.com/Korat+Reviews+-+Dcoetzee

This paper presents Korat, a new framework to generate automatic test cases. Korat is based on the JML framework. Given a method, Korat generates all test inputs satisfying the precondition up to a given size. These inputs can then be used to test the method by verifying that the postcondition holds. The inputs are generated by searching through the input state space.

The two main contributions of this paper are:
* A search method that can prune large portions of the input state space that do not satisfy the precondition. The method relies on instrumenting the precondition check so that fields that are independent are detected. This is made possible by a careful input total ordering.

* A technique to quickly to generate only one input per equivalence classes. This allows Korat to generate fewer test cases while still covering the complete state space of inputs satisfying the precondition. The trick here is to be able to skip all inputs isomorphic to the ones previously generated with low computational costs. The method presented in the paper relies again on inputs ordering. This is most interesting part of the paper.

The experimental part of this paper shows that Korat offers a significant improvement over other test cases generators. It scales to larger input state spaces because of the two aforementioned optimizations. Korat does not model threads, therefore it cannot generate test cases for concurrency bugs. Because it reuses JML for specifications, the tool should be easy to use by mainstream programmers.

Korat is a framework for automatic testing of Java program. Using a formal specification of a method, Korat automatically generates all test cases up to a given small size, then executes the method with each test case and check the correctness of the result against a test oracle.

The finitization, a finite set of objects that limits the size of the inputs, is generated by Korat for testing. To systematically explore the state space, Korat orders all the elements in every class domain and every field domain in each candidate input to form a vector of field domain indices. Korat then uses repOk to check the validity of each candidate. To further optimize the search, Korat seeks to avoid generating multiple candidates that are isomorphic to another (similar in structure).

The key contribution of Korat is the technique for automatic test case generation: given a predicate, and a bound on the size of inputs, Korat generates all nonisomorphic inputs for which the predicate returns true. However, the method does not seem to be scalable as for binary tree with the number of node of n, the state space has (n+1)^(2n+1) potential candidates. Using repOk to check all the candidates might be problematic since the number of potential candidates grows exponentially in terms of the number of nodes.

Korat is an automated testing framework for Java. It builds upon the features that JUnit and the Java Modeling Language (JML) provide; like JUint, it permits automatic running of tests, and like JML, it permits automatic generation of a test oracle. In addition to these features, it also automatically generates test cases; doing this in a robust and efficient manner is its primary contribution, and the method the authors propose is quite clever. Korat instruments the preconditions method and observes the order that fields of the input are accessed. It uses this ordering to prune large sections of the search space. Korat additionally ensures that it does not generate two or more inputs which are isomorphic to each other. These two features greatly reduce the portion of the input subspace that has to be examined and the number of tests that ultimately have to run.

Korat is fast and effective. However, despite the authors' claims, it's a big disingenuous to say that Korat automatically generates test oracles or test cases; the test oracles are generated from postconditions and class invariants that the programmer must provide, and while this is definitely good programming practice, it's hardly automatic. Likewise, the test cases are generated from preconditions, which the programmer must provide, and finitizations, which are created somewhat automatically by Korat but in some circumstances require manual modification by the programmer. The programmer must also use either algorithmic knowledge or trial and error to decide upon the best input space for Korat to test - for example, are binary trees with five nodes sufficient? All of these factors make Korat considerably less automatic than its authors imply. I will be interested to see how automated testing frameworks after Korat tackle some of these issues to reduce the burden on programmers even further.

Korat appears to be a very effective means of generating tests automatically based on Java Predicates. Without attempting to use the framework, as present in the paper a user needs only to write a repOK as well as a finitization method for each class to get nonisomorpic test cases. This could in fact yield a significant increase in the number of users who automatically generate test cases. I appreciated the fact that the authors took the time to compare their framework to the AA and honestly pointed out that it may be easier for the user to create a model with AA, but that Korat produces results in a much shorter time and also requires the user write two methods instead of a separate model.

Korat is an approach for automatically generating test cases based on JML predicates that describe the preconditions and guarantees of the procedure. The key insight is that we can prune the search space of valid inputs by evaluating arguments lazily and rejecting classes of inputs at a time by making the observation that unaccessed arguments cannot affect the result of the validity check.

One of the hallmarks of a really good paper is that the idea seems obvious in retrospect. By this measure, Korat does very well. After reading this paper, the idea of not pruning the statespace in the way seems crazy.

One of the problems that strikes me of this approach is that the way in which data is abstracted seems very important. In the provided example, the automatically generated Finitization seems suspiciously well abstracted for the problem at hand, but on closer inspection, the Node class presented contains no payload. This of course makes it simpler for the generated Finitization to know which values need not be represented, and seems almost like cheating. It may be, however, that the pruning of the search space will make the size of the initial search space less critical.

I would also be interested in seeing what is expressible in JML with Java predicates as opposed to a full blown modeling language. Could it be that for some properties it is not trivial to convert an Alloy model constraint into an equivalent JML constraint?