Multi-level specifications based on traces
Paulo A. S. Veloso, Antonio Luz Furtado · ACM SIGSOFT Software Engineering Notes · 1983
A methodology for the formal specification of data base applications is presented. Central to the methodology is the idea of proceeding through successive levels of "traces", which enables an initial algebra specification to be obtained from one based on preconditions and effects. Besides being executable these trace levels provide a way to go from a natural language specification to an algebraic one.