CITADEL

Overview

CITADEL (Contract-Inference Tool that Applies Daikon to the Eiffel Language) is a tool that provides an Eiffel front-end for the Daikon invariant detector. It is being implemented as a Master's project by Nadia Polikarpova supervised by Ilinca Ciupa (ETH).

Discussions

Unfolded variables

Nadia: Daikon can process values of only few types: five scalar types (boolean, 
 integer, double, string and hashcode) and five more types, which are 
 arrays of these scalars.
 So, if in Eiffel code we a have a variable of one of basic types 
 (BOOLEAN, NATURAL, INTEGER, CHARACTER, REAL or STRING) we can print 
 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 
 certain program point, and present this information to Daikon as a set 
 of  variables, which have Daikon types. The information of interest 
 about a variable includes results of all queries that can be called on 
 this variable at this program point.  However, since queries results may 
 themselves be of non-basic types, we have to perform this operation 
 recursively (to a certain depth).
 For a reference variable information of interest includes also its 
 address (Daikon type "hashcode" is intended for representing object 
 addresses).
 For example, if we had a variable c: POINT, queries of class POINT 
 available at current program point were `x: REAL', `y: REAL' and `twin: 
 POINT' and unfolding depth were set to 2, then `c.unfolded' would be a 
 set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}.
 
 Containers need special kind of unfolding. If we want Daikon to handle 
 them sensibly, they should be converted to arrays of scalars (to be more 
 precise, it should be done only if all container elements are observable 
 at current program point...). It isn't difficult for descendants of 
 CONTAINER class from standard library. Instrumenter may check, if a 
 variable is an indirect instance of CONTAINER, get its 
 `linear_representation', then traverse it and output as array. I think 
 that in the first version we may leave aside those containers, that 
 aren't inherited from CONTAINER.

Functions in unfolded form

Ilinca: I'm not sure about the idea of including argument-less functions in 
 this unfolded form. What if the precondition of the function doesn't 
 hold or we run into some kind of trouble when executing the function 
 body (trouble such as the contracts of a sub-call made by this 
 function not holding or other bugs)? On the other hand, including 
 functions would bring significantly more information about the state 
 of the object... Does the Daikon frontend for Java, for instance, by 
 default evaluate functions too as part of the unfolded form of the 
 objects?

Nadia: Well, this idea is disputable, of cause.
 In Java considering argument-less functions as variables is more 
 dangerous, because Java, like all C-family languages, encourages 
 side-effects in functions. However, in Daikon front-end for Java there 
 exists an option that allows using functions as variables. Together with 
 enabling this option user has to provide a special "purity" file that 
 lists those functions from the system, that are side-effect free. This 
 feature is described in Daikon User Manual, page 82.
 Considering functions as variables is even more relevant in Eiffel 
 context by two main reasons. Firstly, Eiffel encourages absence of 
 abstract side-effects in functions (and, I believe, most Eiffel 
 functions indeed do not have abstract side-effect, am I right?). For 
 those cases, when some functions in system are known to have 
 side-effect, we can allow user to specify an "impurity" file, that would 
 list those functions. I think that these cases would be rare.
 
   Ilinca: Indeed, I also think these cases would be rare, but, depending on the 
   size of the system, it might be very cumbersome for users to determine 
   these functions.

       Nadia: Well, a parameter may be introduced that will turn this facility on 
       and off. So, if a user knows that there are many impure functions in system, 
       he/she will just turn it off. I think, that its enough for the first version.
       
       In future some additional functionality may be introduced. In fact, a user may 
       not know about all impure functions in system (especially in code that was written 
       by someone else). The tool can help user to determine, did anything go wrong with 
       using functions in unfolding. For example, it may do instrumentation twice: first 
       time using only attributes and second time using functions also. As a result two 
       trace files are produces. Then the tool can compare attributes values in two files. 
       If they are the same, then with certain degree of confidence we can say, that called 
       functions had no abstract side effect.

       As I understand, precise analysis of abstract side-effect presence or absence in beyond 
       the state of the art. However, some methods which perform approximate analysis may be 
       introduced.

       Another interesting solution that came to mind is to store object's state each time before 
       calling a function and then recover object after the call. In this case we don't care about 
       function purity, we just get a result that this function might have had, if it was called at 
       this point :)

       Anyway, different partial solutions to this problem may be implemented and user may combine 
       different strategies to get a desired result with a desired degree of confidence.

       Conceptually, my point here is: why an "honest" Eiffel programmer, who never writes impure 
       functions, has to suffer (get less expressive contracts) because of other programmers, who 
       sometimes write impure functions?:)

           Ilinca: :) Indeed, the honest Eiffel programmer shouldn't suffer. So in conclusion, I 
           think we should go for the solution with the file containing the names of impure functions, 
           as Daikon does it. Adding the switch which turns it on and off is also a good idea. 

   Ilinca: Something else: what Daikon calls "purity" is actually 
   weak purity, isn't it? (Weak purity means that creations of local 
   variables are allowed in the body of a pure function. Strong purity 
   disallows this.)

       Nadia: Chicory (Java front end) doesn't check purity of functions that are listed in a purity 
       file. User is totally responsible for what he/she writes in this file. So, I would say that, what 
       Chicory calls purity isn't actually any special kind of purity. It only means that user allowed 
       Chicory to call this functions anywhere in the system, and if something goes wrong, it's user's 
       fault
 
 Nadia: Secondly, Eiffel advocates uniform access principle. Routine's clients 
 don't have to know, which queries, used in precondition, are attributes 
 and which are functions. If inferred preconditions contained only 
 attributes, it would be inconsistent with uniform access principle, I 
 think...

 As for troubles that may arise when calling functions... As I 
 understand, exception in a function, called when its precondition holds, 
 is a bug. So, if it happens, we can just tell user that we found a bug 
 in certain function and that before inferring contracts the bug should 
 be fixed.

Checking preconditions (static vs. dynamic)

 The issue with functions' preconditions that you've mentioned isn't a 
 big problem. If after unfolding we got a variable of the form, e.g., 
 `x.f1.f2', where `f1' and `f2' are functions, printing instructions for 
 this variable can be like this:
   if x.f1_precondition_holds and then x.f1.f2_precondition_holds
   then
      print (x.f1.f2)
   else
      print (Nonsensical)
   end
 
 "Nonsensical" is a special Daikon value that indicates that variable 
 cannot be evaluated.
 Function preconditions are known after parsing. To be able to evaluate 
 them separately, we may, for example, wrap them into functions. 
 `f1_precondition_holds' in the above code is an example of such a 
 function, that was introduced by instrumenter and added to x's 
 generating class.
 
   Ilinca: I don't think it's that easy, mainly because of polymorphism. Statically 
   you can't determine the type that x will be a direct instance of at 
   runtime. Hence, you don't know which preconditions to wrap. Of course, 
   since redefined routines can keep or weaken the preconditions of the 
   original routines, you can take the pessimistic approach of wrapping 
   only the precondition of the function from the static type of x, but 
   then you might miss cases in which the weakened version of the 
   precondition does hold. Do you understand my point?

       Nadia: Yeah, I see...
       I think that the main question here is: should we check "static" or "dynamic" 
       preconditions when calling a function?

       On the one hand, in Eiffel we can write something like:
       class A
          ...
          sqrt (x: REAL): REAL
              require
                  x >= 0.0
              do ... end
       end

       class B
          inherit A
             redefine sqrt end
          ...
          sqrt (x: REAL): REAL
              require else
                True
              do ... end
       end

       class TEST
           ...
           an_a: A

           make is
              do
                   create {B} an_a
                   print (an_a.sqrt (-1.0))
              end
       end

       It works, and assertion checking mechanism doesn't indicate any error.
       But, on the other hand, is it legal? Am I allowed to call a function if it's 
       static precondition doesn't hold?

       As I understand, if I want to make sure that it's legal to call a routine at some 
       program point, I have to check it's static precondition. Even if today I'm sure that 
       dynamic type of `an_a' is always `B', this needn't remain the same tomorrow...

           Ilinca: That's correct. If the "static" precondition of a routine holds, this 
           implies of course that the preconditions of all its redefinitions will also hold. 
           But I was calling this approach "pessimistic" because the precondition of a redefined 
           version of a routine may hold even though the "static" precondition doesn't.

       So, if a programmer wanted to know function value at a program point, he/she would check 
       its static precondition. Then why instrumenter should act differently? Well, actually 
       there is a difference:  instrumenter not only avoids function call when precondition 
       doesn't hold, but also claims that function value is nonsensical. From one point of view, 
       such behavior is incorrect, because function actually could be called and a sensible value 
       could be received. From the other point, since it was illegal to call the function this time, 
       it makes sense to declare function value nonsensical.

       To sum up, I think that it is rather a philosophical then a technical problem, but, as for me, 
       checking static preconditions is more appropriate.

       However, if we wanted to check a dynamic precondition, it's also possible. We can wrap function's 
       precondition into a special function and redefine that special function any time the original 
       function is redefined. It is possible since instrumenter has access to the whole system.

           Ilinca: Well, this would definitely be the more... correct solution, but it's also a lot more 
           work. Couldn't this also be done by not wrapping the function, but simply calling it and adding 
           some exception handling code to the unfolder? I mean, the unfolder would try to call all 
           argument-less functions of a class on an object, and, if it gets a precondition violation, 
           it catches the exception and it declares that particular function as nonsensical?

Nadia: I would like to return to the subject of checking "static" or "dynamic" preconditions 
before function calls in unfolding. I think that this problem arises because the semantics 
of special variable value "nonsensical" in Daikon is ambiguous.

In Java and C there are no preconditions, so this value is originally used in Daikon for the 
only purpose: if a pointer of reference is null, then the dereferenced value (and its attributes, 
if the value is not of primitive type) is declared "nonsensical". In Eiffel we will use 
"nonsensical" for this purpose too: if a reference entity is void, then its queries will be output 
as "nonsensical".

However, in Eiffel we have one more source of problems with evaluating variables: if a variable is 
a result of a function call, then function precondition may not hold, so we won't be able to 
evaluate its result. In this case the variable value should also be declared "nonsensical", because 
this is the only special value in Daikon, which denotes that variable can't be evaluated. However, 
in this case there appears a question: what does it mean that the variable can't be evaluated? Does 
it mean that something terrible will happen (e.g., exception), if we try to evaluate it? Or does 
it mean that it isn't legal to evaluate this variable in this program state?

If we take the first point, then we should check dynamic precondition, because if static precondition 
doesn't hold, but dynamic does, nothing terrible will happen during function call.

If we take the second point, we should check static precondition, because if it doesn't hold then 
it's illegal to call this function, even if dynamic precondition holds. This point seems more 
correct to me, and here is an example that illustrates the situation.

Consider class `INT_LIST' (with feature `item' that has a precondition `not off') and it's heir - 
class EXTRAPOLATED_INT_LIST (that weakens precondition of `item'):

class INT_LIST
...
feature
   item: INTEGER is
      require
         not off
      ...
      end
end

class EXTRAPOLATED_INT_LIST
inherit
   INT_LIST
   redefine
      item
   end
...
feature
   item: INTEGER is
      require else True
      do
         if not off then
            Result := Precursor
         else
            Result := 0
         end
      end
end

Consider also class CLIENT, which is a client of INT_LIST:

class CLIENT
...
feature
   test (a_list: INT_LIST) is
      do ... end
end

Imagine that during system execution, when contracts were inferred, actual argument of `test' was 
always a direct instance of EXTRAPOLATED_INT_LIST,  and in addition it was always passed to this 
procedure in such a state that cursor was before the first element (`off' was true). If we check 
dynamic preconditions for functions in unfolding, than a precondition, inferred for `test', will 
be something like this:

require
  a_list /= Void
  a_list.off
  a_list.item = 0

But this contract isn't correct (as for me), although it is, certainly, true for a specific system 
execution. It becomes a little more correct, if we infer:

require
  a_list /= Void
  a_list.off
  a_list.generator = "EXTRAPOLATED_INT_LIST"
  a_list.item = 0

However, such contracts (connected with dynamic type of variable) seem useless to me. One of the 
goals of dynamic contract inference is to eliminate those properties that happened by chance and 
are not intended properties of the code. Properties that are connected with dynamic types definitely 
happen by chance: they can't be intended properties, because if programmer wanted his software to 
have such a property, he would change static entity type to a more specific (based on descendant).

Such properties may be useful only if we treat them not as contracts but rather as some kind of 
runtime statistics. Programmer may be interested in information that is true for a specific system 
execution, e.g. for debug purposes. It might be useful to add such a feature (inference of dynamic 
type information and properties, connected with dynamic types) in future, but it isn't "classic" 
contract inference, as for me, so I don't think that we need it in the first version. And if we 
don't want to know anything about dynamic types, then we should check static preconditions of 
functions during unfolding.

Checking hand-written contracts

   Ilinca: There's one further problem with this approach: when a function 
   is called as part of the evaluation of a contract, this function's 
   contracts are not checked. The reason for this is to avoid infinite 
   loops. If you wrap your precondition into a function, the contracts of 
   any routines it calls will be evaluated, and thus the system can 
   actually behave differently.

   Should we check at all the hand-written contracts of a system for which CITADEL  
   is trying to infer contracts? We could also start from the assumption that Daikon 
   uses: the tool is given a set of passing test cases and from those it has to infer 
   contracts. If the inferred contracts somehow contradict the hand-written ones, then 
   there's a problem in the system, and the source of the  problem may be that the 
   hand-written contracts are faulty. What do you think?
   
       Nadia: I think that it makes sense to turn assertion checking off when running 
       instrumented system. This will solve the problem with functions inside wrapped 
       preconditions, which you've mentioned.

       In current version instrumented system is supposed to behave exactly the same way 
       as the original system did (except for creating a trace file). So, if a user was 
       sure about the original, hand-written contracts and wanted to check the system against 
       them, he/she could run the original system with assertion checking on, make sure that 
       everything is ok and after that perform contract inference.

       On the other hand, returning to using functions in unfolding: for these calls we have to 
       check hand-written preconditions, because they were introduced by instrumenter, so they are 
       not parts of "passing test cases". Fortunately, as you said before, erroneous preconditions 
       are very rare.

Checking preconditions (wrapping vs. qualification)

Nadia: I started implementing function preconditions checks in unfolding recently and realized 
that my first idea (to wrap these preconditions into functions) has an important disadvantage. 
Without creating new functions for preconditions if we instrument a class, then only the source 
code of that very class changes. However, if during class instrumentation we add functions to 
its clients, then the source code of those clients also changes. It isn't a disaster, of cause, 
but it's an unpleasant property, as for me. It would be nice, if class instrumentation affected 
only the class itself.

The other solution is not to wrap preconditions into functions, but to "qualify" them: if we want 
to check precondition before calling a function `x.f', we should take f's precondition and 
replaced all unqualified calls in it by qualified calls with target `x' and all occurrences of 
`Current' by `x'. This replacement is not difficult conceptually, but its implementation is quite 
voluminous (during this operation we have to replace some identifiers in an expression with function 
calls, so we need to redefine all `process_<something>' procedures of ET_AST_ITERATOR, where 
<something> can appear in expression and can contain identifiers).

What do you think about these two solutions ("wrapping into functions" and "qualification")?

   Ilinca: I think the best way to go is to wrap the precondition in a function in the class that 
   it belongs to. Wrapping it in a function in clients would break encapsulation: you would only 
   be allowed to access the exported features. I don't see any advantages of qualification over 
   function-wrapping, so I think it makes sense to choose the least-work solution

       Nadia: My previous explanation of the problem with "wrapping" was a little bit confused 
       (I wrote that functions have to be added to clients of instrumented class, but actually 
       I meant quite the opposite: that they should be added to suppliers:) )

       Wrapping a precondition in a function in the class that it belongs to is exactly what I 
       wanted to do firstly. The reason for it was that, if we instrument a class `C' and it has, 
       say, an attribute `x: LIST[INTEGER]', then unfolded form of `Current' variable will include 
       a variable `x.first'. Precondition of function `first' in class LIST is `not empty'. However, 
       we need to check this precondition not inside LIST, but inside routines of class `C'. In fact, 
       printing instruction for variable `x.first' should be guarded by condition like this:
       if x /= Void and then not x.empty then
          print (x.first)
       end
       We can't just take a precondition from `first' and insert it into the guarding condition as is, 
       instead we should "qualify" the call to `empty' with target `x'.

       Firstly qualification seemed too complex to me, so I decided to wrap `not empty' into function, say,
       `first_precondition: BOOLEAN' and add it to class `LIST', so that inside `C' I can check simpler 
       condition before printing x.first:
       if x /= Void and then x.first_precondition then
           print (x.first)
       end.
       However, as you can see, it involves modifying class `LIST' (and possibly any other supplier of 
       `C') while instrumenting `C'. If only `C' changed, then we could print only its source code after 
       instrumentation, we could compile only `C' (if incremental compilation is used) and don't recompile 
       base library, we would have no problems with tracking added functions (the problems are like this: 
       if we instrument class `LIST' after `C', we probably don't want neither to instrument added functions, 
       nor to see them in unfolded form of `Current' variable of class `LIST'). As for me, wrapping adds 
       surplus dependencies into the system, and software never benefits from dependencies :)

       That is why later I inclined to "qualification" solution. Actually, I have already mostly implemented 
       it:) Current implementation might be incomplete, there are several syntactic constructs that it doesn't 
       handle, because I'm not sure that they can appear in preconditions, but I'll check it and fix the problem.

           Ilinca: Ok, so what I was thinking about was that you wanted to wrap the whole precondition of 
           `first' into a function in class C. So, in class C you would have a routine
           precondition_first (l: LIST[G]): BOOLEAN
                require
                     l_not_void: l /= Void
                do
                     Result := not l.empty
                end
           Then the guard for printing x.first would be
                if x /= Void and then precondition_first (x) then
                     print (x.first)
                end

           But of course whether or not you wrap the precondition in a function or just quote it in the if 
           statement does not make a big difference.

One more question: should the tool allow instrumenting library classes? If a library was precompiled, 
then instrumenting any of its classes will result in recompiling the whole library, am I right? Are 
precompiled libraries anyway recompiled during system finalization or not? (It matters for choosing 
between "wrapping into functions" and "qualification" solutions, because "wrapping into functions" can 
change library classes, even if user wants to implement only classes from his own clusters).

Support for loop invariants

Ilinca: Does the "classic" Daikon support loop invariants?

Nadia: Daikon uses standard program point 
 suffixes to infer more invariants. E.g., it understands that 
 some_routine:::ENTER and some_routine:::EXIT are entry and exit points 
 of the same routine. Thanks to this, it knows `old' values of variables 
 at exit and can infer invariants like "x = old x". As I understood, if 
 Daikon sees an unknown suffix, it treats corresponding program point as, 
 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.

   Ilinca: You'll have to pay attention though to inserting the corresponding 
   program point(s) at the right location(s). A loop invariant has to hold after 
   initialization (the "from" clause) and be preserved by the loop body, i.e. it 
   must hold after every execution of the loop body, including when the exit 
   condition becomes true. So actually, I guess the program point should be in 
   the "until" clause, because it gets evaluated after initialization and then 
   after every execution of the loop body. What do you think?

       Nadia: `Until' clause is conceptually the right place, but instructions 
       can't be inserted in there. So printing instructions can be inserted at 
       the end of `from' clause and at the end of  `loop' clause. As I understand, 
       all variable values that are observed in `until' condition appear at one of 
       those points.
 
 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 
 index. However, I thought, that position is too unstable to become loop 
 identifier, so I chose instruction number instead. These numbers are 
 unique numbers of instructions within surrounding routine, they may be 
 used not only for loops, but for arbitrary instructions. 
 CI_INSTRUCTION_COUNTER is responsible for counting instruction while 
 iterating through AST.

Inferring contracts for generic classes

Nadia: there are actually two different cases.
 1. Contracts inside generic classes. This is not really a problem. 
 Entities, which have parameter type, can be treated as if their 
 generator is constraining class (ANY, if genericity is unconstrained).
 
 2. Contracts in clients of generic classes. Here some problems arise. If 
 we have an entity `x: ARRAYED_LIST[INTEGER]', its unfolding involves 
 processing the `item' query. `item' is declared to be of type `G' in 
 ARRAYED_LIST and, as I understand, parsing is not enough (some type 
 analysis is needed) to infer that `G' means `INTEGER' in current 
 context. Two approaches to this problem, that I see at present, are: 
 perform such a type analysis in compile time (with the help of gobo 
 compilation facilities) or leave some unfolding work until runtime, 
 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.

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