Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Ali E. Abdallah , South Bank University
In recent years, there have been growing interests in systematic methods for refining Z specifications into programs. In this paper, we consider a transformational programming strategy known as filter promotion and examine its use for refining a class of Z specifications into sequential as well as parallel programs. This strategy is particularly useful for transforming specifications of generate and test problems into efficient algorithms. We find it convenient to use different notations at different level of abstractions: Z to capture the starting specification, Bird-Meertens functional notation to express algorithms and Hoare's CSP to describe parallelism and communications. The basic ideas are illustrated by systematic transformational developments of sequential and parallel algorithms for sorting and searching problems.
Specification, refinement, program transformation, filter promotion, accumulation, parallelism, communicating processes
A. E. Abdallah, "Filter Promotion Transformation Strategies for Deriving Efficient Programs from Z Specifications," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 157.