The main documentation of the Finalize_Status Procedure contains additional explanation of this code listing.
subroutine Finalize_Status (S)
! Input/Output variable.
type(Status_type), intent(inout) :: S ! Status to be finalized.
!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
! Verify requirements.
VERIFY(Valid_State(S),1) ! S is valid.
! Finalizations.
S%status = 0
! Verify guarantees.
VERIFY(.not.(Valid_State(S)),1) ! S is no longer valid.
return
end subroutine Finalize_Status