B.1.1 Initialize_Status Procedure

The main documentation of the Initialize_Status Procedure contains additional explanation of this code listing.

  subroutine Initialize_Status (S)

    ! Output variable.

    type(Status_type), intent(out) :: S  ! Status to be initialized.

    !~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    ! Verify requirements - none.

    ! Initializations.

    S = 'Unset'

    ! Verify guarantees.

    VERIFY(Valid_State(S),1)  ! S is now valid.

    return
  end subroutine Initialize_Status