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 06: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}.