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