B.1.3 Finalize_Status Procedure

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.

  end subroutine Finalize_Status

Michael L. Hall