The main documentation of the Status_Equal_Status Procedure contains additional explanation of this code listing.
function Status_Equal_Status (S1, S2) result(Equal)
! Input variables.
type(Status_type), intent(in) :: S1, S2 ! Status variables to be compared.
! Output variable.
type(logical) :: Equal ! Equality boolean.
!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
! Verify requirements.
VERIFY(Valid_State(S1),1) ! S1 is valid.
VERIFY(Valid_State(S2),1) ! S2 is valid.
! Check equality.
Equal = S1%status == S2%status
! Verify guarantees.
! Equal should be what it was set to.
VERIFY(Equal .eqv. (S1%status == S2%status),2)
return
end function Status_Equal_Status