Universitat Politècnica de Catalunya. Departament d'Enginyeria de Serveis i Sistemes d'Informació
Publication date
1995-03
Abstract
A framework that combines imperative programs with algebraic specifications is presented. We focus on an execution mechanism that allows the arbitrary combination of programs and equations, which is based on the evaluation of expressions by means of the transformation of values from data structures to terms and vice versa, using the abstraction function of the implementation. The correctness of the execution procedure follows from a set of basic transformation rules.
