Difference between revisions of "CITADEL"
(→Discussions) |
(→Discussions) |
||
| Line 27: | Line 27: | ||
POINT' and flattening depth were set to 2, then `c.flattened' would be a | POINT' and flattening depth were set to 2, then `c.flattened' would be a | ||
set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}. | set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}. | ||
| + | |||
| + | Containers need special kind of flattening. 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. | ||
Revision as of 06:51, 14 December 2007
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
- Flattened 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 flattening depth were set to 2, then `c.flattened' would be a
set of variables: {$c, c.x, c.y, $c.twin, c.twin.x, c.twin.y}.
Containers need special kind of flattening. 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.
