The Rely-Guarantee Method Thread Thread Environment ■Rely and Guarantee ■A,G:State→State>Prop Thread Modularity Non-Interference (interface compatibility): ■ij.i月→G,→A Safety of each thread ■T:(A,G) 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens The Rely-Guarantee Method ◼ Thread + Thread Environment ◼ Rely and Guarantee ◼ A, G: State → State → Prop ◼ Thread Modularity ◼ Non-Interference (interface compatibility): ◼ i,j. ij  Gi  Aj ◼ Safety of each thread ◼ Ti : (Ai , Gi )