CITADEL - Revision history

Ilinca: /* Experiment */

2008-04-29T13:39:56Z

Experiment

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

	==Experiment==		==Experiment==

	~~EXPERIMENTS~~

	See Google doc.		See Google doc.

Ilinca: /* Experiment */

2008-04-29T13:32:57Z

Experiment

Show changes

Ilinca: /* Experiment */

2008-04-29T13:25:42Z

Experiment

← Older revision		Revision as of 13:25, 29 April 2008
Line 519:		Line 519:

	How to choose the c classes:		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:		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:		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:		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).		- 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:		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:

Ilinca at 13:23, 29 April 2008

2008-04-29T13:23:10Z

← Older revision		Revision as of 13:23, 29 April 2008
Line 563:		Line 563:

	GENERAL CONCLUSIONS:		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.

Ilinca at 13:21, 29 April 2008

2008-04-29T13:21:35Z

Show changes

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

2007-12-25T12:33:31Z

Inferring contracts for generic classes

← 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.

Nadia Polikarpova: /* Support for loop invariants */

2007-12-25T12:28:00Z

Support for loop invariants

@@ 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

Nadia Polikarpova: /* Unfolded variables */

2007-12-25T12:22:37Z

Unfolded variables

← Older revision		Revision as of 12:22, 25 December 2007
Line 10:		Line 10:
	arrays of these scalars.		arrays of these scalars.
	So, if in Eiffel code we a have a variable of one of basic types		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		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		all the information about it that is of interest and is available at

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