This paper introduces a tool that automatically translates a concrete form of specifications into C code linked with BSPlib. The translation tool is rigorously developed with important safety properties proved. A LOGS specification for Bulk-Synchronous Parallelism is a relation of an initial state, a final state and some intermediate states. Nondeterminism and parallelism correspond to disjunction and conjunction respectively. Various advanced specification commands can be derived from the basic ones. The translator checks syntax, freedom of communication interference, type consistency and communication dependencies before generating the target code. Static analysis (including both static checkings and translation) is presented in abstract interpretation. It is shown that a few laws are complete for transforming any specification into a normal form. These laws are satisfied by the abstract functions. We demonstrate the actual effects of the abstract functions by applying them on the normal form. The approach has been implemented using an object-oriented language. © Springer-Verlag Berlin Heidelberg 2005.

Zhou J., Chen Y.

707.pdf    Gửi cho bạn bè

Từ khóa : Abstracting; Computer aided language translation; Object oriented programming; Parallel processing systems; Specifications; Specification commands; Static analysis; Syntax; Code converters