B.1.17 Status_Not_Equal_Status Procedure

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

  function Status_Not_Equal_Status (S1, S2) result(Not_Equal)

    ! Input variables.

    type(Status_type), intent(in) :: S1, S2  ! Status variables to be compared.

    ! Output variable.

    type(logical) :: Not_Equal               ! Nonequality boolean.

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

    ! Verify requirements.

    VERIFY(Valid_State(S1),1)   ! S1 is valid.
    VERIFY(Valid_State(S2),1)   ! S2 is valid.

    ! Check nonequality.

    Not_Equal = S1%status /= S2%status

    ! Verify guarantees.

    ! Not_Equal should be what it was set to.
    VERIFY(Not_Equal .eqv. (S1%status /= S2%status),2)

    return
  end function Status_Not_Equal_Status