Skip to content

Differences between Overture and VDMTools

Jump to bottom Edit New page
Nick Battle edited this page Oct 29, 2018 · 6 revisions

This page lists the known differences between Overture and VDMTools.

Table of Contents

Dialect Support Differences

The tools differ in the VDM dialects supported:

  • Overture supports VDM-SL, VDM++ and VDM-RT.
  • VDMTools only supports VDM-SL and VDM++

RM Differences

As Language Board RMs are introduced, tools implement them at different times. The following RMs have not been implemented in both tools as yet:

  • VDMTools does not support the reverse keyword. Overture supports it in VDM10.
  • The stop and stoplist statements are available in Overture only
  • Any RMs to do with VDM-RT are only available in Overture, as VDMTools does not support VDM-RT
  • Unlike Overture, VDMTools cannot have an expression in a periodic thread definition, only an integer literal
  • Both tools implement Object Patterns, but VDMTools allows them to be called from functions, which Overture does not.
  • VDMTools does not yet implement pure operations.

Parser Differences

There are some small differences in the way Overture and VDMTools parse specifications. Generally speaking, Overture is more forgiving.

  • Overture will allow either order of imports and exports in a module header, VDMTools requires imports then exports.
  • Overture will allow you to omit semi-colon separators between imports/exports clauses, VDMTools requires them.
  • Overture will allow either order of inv and init clauses in a state definition, VDMTools requires inv before init.
  • Overture will allow any order of inv, eq and ord clauses in a type definition, VDMTools requires inv, eq, ord
  • Overture will allow you to put a semi-colon separator between traces, VDMTools will not.

Type Checker Differences

There are some differences in the detail of the type checking between VDMTools and Overture:

  • VDMTools can type check with both possible and definite semantics, Overture has only possible semantics.
  • Overture and VDMTools differ on the form of measures for recursive curried functions (VDMTools has curried measures, Overture does not).
  • Overture defines a non-standard "?" representing any type, which is used in some libraries, like println: ? ==> () to print a value of any type.
  • Overture can sometimes cope with forward references, but VDMTools cannot.
  • Overture allows type invariant variables to have the same name as the type, VDMTools does not.

Language Differences

There are some cases where the tools disagree about the correct form or behaviour of a specification:

  • VDMTools will implicitly export names from a module in some cases; Overture requires an explicit exports all for this.
  • There are several subtle differences in object oriented semantics between the tools for VDM++ (this whole area is poorly defined):
    • Calling an overridden operation in a constructor calls the local version in Overture (like C++), but the overridden version in VDMTools (like Java).
    • Constructors are not inherited by subclasses in Overture, but they are in VDMTools
    • VDMTools does not produce pre_op and post_op functions for operations in VDM++. Overture defines non-standard ones.
    • For more details, see Object Oriented Issues in VDM++
  • Overture doesn't implicitly import a function's pre_ and post_ functions (if any), or a type's inv_ etc. VDMTools does.
  • VDMTools always(?) allows a function to call an operation. Overture does not permit this with the VDM10 option enabled.

Operational Differences

There are some differences in the way the tools evaluate the same specification. Both should be within the permitted definition of the language semantics, but they do not necessarily produce the same result where looseness is concerned. Some cases are very unintuitive.

  • For example, exists1 {x, y} in set { {3, 4} } & x=3 and y=4 is true in Overture, but false in VDMTools. Both are valid.
  • Both VDMTools and Overture have deterministic schedulers, but they do not schedule threads in the same way as each other.
  • Overture can evaluate type binds for finite types. VDMTools cannot (yet). eg { b | b : bool } is {true, false} in Overture.
  • Overture will evaluate and check recursive measures for functions. VDMTools will not (yet).

Feature Differences

The two tools offer some different features

  • VDMTools supports C++ and Java code generation, Overture only supports Java, though C++ is in progress.
  • VDMTools has some support for Java to VDM++ conversion
  • VDMTools will generate LaTeX output for the mathematical notation (Pretty Printing)
  • VDMTools can read source from LaTeX, RTF or plain text, Overture supports LaTeX, Word (.doc/.docx), ODF (OpenOffice etc) and plain text.
  • Overture can produce coverage reports in Word or LaTeX format, VDMTools only supports LaTeX(?)
  • Overture (VDMJ) provides a Java JUnit test framework.
  • VDMJ has an experimental build that uses arbitrary precision arithmetic.

What should I do when I discover other issues?

Please send an e-mail to overturetool-core@overturetool.org, and we will get back in touch with you.

Add a custom footer

Language Board Wiki

Main Pages

Processes

Specific Issues

Clone this wiki locally