Paulo Borba and Joseph A Goguen
November 1995, 39pp.
FOOPS is a concurrent object oriented language. Based on FOOPS operational semantics, we introduce a notion of refinement for states of FOOPS systems together with a proof technique for proving refinement. Using this notion, we define refinement of FOOPS (method) expressions and programs. Although we focus on FOOPS, our definition of refinement is independent of this language.
We also illustrate the use of refinement for stepwise formal development of programs in FOOPS. Based on that, we give an overall evaluation of our approach and comment on alternative approaches for the refinement of concurrent object oriented programs, concluding that none of them provide both a general definition of refinement and an effective proof technique such as the one presented here.