Core Modules
The core modules are written in pure Java and all their dependencies are managed exclusively through Maven. This makes building and working on them a fairly straightforward process (see this link for some quick Maven instructions).
Fundamentally, all modules are built around the Abstract Syntax Tree (AST).
The AST is an in-memory representation of the VDM model being worked on.
The Parser is responsible for reading a VDM source and constructing its
tree. The Type Checker is responsible for validating a tree. Practically
all use cases for Overture involve a type checked AST. However, most modules
should not need to interact with the Parser nor the
Type Checker (but see further below) and instead should have a type checked AST
provided to them. The task of constructing this AST should fall to an overall
core module and only comes into play when interacting with the user. For
example, the interpreter should only concern itself with executing an AST.
How that AST came to be is of no importance to the interpreter.
The following figure gives an idealized an overall view of the modules and their
interdependencies. It does not match the Maven modules on a 1 to 1 basis since
it groups a few of them (for example Combinatorial Testing represents 2
Maven modules), But it should give you a good idea of the overall architecture of the
Overture core. If you're curious, here is the whole
thing.
Each module is explained below but there are some points worth making right away:
- Most modules should interact only with the AST (either to build/analyze it) and with
the
Test Framework. - The
Test Frameworkconsists of some utility methods to use VDM sources as inputs and XML files as results. Most modules use it for testing, as expected. -
Command LineandGUI Builderare isolated because they are not really modules in the same sense as the rest. TheCommand Lineis just a bash script to wrap the core jars and theGUI Builderis an externally developed VDM tool that we bundle with Overture - A few of the plug-in modules need to interact with each other:
- The
POGuses thePretty Printerto format its output -
Combinatorial Testinguses theInterpreterto execute the generated tests.
While the current architecture is a significant step up from previous efforts, there are still some problems. The biggest issue is a lack of an overall module to coordinate the work between the various plug-ins. This is the reason why several plug-ins depend on each other. This issue occurs primarily when exposing functionality to the user. It is significantly less relevant on the IDE side where this kind of coordination code exists. But on the core side the lack of a coordinator introduces several additional dependencies that are not really needed.
Almost all Overture modules need to to interact with the AST. However,
direct interaction with the tree is highly discouraged. This should be
done with the visitor pattern. The AST contains a series of abstract
visitors and interfaces that can be subclassed as necessary. See the
Visitor Guide for details of how to build and use visitors.
The base functionality of most modules is implemented as a series of visitors.
For, example the Type Checker consists of visitors that
Assistants are responsible for providing generic functionality that is required in multiple situations and that (for various reasons) cannot be implemented directly as a visitor. Once created, assistants are typically invoked from within a visitor as necessary. See the Assistant Guide for more information on assistants.
Consists of 2 very simple scripts (bash and bat) to run the command line version of Overture. These scripts essentially wrap the call to the main Overture jar. They are not actually connected to any of the modules so their influence on the architecture is none. Still, they are mentioned for completeness' sake.
This is an externally developed that is currently being bundled together with Overture. This module also has no impact on the Overture architecture.
This is the central module of Overture. The AST module provides a series of
classes that implement an AST for VDM. It consists mainly of node classes (the
INode hierarchy) that represent the nodes of the tree and a series
of abstract visitors that can be subclassed in order to implement new
functionality visitors. Both the nodes and visitors are generated automatically
with the ASTCreator tool from a specification file.
In addition to the auto-generated classes, there are several utility and support classes. The most notable are:
-
AstFactory, as the name implies, provides a factory for constructing most nodes in the tree. If you need to construct nodes for some reason, you are strongly encouraged to use this. - Assistants providing a series of generic functionalities.
- Lex classes providing an implementation of the various kinds of tokens present in a VDM grammar.
As for the tree itself, it is very large and complex (around 300 nodes). This
is because VDM itself is a rather large language (3 dialects) with a lot of
syntax and the Overture tree follows the grammar very closely, practically on a
1-to-1 basis. As such the best way to familiarize yourself with the tree is to
study the VDM grammar, available in the VDM language manual that ships with
Overture (it can also be found in the documentation folder of the
repository).
| Relation | Modules |
|---|---|
| Depends on: | None |
| Dependency of: |
Parser, Type Checker, Pretty Printer ,POG, Combinatorial Testing, Code Generator, Interpreter, Pro B Solver
|
This is a support module for testing purposes. Its main functionalities are
are to process test inputs and compare/store test results. In order to use it,
you must subclass a TestCase and a TestSuite classes and implement
a handful of methods for result handling. The framework itself is quite
generic and does not actually depend on any other modules so it's usage is not
necessarily specific to Overture/VDM. However, the framework's handling of
result files is compatible with other VDM tools and so it enables the usage
of additional tests. A crash user guide is available here.
| Relation | Modules |
|---|---|
| Depends on: | None |
| Dependency of: |
Parser, Type Checker, POG, Combinatorial Testing, Code Generator, Interpreter, Pro B Solver
|
This module is responsible for constructing an AST from VDM source files. The
Overture parser is handwritten and while quite efficient, is challenging to
maintain. The parser provides utility classes and methods to turn an input
(String, File...) into an AST. These are used by various modules and are, in
general, problematic since the parser should not be depended upon
by modules that have no concept of VDM sources. Many of these usages are
strictly for testing purposes since the only way to construct any but the most
trivial AST is to write a VDM source and parse it. As such we have omitted
these connections from the idealized diagram.
The parser dependency issue should be alleviated by introducing a framework to
directly manipulate the AST for testing purposes. In addition, the dependencies
on the parser themselves should be made looser since at the moment they exist
as static calls to parser methods which makes it harder to replace/change the
parser. It also makes extending the modules problematic since the static
calls cannot easily be hooked into. In general, there should be an intermediate
facade module to provide parsing(and type checking) functionalities to all
other plug-ins.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Test Framework
|
| Dependency of: |
Type Checker, POG, Code Generator
|
This module is used following the parser in almost all use cases for
Overture. It is responsible for type checking an AST which consists of
validating the types and setting them on all nodes across the tree. Much
like the parser, there are utility methods for type checking an AST but also
for producing a type checked tree from a VDM source. These methods are used in
similar contexts as the ones from the parser and suffer from the same issues.
There is also the fact that it's possible to build a type checked tree directly
through the type checker or in two steps by using first the parser and then
the type checker. In general, this kind of duplication only serves to muddle
things. There should be a single way to perform such a basic and standard task.
Unlike with the parser, the type checker has additional utility methods
that are used in the production code. These methods perform various kinds of
functionalities such as, for example, testing if a given union type contains a
boolean type. Most of these utilities are exported through the assistant system
so they do not pose as much of an extensibility issue. However, from a
conceptual point of view, while many of these features are crucial, they are
not features of the type checker itself but rather of the VDM type system.
The type checker should be separated into two modules: a type checker
module that is only responsible for validating a tree and that would contain
most of the visitors and code for traversing a tree; and a type system module
with the various utilities that would allow a developer to more easily
interact with the VDM type system. It's possible that these modules would be
tightly coupled and the type checker would surely make extensive use of the
type system. But this would allow other modules to disconnect from the
type checker which would be important since the other modules have no notion
of type checking a tree. For them, all trees are type correct.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Test Framework, Parser
|
| Dependency of: |
Pro B Solver, POG, Interpreter, Code Generator
|
This module is used for printing an AST, ie, converting it to a String. The
module depends only on the AST and can be used by any module that wishes
to display a tree to the user. At the moment, that includes only the POG. The
module is implemented mostly as a series of visitors that walk the tree and
produce a String for any given node.
Please note however, that this module is very outdated and incomplete.
It's functionality can be (badly) approximated by toString() methods in the
AST nodes and that is what most modules end up using.
| Relation | Modules |
|---|---|
| Depends on: | AST |
| Dependency of: | POG |
This module is used for generating Proof Obligations for a VDM model that, if discharged, ensure the internal consistency of the model. The POG is particular
in the sense that both its input and output are ASTs.
The POG relies on the Type Checker for interacting with the VDM type system and the Parser for testing purposes, both of which are considered a bad
code smell.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Pretty Printer, Type Checker, Parser, Test Framework
|
| Dependency of: | None |
This module is used to generate tests for a model, based on user-specified traces. The module is also responsible for executing the generated tests.
| Relation | Modules |
|---|---|
| Depends on: | Interpreter |
| Dependency of: | None |
This module is responsible for generating source code (Java/C++...) based off a VDM model. It is still in early stages of development and subject to heavy changes.
The Code Generator relies on the Type Checker for interacting with the VDM type system and the Parser and Interpreter for testing purposes, all of which are considered a bad code smell.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Parser, Type Checker, Interpreter
|
| Dependency of: | None |
This module is responsible for executing VDM models and interacting with the
user. Because it interacts with the user, it also implements significant
portions of the command line interface, such as access to the POG. This
is considered a code smell.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Type Checker, POG, Test Framework
|
| Dependency of: |
Combinatorial Testing, Pro B Solver
|
This module integrates Overture with the Prob B tool to enable the execution of implicit VDM definitions.
This module is composed of two sub-modules. One of them implements the actual
Pro B connection. The other provides integration between the Pro B Connection
and the Interpreter in order to execute the models. This is a potential
alternative to organize the core modules with various integration modules
instead of the single orchestration module.
| Relation | Modules |
|---|---|
| Depends on: |
AST, Type Checker, Interpreter
|
| Dependency of: | None |