Library Writers Guide

I'm guessing the Library Writer's Guide is for people who want to write libraries?

Yes, that's right.

Is that a common thing to do?

No, actually it's quite rare. You might consider it if you had lots of VDM different specifications that had a common core of functions. Or you might consider writing a VDM library to call a specialised native Java library, so that other VDM writers can access it too. The guide has some more examples of things you can do with libraries.

Is it difficult to write a library?

No, not at all. If you want to link to native Java, you have to write your Java methods in a particular way and then match those as functions or operations in VDM using is not yet specified as the body. Libraries written in pure VDM don't need to do anything special. If you want a library to be used by the VSCode extension, you need to include a special META-INF file in a particular format. But that's all.

And the standard libraries are the same?

Yes, exactly. So you can look at how they're written as a good example. The document just brings it all together. It isn't very large.

So briefly, how is the document structured?

It starts with an overview and explains how library code is linked with VDMJ. Then it gives detail of how to write the Java and linking VDM functions. There is a section about the META-INF file for VSCode. And lastly there are some examples of what you might use a library for.

And to use them, you just put them on the classpath, like annotations?

Exactly. It's easy!

Okay, thanks for that.