behavior, for a well-formed program construct and correct data, that depends on the implementation and that each implementation documents