Difference between revisions of "CITADEL"
(→Discussions) |
|||
| Line 7: | Line 7: | ||
* Flattened variables | * Flattened variables | ||
Nadia: Daikon can process values of only few types: five scalar types (boolean, | Nadia: Daikon can process values of only few types: five scalar types (boolean, | ||
| − | integer, double, string and hashcode) and five more types, which are | + | integer, double, string and hashcode) and five more types, which are |
| − | arrays of these scalars. | + | arrays of these scalars. |
| − | So, if in Eiffel code we a have a variable of one of basic types | + | So, if in Eiffel code we a have a variable of one of basic types |
| − | (BOOLEAN, NATURAL, INTEGER, REAL or STRING) we can print its value | + | (BOOLEAN, NATURAL, INTEGER, REAL or STRING) we can print its value |
| − | directly as if it has one of Daikon's types. | + | directly as if it has one of Daikon's types. |
| − | If, however, we have a variable of any other type, we have to collect | + | If, however, we have a variable of any other type, we have to collect |
| − | all the information about it that is of interest and is available at | + | all the information about it that is of interest and is available at |
| − | certain program point, and present this information to Daikon as a set | + | certain program point, and present this information to Daikon as a set |
| − | of variables, which have Daikon types. The information of interest | + | of variables, which have Daikon types. The information of interest |
| − | about a variable includes results of all queries that can be called on | + | about a variable includes results of all queries that can be called on |
| − | this variable at this program point. However, since queries results may | + | this variable at this program point. However, since queries results may |
| − | themselves be of non-basic types, we have to perform this operation | + | themselves be of non-basic types, we have to perform this operation |
| − | recursively (to a certain depth). | + | recursively (to a certain depth). |
| − | For a reference variable information of interest includes also its | + | For a reference variable information of interest includes also its |
| − | address (Daikon type "hashcode" is intended for representing object | + | address (Daikon type "hashcode" is intended for representing object |
| − | addresses). | + | addresses). |
| − | For example, if we had a variable c: POINT, queries of class POINT | + | 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: | + | 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 | + | 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}. |
Revision as of 05:50, 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}.
