Robert wrote:I also observe the inconsistency of Josef's stance: he wants to keep the large amount of unhelpful and irrelevant extra text in the Mod file, but objects to the relatively modest amount of extra, relevant, and helpful text in the Docu file.

The additional text in the Math module source is not read by normal users. It is only for developers.

The text in the Math docu is read by normal users. This makes the difference.

I was also trying to find a formulation that is nice and compact but have given up

because whatever I did it was not compact or not nice.

This is really an intricate task.

Anyway, here are some remarks that may us bring a step closer to a nice docu.

The first point is the formulation of the function's meaning:

"quadrant-correct principal value of the argument"

For me this is a very abstract scientific formulation; most simple minded users (including me!) know this as the "angle"

of the complex number. I would suggest to add this term as an alias such as:

"quadrant-correct principal value of the argument (the angle)"

The general post condition should remain, I think. This is simple and in line with the existing docu.

In addition I would add the reference to the IEEE 754-2008 standard indeed.

This saves at least the expert the time to compare all values in the table just to find

out that it is the same as everywhere.

Then comes the special cases table but with y first, i.e. same order as in the parameter list.

Non-special cases should be removed because this table lists the special cases.

Sample values +/-1 should be replaced by ranges PF and NF for positive finite and negative finite.

I would suggest to use the CP keyword INF instead of the infinity symbol.

It may be more beautiful for a mathematician but it contradicts existing conventions

used throughout the module's docu.

It's also easier for textual search, e.g. Search In Docu returns all instances of INF.

Same for pi.

There is nothing that speaks against using a ruler in the docu, as far as I know.

Don't forget to add another ruler after the table.

With these considerations the post condition would look like this:

- Code: Select all
`Post`

-pi <= result <= pi

result follows IEEE 754-2008; special cases are listed below where

PF means the range (0, INF) and NF means the range (-INF, 0)):

y x result y x result

−INF −INF − 3 pi / 4

NF −INF − pi

−0. −INF − pi

+0. −INF pi

...

The cases for all INF and all 0 may be reordered to keep them together.

Or should we go counter clockwise from +0. to -0.? What is the best order?

What was the old order? Was there one?

Another open detail is the notation for positive zero. Should it be 0 or +0 or 0. or +0.?

"0" is shortest and converted in CP to "+0.". "+0." is symmetric with "-0.".

"+0" and "0." are somewhere in between. I have a weak preference for "+0.".

- Josef