High Precision Guide

I thought VDM was all about being precise, so what is the High Precision Guide for?

Well, usually VDMJ uses the standard precision numeric types within Java to do calculations. So all of VDM's integer types are held in 64-bit Java longs, and real/rational values are held in Java doubles. That is fine for 99% of specifications, which don't need to handle extremely large integers or floating point numbers to more than 15 decimal places. But in some rare cases, the Java types are not big enough.

But a 64-bit number is huge! Who would need numbers bigger than that?

Yes, true. But for example, I had to produce a specification recently which had "MAX" constants that were unsigned 64-bit quantities. Since Java longs are always signed, these constants would not fit using the standard precision build. So I had to move the specification over to the high precision build.

And what is the high precision build, exactly?

It's a different build of VDMJ that uses BigIntegers and BigDecimals to represent integer and floating point numbers. The floating point values additionally have a "precision", which defines the number of significant digits that you want to have. It defaults to 100 decimal places.

Remind me how many decimal places are in a Java double?

It's around 15 or 16. So you can see that we're adding a lot of precision by default, and you can set that precision much higher if you need it.

I see. So the specification you mentioned works with high precision?

Yes. A BigInteger can contain arbitrarily large integers, so an unsigned 64-bit value is no problem. Any specification that works in standard precision should work in high precision, but not the other way round.

Cool. But why do we have to have two separate builds of the tool? Couldn't we do everything with high precision?

We could, but it's much slower to do all arithmetic using the "Big" classes, especially with large precision values. Since 99% of specifications don't need this, it seemed better to not slow everything down for the 1%. So you'll see there are Java jars with "-P" in the release repository. These are the high precision jars.

And the guide?

That just shows the extra options that are available. It amounts to a new -precision command line option and a precision command in the interpreter for changing it on the fly. It's just two pages.

There are some very cool examples in the guide too, like Euler's constant shown to 1000 decimal places.

Yes, there's something intriguing about very high precision values. But it has a serious purpose too!