SPECIFICATION SpecProcedures8
INVARIANT ProceduresInvariant8
PROPERTY EventuallyReturns8