EiffelStudio: an EiffelSoftware project - User contributions [en]

CITADEL

2007-12-25T12:33:31Z

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

[[Category:Assertion checking]]

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

CITADEL

2007-12-25T12:28:00Z

Nadia Polikarpova: /* Support for loop invariants */

CITADEL

2007-12-25T12:22:37Z

Nadia Polikarpova: /* Unfolded variables */

[[Category:Assertion checking]]

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

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.

CITADEL

2007-12-25T12:17:43Z

Nadia Polikarpova: /* Unfolded variables */

[[Category:Assertion checking]]

==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, 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.

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.

CITADEL

2007-12-25T12:16:38Z

Nadia Polikarpova: /* Unfolded variables */

[[Category:Assertion checking]]

==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, 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...

Nadia: 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.

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.

CITADEL

2007-12-25T12:13:42Z

Nadia Polikarpova: Added topics: "chechink preconditions" ("static vs. dynamic" and "wrapping vs. qualification") and "checking hand-written contracts"

[[Category:Assertion checking]]

==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, 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.

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.

CITADEL

2007-12-25T11:07:11Z

Nadia Polikarpova: Term "flattening" changed to "unfolding"

CITADEL

2007-12-25T11:06:04Z

Nadia Polikarpova: Term "flattened" changed to "unfolded"