I recently discovered that I have a fondness for the work of Dijkstra. I am currently reading random EWDs, and stumbled across one with some notation that I couldn't quite grasp.
Dijkstra states that $[ x < y \implies f.x.y < f.y.x]$
OK, so. This isn't a list comprehension, right? Why the brackets?
Also, how could this be read aloud? What does $\implies$ mean?
And finally, what does $f.x.y$ and $f.y.x$ mean?
And how could this statement be written more conventionally? And does Dijkstra's notation derive from anything, or is it entirely his own invention?