|
|
Abstract:
Concurrent programming is a complex activity, which requires a formal approach for constructing correct algorithms. Based in the Owicki-Gries theory, Feijen and Van Gasteren have elaborated a method for developing concurrent programs from their specification. In this framework, since progress can not be expressed in general in the OG theory, derivations are driven only by safety requirements, and the progress constraints are satisfied in a later stage. But in most algorithms, an important amount of the code is there for guaranteeing progress and therefore any method that elides this requirement can produce only a portion of the final code. Other methods for deriving concurrent programs using progress requirements have been proposed that fall outside the OG theory, but they lack the former 's clear style and simplicity, and add more complexity to the problem being solved. In this work, we propose a method for deriving concurrent programs using progress requirements, and within the Owicki-Gries theory. For doing this we rely in a generalized bound function. Furthermore, a property regarding composition of multiprograms is given, and used for the construction of complex protocols out of simpler ones.
|