I read here https://wiki.eclipse.org/OCL/FAQ that
How do I access unnavigable opposites in Ecore
In UML, an association that is intended only to be navigated in one direction at run-time may be drawn with a unidirectional arrow.
OCL evaluation occurs at analysis-time and may navigate in both directions regardless of the arrows.
Is this part of the OCL standard or only an eclipse ecore thing?
An example: Given two classes A and B, and a uni-directional association from A to B (but not from B to A). In a class diagram, this could be illustrated with an arrow from A to B (a line with one arrowhead pointing to B).
Is it really part of the standard to write OCL constraints that navigate against this arrow direction?
I could not find anything about this in the OCL spec, see here.
The navigability indication in UML is not absolute, but merely an indicator of how you can easily navigate.
From the UML 2.5 specs
Navigability means that instances participating in links at runtime (instances of an Association) can be accessed efficiently from instances at the other ends of the Association. The precise mechanism by which such efficient access is achieved is implementation specific. If an end is not navigable, access from the other ends may or may not be possible, and if it is, it might not be efficient.
So therefore I guess OCL should be able to navigate in both ways, regardless of the navigability.