DTRE -- a semi-automatic transformation system. This paper describes the theoretical framework and an implemented system (Dtre) for the specification and verified refinement of specifications using operations on abstract data types. The system is semi-automatic in that users can specify some (possibly none) of the implementations and the system will determine the rest of the implementations. Data types are specified as parameterized theories within many-sorted first-order logic; usually these theories are centered around inductive sorts. Abstract specifications (theories) are refined in a stepwise fashion into increasingly more concrete theories. Our primary method of refinement is based on theory interpretation [1, 2, 3]. Theories and interpretations provide a clean, logically based separation between types and their implementations; thus permitting specification to proceed independently of implementation while simultaneously providing a basis for rapid and verifiably correct transformation to efficient code. Dtre provides a conven..
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam: Fiat: deductive synthesis of abstract data types in a proof assistant (2015)
- Tomasik, Jerzy; Weyman, Jerzy: Category localization semantics for specification refinements (2007)
- Smith, Douglas R.: Constructing specification morphisms (1993)