DTRE (Data Type Refinement Environment) Project

DTRE is a system for analysis and optimization of programs, primarily through the selection and synthesis of efficient implementations of high level data types such as sets and sequences. It is built in REFINE and is used in KIDS.

DTRE facilitates the capture and (re)use of programming knowledge expressed at a very high level:

• Data Types specified as Theories
• Data Type Refinements specified as Theory Interpretations
• Implementations specified as compositions of Refinements
• Applicability Conditions for Refinements
• Data Structure Selection Rules

The use of DTRE is also at a high level. Users specify (or change) implementations by annotating program objects with the directives for the desired implementations. DTRE is a semi-automatic system: users specify implementations of some objects and DTRE selects (based on program analysis) the remaining implementations.

A typical interaction is the select (specify), synthesize, test and collect data, analyze loop used (for example) when modifying specs to meet a performance constraint.