QuickCheck High Level Design

I can guess what the QuickCheck High Level Design is for, but can you explain it anyway?

It's the design of the QuickCheck plugins. These are VDMJ and LSP plugins that add the qc and qr commands to the VDMJ and LSP consoles, and the ability to respond to the "QuickCheck" button in the VDM-VSCode GUI.

Does it follow the same style as the other VDMJ designs?

Naturally! :-)

So who would read this one?

If you wanted to do some work on QuickCheck, or if you wanted to add more related commands or LSP messages, this would be a useful place to help you understand the code. It doesn't help with the process of creating and checking proof obligations though. There are some wiki pages that help explain that process.

So can you give us a quick outline of the doc?

Of course. So it starts with a very quick overview of what proof obligations are and what the top level Java packages do. Then it shows a diagram of the main classes that are involved -- an architectural diagram, showing how VDMJ and LSP have separate support classes that call through to a common implementation.

Okay. Then?

Then it goes through each package, listing the classes involved and giving a short description of what the classes do and how they all hang together.

Each package section also includes a "Comments" subsection, which is a chance to describe the shortcomings or reasons for unusual aspects in the design, rather than cluttering the main description.

I remember seeing Comments in other designs. So is that all?

A section covers the usage of the two commands, qc and qr. Though as I said, this isn't really about explaining how to verify a model, it's just about what the various tool options do -- there are quite a lot of options in qc!

Lastly, a section gives a walkthrough of the built-in "random" strategy, and an "example" strategy that is included with the source code. It uses these to give advice about how to write your own strategies.

Okay, thanks for the summary.