CITADEL - Revision history

Ilinca: /* Experiment */

2008-04-29T13:39:56Z

‎Experiment

Ilinca: /* Experiment */

2008-04-29T13:32:57Z

‎Experiment

Show changes

Ilinca: /* Experiment */

2008-04-29T13:25:42Z

‎Experiment

Ilinca at 13:23, 29 April 2008

2008-04-29T13:23:10Z

Ilinca at 13:21, 29 April 2008

2008-04-29T13:21:35Z

Nadia Polikarpova: /* Inferring contracts for generic classes */

2007-12-25T12:33:31Z

‎Inferring contracts for generic classes

Nadia Polikarpova: /* Support for loop invariants */

2007-12-25T12:28:00Z

‎Support for loop invariants

Nadia Polikarpova: /* Unfolded variables */

2007-12-25T12:22:37Z

‎Unfolded variables

Nadia Polikarpova: /* Unfolded variables */

2007-12-25T12:17:43Z

‎Unfolded variables

Show changes

Nadia Polikarpova: /* Unfolded variables */

2007-12-25T12:16:38Z

‎Unfolded variables

Show changes

← Older revision		Revision as of 13:39, 29 April 2008
Line 509:		Line 509:

	==Experiment==		==Experiment==
−
−	~~EXPERIMENTS~~

	See Google doc.		See Google doc.

@@ Line 519: / Line 519: @@
 How to choose the c classes:
-- They should have various sizes (LOC, #routines, depth of inheritance tree)
+* They should have various sizes (LOC, #routines, depth of inheritance tree)
-- They should have various semantics
+* They should have various semantics
-- They should also contain routines missing preconditions/postconditions.
+* They should also contain routines missing preconditions/postconditions.
-- They should also contain routines using loops.
+* They should also contain routines using loops.
-- They should also contain contracts (either already given or intended) that can only be expressed using functions.
+* They should also contain contracts (either already given or intended) that can only be expressed using functions.
 Observations:
-- We will manually create the n1 test cases, then add n2-n1 which test other cases - so hopefully and informally also increase coverage - and then add n3-n2 test cases which also cover other cases.
+* We will manually create the n1 test cases, then add n2-n1 which test other cases - so hopefully and informally also increase coverage - and then add n3-n2 test cases which also cover other cases.
-- We take test suite size as a measure of its quality. We will also measure coverage (manually) and then see if there's any relation between increased coverage (as the extended test suites will probably have) and better contract inference.
+* We take test suite size as a measure of its quality. We will also measure coverage (manually) and then see if there's any relation between increased coverage (as the extended test suites will probably have) and better contract inference.
-- The test suite size as proposed initially might be too small, but we can increase it during the experiment if we see that we're not getting results that are relevant enough.
+* The test suite size as proposed initially might be too small, but we can increase it during the experiment if we see that we're not getting results that are relevant enough.
-- It would be interesting to compare results of experiment for library classes and classes from ordinary application (open source written by someone else), because manually written contracts for library classes must be of higher quality. We will run this experiment too if we have the time.
+* It would be interesting to compare results of experiment for library classes and classes from ordinary application (open source written by someone else), because manually written contracts for library classes must be of higher quality. We will run this experiment too if we have the time.
@@ Line 592: / Line 592: @@
 OBSERVATIONS:
-- Assumption 1 is purely quantitative, the rest are qualitative.
+* Assumption 1 is purely quantitative, the rest are qualitative.
-- Each of the above assertions depends on the following parameters:
+* Each of the above assertions depends on the following parameters:
-	- number of tests given to Daikon
+** number of tests given to Daikon
-	- quality of tests given to Daikon (traditional coverage criteria don't fit in this case [4, 5])
+** quality of tests given to Daikon (traditional coverage criteria don't fit in this case [4, 5])
-- The set of inferred assertions is itself a useful measure of test suite quality. It allows using it for test suit improvement. And what is even better there is no dilemma, whether to use assertion inference for test suit improvement OR for contract strengthening. It can be used for both simultaneously.
+* The set of inferred assertions is itself a useful measure of test suite quality. It allows using it for test suit improvement. And what is even better there is no dilemma, whether to use assertion inference for test suit improvement OR for contract strengthening. It can be used for both simultaneously.
-- We might want to check each of the above assumptions separately for preconditions, postconditions and class invariants.
+* We might want to check each of the above assumptions separately for preconditions, postconditions and class invariants.
@@ Line 603: / Line 603: @@
 OTHER QUESTIONS:
-- How does the set of templates used by Daikon influence its results?
+* How does the set of templates used by Daikon influence its results?
-- How can we improve Daikon's results?
+* How can we improve Daikon's results?
 	- The set of expressible assertions depends mainly on two things: Daikon's grammar (I mean, the set of assertion templates) and the set of variables at program point (those that were produced by instrumenter + those that are derived by Daikon).  In Eiffel assertion grammar is rather simple, all its expressive power is "hidden" in ability to use function calls. So, to make Daikon's output close to what Eiffel developers write by hand, we shouldn't extend its grammar (I think, that we could even simplify it a bit...), instead we should make it use more functions from the code of processed system (as you know, currently only zero-argument functions are used).
 Instrumenter could include not only zero-argument functions in unfolding, but also functions with 1 or even 2 arguments (other variables in scope and also some predefined constants could serve as actuals). Of cause, it will significantly increase the number of variables at program point, however in this case we can:

@@ Line 563: / Line 563: @@
 GENERAL CONCLUSIONS:
-- Daikon does a better/worse job than programmers at coming up with contracts.
+* Daikon does a better/worse job than programmers at coming up with contracts.
-- Daikon can/cannot be used to strengthen already existing contracts.
+* Daikon can/cannot be used to strengthen already existing contracts.
-- Daikon can/cannot be used to correct already existing contracts.
+* Daikon can/cannot be used to correct already existing contracts.
-- Comparing Daikon's output to user-written contracts allows/does not allow improving test suites.
+* Comparing Daikon's output to user-written contracts allows/does not allow improving test suites.

← Older revision		Revision as of 13:21, 29 April 2008
Line 506:		Line 506:
	On my opinion, a separate .decls file, generated during instrumentation		On my opinion, a separate .decls file, generated during instrumentation
	phase, is a better design decision.		phase, is a better design decision.
		+
		+
		+	==Experiment==
		+
		+	EXPERIMENTS
		+
		+	Experiment 1: Take c classes from Base and Gobo and run CITADEL on them first with a test suite of size n1, then with a test suite of size n2, then with a test suite of size n3 (where n1 < n2 < n3). ni represents the number of calls to routines of the class under test contained in the test suite.
		+	c = 10 (or 20?)
		+	n1 = #routines of the class under test
		+	n2 = 2 * n1
		+	n3 = 3 * n1
		+
		+	How to choose the c classes:
		+	- They should have various sizes (LOC, #routines, depth of inheritance tree)
		+	- They should have various semantics
		+	- They should also contain routines missing preconditions/postconditions.
		+	- They should also contain routines using loops.
		+	- They should also contain contracts (either already given or intended) that can only be expressed using functions.
		+
		+
		+	Observations:
		+	- We will manually create the n1 test cases, then add n2-n1 which test other cases - so hopefully and informally also increase coverage - and then add n3-n2 test cases which also cover other cases.
		+	- We take test suite size as a measure of its quality. We will also measure coverage (manually) and then see if there's any relation between increased coverage (as the extended test suites will probably have) and better contract inference.
		+	- The test suite size as proposed initially might be too small, but we can increase it during the experiment if we see that we're not getting results that are relevant enough.
		+	- It would be interesting to compare results of experiment for library classes and classes from ordinary application (open source written by someone else), because manually written contracts for library classes must be of higher quality. We will run this experiment too if we have the time.
		+
		+
		+	ASSUMPTIONS
		+
		+	Assumption 1: Daikon finds more assertions than programmers write.
		+	How to check: Look for cases in which the programmer did not write any assertion (for a routine pre- or postcondition, class invariant or loop invariant) but Daikon correctly inferred one and see how often this happens.
		+	Note: We expect this will be mostly true for loop invariants.
		+	Experiment: 1
		+
		+	Assumption 2: Daikon-inferred assertions are generally stronger than the user-supplied assertions expressible in Daikon's grammar, but as test suite size and coverage increases, they "converge" to user-supplied ones.
		+	How to check: Try to find inclusion relations between the sets of states allowed by Daikon-inferred and by user-written contracts.
		+	Note: It would be interesting to see how many of the user-written assertions are not expressible in Daikon's grammar.
		+	Experiment: 1
		+
		+	Assumption 3: Daikon-inferred assertions are sometimes incompatible with programmer-written contracts.
		+	How to check: Try to find exclusion relations between the sets of states allowed by Daikon-inferred and by user-written contracts.
		+	Experiment: 1
		+
		+	Assumption 4: Most assertions that were inferred by Daikon follow one of a small number of patterns (e.g., equality, `/= Void', comparisons between printable variables), while most assertions that were not inferred contain one- or two-argument functions from the code.
		+	How to check: Take user-supplied assertions that were inferred by Daikon and those that were not, examine the nature of assertions from both sets and try to find what is specific about each set. Measure the exact percentage of assertions from both sets that have the assumed property.
		+	Interpretation of the conclusion (if it proves correct): Daikon does all the routine work for the developer (nobody likes writing these endless `an_arg /= Void' in preconditions or `attr = an_arg' after setter routines), however it still leaves the creative part of work to human. It would also give some empirical grounds for the idea to include more functions in unfolding.
		+	Experiment: 1
		+
		+	Assumption 5: Comparing inferred assertions to user-supplied ones can be used to improve test-suites (and, as a consequence, finding and fixing bugs).
		+	How to check: Try extending test-suite until inferred precondition is implied by user-defined one. Try on a few existing classes -- if we find more bugs in them with the extended test suite than with the original one, then we're done. If this doesn't work for existing classes, we will create some realistic examples of our own to illustrate the point.
		+
		+	Note: Test cases are created manually and preconditions are compared by human.
		+	Experiment: 1 modified: start with a test suite of size n1. We then infer assertions with this small test suite and inspect them, picking out those, that are likely to be test suit properties. Finally we extend the existing test suite with cases that violate those properties. If we do not find more faults in the classes under test this way, we'll have to create our own examples. (This approach will most likely produce the most relevant inferred assertion, however neither it can be used with existing test suites, nor can such test suites be easily constructed automatically.)
		+
		+
		+
		+	GENERAL CONCLUSIONS:
		+	- Daikon does a better/worse job than programmers at coming up with contracts.
		+	- Daikon can/cannot be used to strengthen already existing contracts.
		+	- Daikon can/cannot be used to correct already existing contracts.
		+	- Comparing Daikon's output to user-written contracts allows/does not allow improving test suites.
		+
		+
		+	(
		+	The following 2 assumptions are probably not verifiable in a reliable manner, because they are based on us having access to the "real" or "full" specification, which we can only approximate. I record them here for reference anyway.
		+	Assumption 6: Daikon does not infer fully specified contracts.
		+	How to check: Manually provide "full" specifications for the subject classes and check if Daikon found all of them.
		+	Nadia::
		+	As I said before, I'm afraid it won't be able to infer all assertions even from a regular user-supplied contract, not to mention full specification...
		+	::
		+	Ilinca::
		+	Well that's fine, it's also an interesting result. But as I mentioned above, I'm afraid we won't be able to make any reasonable estimation of what the "full" specification would be.
		+	::
		+	Assumption 7: Daikon more often determines contracts stronger than the real specification than it determines contracts weaker than the real specification.
		+	How to check: Try to find relations between the sets of states allowed by Daikon-inferred and by the "real" contracts. (Note that the "real" contracts are not the ones written by programmers, which might be buggy too, but the contracts as implied by the intended specification of the software.)
		+	Nadia::
		+	I think that we rarely can find any implication between real and inferred contracts. To say informally, inferred contracts are stronger, as they also state properties of a test suit, and at the same time they are weaker, as not all assertions can be expressed by Daikon...
		+	::
		+	Ilinca::
		+	That's a good point, we probably won't get a black-or-white result anyway.
		+	::
		+	)
		+
		+
		+
		+	OBSERVATIONS:
		+	- Assumption 1 is purely quantitative, the rest are qualitative.
		+	- Each of the above assertions depends on the following parameters:
		+	- number of tests given to Daikon
		+	- quality of tests given to Daikon (traditional coverage criteria don't fit in this case [4, 5])
		+	- The set of inferred assertions is itself a useful measure of test suite quality. It allows using it for test suit improvement. And what is even better there is no dilemma, whether to use assertion inference for test suit improvement OR for contract strengthening. It can be used for both simultaneously.
		+	- We might want to check each of the above assumptions separately for preconditions, postconditions and class invariants.
		+
		+
		+
		+
		+	OTHER QUESTIONS:
		+	- How does the set of templates used by Daikon influence its results?
		+	- How can we improve Daikon's results?
		+	- The set of expressible assertions depends mainly on two things: Daikon's grammar (I mean, the set of assertion templates) and the set of variables at program point (those that were produced by instrumenter + those that are derived by Daikon). In Eiffel assertion grammar is rather simple, all its expressive power is "hidden" in ability to use function calls. So, to make Daikon's output close to what Eiffel developers write by hand, we shouldn't extend its grammar (I think, that we could even simplify it a bit...), instead we should make it use more functions from the code of processed system (as you know, currently only zero-argument functions are used).
		+	Instrumenter could include not only zero-argument functions in unfolding, but also functions with 1 or even 2 arguments (other variables in scope and also some predefined constants could serve as actuals). Of cause, it will significantly increase the number of variables at program point, however in this case we can:
		+	- turn off variable derivation inside Daikon (Daikon doesn't know anything about context, its variable derivation templates are too common, so they are unlikely to be more relevant than function calls)
		+	- simplify Daikon's grammar. I guess we can eliminate a number of templates from Daikon grammar and still get more relevant assertions inferred (I mean, "using functions + less templates" is better than "not using functions + more templates"). At the same time, eliminating assertion templates considerably saves time: e.g., if we get rid of ternary invariants, worst inference time reduces from cubic to square in the number of variables. Including functions with number of arguments up to 1 we'll already get much information, and up to 2 - we'll have almost the whole picture :)
		+	- Are unit tests or system tests better for Daikon?
		+	Note: Nimmer & Ernst state in [1] that system tests are much better for Daikon than unit tests, where they define unit tests as "tests that check specific boundary values of procedures in a single module in isolation". This explains why they were not successful: Daikon observed not a typical behavior of a module, but rather a small set of special case behaviors; while during system tests typical and valid behavior is observed, and there are many samples. If we consider unit tests in a wider sense, i.e. including not only a small number of boundary-value tests, but also tests with input values distributed uniformly throughout routine's domain, we'll get quite good results.
		+
		+
		+
		+
		+	FACTS from already performed evaluations of Daikon:
		+	- Daikon seems to produce, even from relatively small test suites, assertions that are consistent and sufficient for automatic verification (proving the absence of runtime errors) with very little change. [1]
		+	- Daikon does not scale, because:
		+	- it writes traces to disk, hence it can easily run out of storage space [1] (Note: Even if we have a large system and a number of large system tests that execute all parts of system, nobody makes us instrument the whole system at once! We can instrument it class by class and each time get a small trace. Inferred assertions for different classes are independent.)
		+	- invariant detection time is cubic in the number of variables in scope at a program point, linear in the number of times a program point is executed, and linear in the number of instrumented program points [2]. The number of variables over which invariants are checked is the most important factor.
		+	- Randomly generated tests are not good for inferring assertions [2]
		+	- Users' experience with Daikon [3, chapter 6]:
		+	- Using Daikon does not speed up or slow down users trying to annotate programs with assertions, but it improves other factors:
		+	- recall (how many of the assertions written by users are correct)
		+	- bonus (ratio of verifiable assertions to the minimal set)
		+	- Half of the users considered Daikon to be helpful. They used the generated assertions as support for finding others.
		+	- 1/3 of the users complained about the textual size of the generated assertions.
		+	- More than half the users found removing incorrect assertions easy.
		+	- Existing code coverage criteria (branch coverage, definition-use pair coverage) don’t provide test suites that are good enough for invariant detection (they produce many false, test suite dependent invariants). However, test suites that satisfy these traditional criteria produce more relevant assertions than random [4, 5].
		+
		+
		+
		+	Bibliography
		+	[1] Nimmer, Erst, "Automatic Generation of Program Specifications"
		+	[2] Nimmer, Ernst, "Invariant Inference for Static Checking: An Empirical Evaluation"
		+	[3] Ernst, PhD thesis
		+	[4] Gupta "Generating test data for dynamically discovering likely program invariants"
		+	[5] Gupta, Heidepriem "A new structural coverage criterion for dynamic detection of program invariants"
		+	[6] Perkins, Ernst Efficient Incremental Algorithms for Dynamic Detection of Likely Invariants

← Older revision		Revision as of 12:33, 25 December 2007
Line 483:		Line 483:
	compilation facilities) or leave some unfolding work until runtime,		compilation facilities) or leave some unfolding work until runtime,
	when reflections may be used to determine variable's generating class.		when reflections may be used to determine variable's generating class.
		+
		+	Ilinca: As far as I know gobo is able to do this kind of analysis.
		+	I think it's preferable that all variables get unfolded statically
		+	-- it would be a cleaner system design. Besides, doesn't Daikon need
		+	the .decls files as input?
		+
		+	Nadia: I also think that static unfolding is better.
		+
		+	As for .decls files: if a batch version of Daikon is used, then Daikon
		+	itself is run only after instrumented system terminates. A .decls file
		+	thus may be generated not only during instrumentation, but also during
		+	instrumented system execution.
		+
		+	If an on-line Daikon version is used, Daikon is executed simultaneously
		+	with instrumented system. However, even in this case it is possible to
		+	generate program point declarations during runtime. Actually, Daikon
		+	allows to place declarations not only in separate .decls file, but also
		+	inside the .dtace file, together with program point samples. The only
		+	requirement is that a declaration of a program point must appear before
		+	any sample of this program point.
		+
		+	On my opinion, a separate .decls file, generated during instrumentation
		+	phase, is a better design decision.

@@ Line 443: / Line 443: @@
    so to say, "standalone" and doesn't try to connect it with any other.
    We don't need any extra support from Daikon to handle loop invariants.
-   If we want to infer loop invariants, we should introduce a separate
+   Nadia: If we want to infer loop invariants, we should introduce a separate
    program point for each loop. So, we need a way to distinguish loops
    within a routine. One way is to take its position in source code as

@@ Line 10: / Line 10: @@
    arrays of these scalars.
    So, if in Eiffel code we a have a variable of one of basic types
-   (BOOLEAN, NATURAL, INTEGER, REAL or STRING) we can print its value
+   (BOOLEAN, NATURAL, INTEGER, CHARACTER, REAL or STRING) we can print
-   directly as if it has one of Daikon's types.
+   its value directly as if it has one of Daikon's types.
    If, however, we have a variable of any other type, we have to collect
    all the information about it that is of interest and is available at