查看文章

A rely/guarantee specification for a program P is a specification of the form R ⊃ G (R implies G), where R is a rely condition and G is a guarantee condition. A rely condition expresses the conditions that P relies on its environment to provide, and a guarantee condition expresses what P guarantees to provide in return. This paper presents a proof technique that permits us to infer that a program P satisfies a rely/guarantee specification R ⊃ G, given that we know P satisfies a finite collection of rely/guarantee specifications R _i ⊃ G _i , (i ∈ I). The utility of the proof technique is illustrated by using it to derive global liveness properties of a system of concurrent processes from a collection of local liveness properties satisfied by the component processes. The use of the proof rule as a design principle is also considered.