[ref_impl_eiffel] [971] Add a missing postcondition.

Revision: 971
Author: peter.gummer
Log Message: