Paulo Borba and Joseph A Goguen
November 1994, 28pp.
FOOPS is a concurrent object-oriented language. Based on FOOPS operational semantics, we define a notion of refinement, and an associated proof technique. The use of refinement for stepwise formal development of programs in FOOPS is illustrated by examples involving memory cells, and different implementations of buffers.