Difference between revisions of "CITADEL"
| Line 1: | Line 1: | ||
[[Category:Assertion checking]] | [[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). | 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}. | ||
Revision as of 05:49, 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}.
