A case study of the formal development of an object manager