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 enormous floating point numbers. But in some rare cases, the Java types are not big enough.

That's a surprise! I mean, a 64-bit number is huge.

*Yes, true. But for example, I had to produce a specification recently which had 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's that, 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.

So the specification you mentioned, that works with high precision?

*Yes. A BigInteger can effectively contain arbitrarily large integers, so an unsigned 64-bit value is no problem.

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. 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.

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 high precision values. But it has a serious purpose too!