Understanding Dijkstra's notation $f.x.y$

Question

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?

Answer 1

I think this would read as follows in modern notation (although field-local variations are possible):

$$\forall x y. x < y \Rightarrow f(x,y) < f(y,x).$$

Read aloud: for all x and y, x is less than y implies that f of x and y is less than f of y and x.

If you read the first sentence of the linked document, it says that square brackets represent universal quantification over $x$ and $y$. The second states that $f$ is a function. => is ASCII art for $\Rightarrow$ (logical implication).

The main problem here is missing context (and detective skills). This article refers to EWD878. Perhaps looking there would have helped. Indeed, looking at that article, you see notation slightly closer to what is used today (at least, by Haskell programmers: f.x.y becomes f\ x\ y).