The main documentation of the Status_Not_Equal_Character Procedure contains additional explanation of this code listing.
function Status_Not_Equal_Character (S, C) result(Not_Equal)
! Input variables.
type(Status_type), intent(in) :: S ! Status variable to be compared.
type(character,*), intent(in) :: C ! Selector flag string to be compared.
! Output variable.
type(logical) :: Not_Equal ! Nonequality boolean.
!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
! Verify requirements.
VERIFY(Valid_State(S),1) ! S is valid.
! Check nonequality.
Not_Equal = status_flag(S%status)%selector /= C
! Verify guarantees.
! Not_Equal should be what it was set to.
VERIFY(Not_Equal .eqv. (status_flag(S%status)%selector /= C),2)
return
end function Status_Not_Equal_Character