As further reading with respect to the verification of programs, I recommend [AptO] and [Dahl92]. An assertion logic for a parallel object-oriented language is presented in [AmBo93].