Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability

Abstract

In this paper the problems of parameter passing and implementation for parameterized algebraic specifications are studied on a proof theoretic level.A syntactic equivalent to the semantic notion of persistency deemed by the ADJ group is introduced for parameterized specifications.It is shown to lead to similar results concerning the correctness of parameter passing and the nesting of parameters.Then a formal notion of implementation is developed for persistent specifications.It allows for developing implementations in a stepwise fashion.Moreover, implementations for instantiations (i.e., specifications that result from applying a parameterized specification to an actual parameter) can be constructed mechanically from given implementations for the specification procedure and the actual parameter.Correctness of implementation is required only with respect to observable properties of a specification, so an increased amount of optimization is allowed.