Printing to console in VDM++?

Question

How do I print text or values to the console to validate that my model is working correctly?

I would like to do something like this:

class Main
operations
    public Run: () ==> ()
    Run() ==
        print "Text"
        print mon.Func()
end Main

It seems to be possible, but I just cant figure out how to do it.

Answer 1

Nick Battle answered my question but for other beginners to VDM, there is missing a detail to his answer, how to include libraries.

Before one can use the IO library, you first have to include it. I am using Overture and to include libraries into your project, you have to right-click on the project in the side menu and press New > Add VDM Library. You can then choose which libraries you want to include in a menu that pops up. Here you choose IO.

After this you should be able to print out values using the IO`println(val) function.

Answer 2

You need to use the VDM IO library. There are a couple of operations that do what you want - println (for printing fixed values) and printf, which has parameter substitution. So you would call IO`println("hello"), for example.

In the latest release of Overture and VDMJ, you can also use a VDM annotation to print values without adding anything to the "content" of the specification itself. Annotations are rather added as comments. See @Printf.