overturetool/overture

The Overture Tool

The Overture Tool

General Information

If you'd like general information about the Overture Project, we suggest you have a look at http://overturetool.org.

Development

Before you download and try to use the code provided in this open-source repository, please browse through the development wiki first!

This directory contains several subdirectories:

• The core Overture libraries are found in core, and are pure Java with no Eclipse dependencies
• The Overture IDE, based on Eclipse, is found in ide
• Technical Documentation for Overture is in documentation

Release

The release procedure is described here.

overture's Issues

NPE when opening file outside the workspace

The following bug was originally reported on Sourceforge by volkersf, 2009-11-19 14:16:39:

In oIDE, select File->Open and navigate to a VMD-file somewhere in the file system (not the workspace!). I tried with one of the POP3-vmdpp's while chatting with pgl today.

java.lang.NullPointerException
at org.overture.ide.parsers.vdmj.internal.VdmjSourceParser.parse(VdmjSourceParser.java:47)
at org.eclipse.dltk.core.SourceParserUtil.getModuleDeclaration(SourceParserUtil.java:120)
at org.eclipse.dltk.core.SourceParserUtil.getModuleDeclaration(SourceParserUtil.java:45)
at org.eclipse.dltk.core.AbstractSourceElementParser.parse(AbstractSourceElementParser.java:48)
at org.eclipse.dltk.core.AbstractSourceElementParser.parseSourceModule(AbstractSourceElementParser.java:28)
at org.eclipse.dltk.core.SourceParserUtil.parseSourceModule(SourceParserUtil.java:237)
at org.eclipse.dltk.internal.core.AbstractSourceModule.buildStructure(AbstractSourceModule.java:529)
at org.eclipse.dltk.internal.core.Openable.generateInfos(Openable.java:182)
at org.eclipse.dltk.internal.core.ModelElement.openWhenClosed(ModelElement.java:177)
at org.eclipse.dltk.internal.core.BecomeWorkingCopyOperation.executeOperation(BecomeWorkingCopyOperation.java:42)
at org.eclipse.dltk.internal.core.ModelOperation.run(ModelOperation.java:698)
at org.eclipse.dltk.internal.core.ModelOperation.runOperation(ModelOperation.java:763)
at org.eclipse.dltk.internal.core.SourceModule.becomeWorkingCopy(SourceModule.java:70)
at org.eclipse.dltk.core.WorkingCopyOwner.newWorkingCopy(WorkingCopyOwner.java:147)
at org.eclipse.dltk.internal.ui.editor.SourceModuleDocumentProvider.createFakeSourceModule(SourceModuleDocumentProvider.java:1702)
at org.eclipse.dltk.internal.ui.editor.SourceModuleDocumentProvider.createFakeSourceModule(SourceModuleDocumentProvider.java:1620)
at org.eclipse.dltk.internal.ui.editor.SourceModuleDocumentProvider.createFileInfo(SourceModuleDocumentProvider.java:1244)
at org.eclipse.ui.editors.text.TextFileDocumentProvider.connect(TextFileDocumentProvider.java:478)
at org.eclipse.dltk.internal.ui.editor.SourceModuleDocumentProvider.connect(SourceModuleDocumentProvider.java:1517)
at org.eclipse.ui.texteditor.AbstractTextEditor.doSetInput(AbstractTextEditor.java:4134)
at org.eclipse.ui.texteditor.StatusTextEditor.doSetInput(StatusTextEditor.java:203)
at org.eclipse.ui.texteditor.AbstractDecoratedTextEditor.doSetInput(AbstractDecoratedTextEditor.java:1413)
at org.eclipse.dltk.internal.ui.editor.ScriptEditor.internalDoSetInput(ScriptEditor.java:776)
at org.eclipse.dltk.internal.ui.editor.ScriptEditor.doSetInput(ScriptEditor.java:1259)
at org.eclipse.ui.texteditor.AbstractTextEditor$19.run(AbstractTextEditor.java:3115)
at org.eclipse.jface.operation.ModalContext.runInCurrentThread(ModalContext.java:464)
at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:372)
at org.eclipse.jface.window.ApplicationWindow$1.run(ApplicationWindow.java:759)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.jface.window.ApplicationWindow.run(ApplicationWindow.java:756)
at org.eclipse.ui.internal.WorkbenchWindow.run(WorkbenchWindow.java:2579)
at org.eclipse.ui.texteditor.AbstractTextEditor.internalInit(AbstractTextEditor.java:3133)
at org.eclipse.ui.texteditor.AbstractTextEditor.init(AbstractTextEditor.java:3160)
at org.eclipse.ui.internal.EditorManager.createSite(EditorManager.java:798)
at org.eclipse.ui.internal.EditorReference.createPartHelper(EditorReference.java:644)
at org.eclipse.ui.internal.EditorReference.createPart(EditorReference.java:462)
at org.eclipse.ui.internal.WorkbenchPartReference.getPart(WorkbenchPartReference.java:595)
at org.eclipse.ui.internal.PartPane.setVisible(PartPane.java:313)
at org.eclipse.ui.internal.presentations.PresentablePart.setVisible(PresentablePart.java:180)
at org.eclipse.ui.internal.presentations.util.PresentablePartFolder.select(PresentablePartFolder.java:270)
at org.eclipse.ui.internal.presentations.util.LeftToRightTabOrder.select(LeftToRightTabOrder.java:65)
at org.eclipse.ui.internal.presentations.util.TabbedStackPresentation.selectPart(TabbedStackPresentation.java:473)
at org.eclipse.ui.internal.PartStack.refreshPresentationSelection(PartStack.java:1256)
at org.eclipse.ui.internal.PartStack.setSelection(PartStack.java:1209)
at org.eclipse.ui.internal.PartStack.showPart(PartStack.java:1608)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:499)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:103)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:485)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:112)
at org.eclipse.ui.internal.EditorSashContainer.addEditor(EditorSashContainer.java:63)
at org.eclipse.ui.internal.EditorAreaHelper.addToLayout(EditorAreaHelper.java:225)
at org.eclipse.ui.internal.EditorAreaHelper.addEditor(EditorAreaHelper.java:213)
at org.eclipse.ui.internal.EditorManager.createEditorTab(EditorManager.java:778)
at org.eclipse.ui.internal.EditorManager.openEditorFromDescriptor(EditorManager.java:677)
at org.eclipse.ui.internal.EditorManager.openEditor(EditorManager.java:638)
at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditorBatched(WorkbenchPage.java:2854)
at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditor(WorkbenchPage.java:2762)
at org.eclipse.ui.internal.WorkbenchPage.access$11(WorkbenchPage.java:2754)
at org.eclipse.ui.internal.WorkbenchPage$10.run(WorkbenchPage.java:2705)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2701)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2685)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2668)
at org.eclipse.ui.ide.IDE.openEditorOnFileStore(IDE.java:1151)
at org.eclipse.ui.internal.ide.actions.OpenLocalFileAction.run(OpenLocalFileAction.java:107)
at org.eclipse.ui.internal.ide.actions.OpenLocalFileAction.run(OpenLocalFileAction.java:76)
at org.eclipse.ui.internal.PluginAction.runWithEvent(PluginAction.java:251)
at org.eclipse.ui.internal.WWinPluginAction.runWithEvent(WWinPluginAction.java:229)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:411)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:3543)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1250)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1273)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1258)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1079)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3441)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3100)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
at org.eclipse.equinox.launcher.Main.run(Main.java:1311)

Visibility of protected def

The following bug was originally reported on Sourceforge by pglvdm, 2009-05-24 11:37:21:

If the attaced vpp files are checked together there should be no type error. However, VDMJ TC reports one error here.

VDMRuntimeException when exporting as XMI

The following bug was originally reported on Sourceforge by volkersf, 2009-11-19 14:36:34:

In a VDM++-project, I have imported the Cashdispenser files. Right-click on the project, UML Transformation -> Export as XMI (to be continued below):

jp.co.csk.vdm.toolbox.VDM.VDMRunTimeException: Run-Time Error:Precondition failure in getSpecifications
at jp.co.csk.vdm.toolbox.VDM.UTIL.RunTime(UTIL.java:150)
at org.overturetool.ast.imp.OmlDocument.getSpecifications(OmlDocument.java:89)
at org.overturetool.umltrans.Main.Translator.TranslateVdmToUml(Translator.java:40)
at org.overturetool.umltrans.Main.Translator.TransLateTexVdmToUml(Translator.java:56)
at org.overture.ide.plugins.umltrans.actions.Vdm2UmlAction$1.run(Vdm2UmlAction.java:113)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

Wondering if it might be stumbling about the "test" package/folder that was present from the import, I deleted that one and then got:

jp.co.csk.vdm.toolbox.VDM.VDMRunTimeException: Run-Time Error:Illegal index
at jp.co.csk.vdm.toolbox.VDM.UTIL.RunTime(UTIL.java:150)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.buildParameters(Vdm2Uml.java:1410)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.buildFunction(Vdm2Uml.java:1628)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.build_udef_ublock(Vdm2Uml.java:1549)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.build_udef_ub(Vdm2Uml.java:605)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.build_uClass(Vdm2Uml.java:307)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.build_uuml(Vdm2Uml.java:188)
at org.overturetool.umltrans.vdm2uml.Vdm2Uml.init(Vdm2Uml.java:110)
at org.overturetool.umltrans.Main.Translator.TranslateVdmToUml(Translator.java:40)
at org.overturetool.umltrans.Main.Translator.TransLateTexVdmToUml(Translator.java:56)
at org.overture.ide.plugins.umltrans.actions.Vdm2UmlAction$1.run(Vdm2UmlAction.java:113)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

I think I'll read the manual next :-)

Another type error (twice)

The following bug was originally reported on Sourceforge by pglvdm, 2009-05-26 16:20:48:

Errors are reported for two classes in the test dir. I believe that bboth of these are type correct.

Coloring of text

The following bug was originally reported on Sourceforge by lausdahl, 2009-07-28 14:32:24:

If this line below is inseret all text efter the line changes to blue

-- headerBegin : String = "

I guess that its because of the missing quote ". But its commented so it should not change the coloring of the rest of the file

VDMJ allows operations to directly call constructors

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-30 13:38:49:

An operation in a class can call any constructor of that class as though it was a normal operation, returning a new instance of the class - ie. a call to "C(x)" is the same as "return new C(x)". Constructors ought to be inaccessible to operations, other than via the "new" expression.

Debug with VDM-RT thread view updating too fast

The following bug was originally reported on Sourceforge by lausdahl, 2009-11-08 12:27:45:

If a VDM-RT is being debugged it is next to impossible to select a specific thread in the thread view if the model contains a lot of periodic/ async threads. Discovered in HomeAutomation test example

Post condition fail not trapping into debugger

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:16:46:

Execute a small test with a post condition failure in the operation being called (ie. at the very end of the execution). Does not trap into the debugger, even when running with the debug button. Prints (red) "Main 998: an internal error in the debugger occurred" followed by the (correct) text of the postcondition failure.

Adding a breakpoint on the postcondition does correctly trap into debug.

Invalid version data in "About"-info

The following bug was originally reported on Sourceforge by volkersf, 2010-04-20 07:58:38:

With the current download of the OvertureIDE for Mac, when I select "About Overture Tools" from the menu, it shows

Overture Platform
Version: @Version@

Looks like the plugin data/properties haven't been substituted.

CT for flat SL spec

The following bug was originally reported on Sourceforge by pglvdm, 2010-12-19 10:03:53:

If you try to run CT on the Dwarf example you get:
org.overturetool.vdmj.typechecker.ModuleEnvironment cannot be cast to org.overturetool.vdmj.typechecker.FlatEnvironment

NPE when opening file outside the workspace (see 2900466)

The following bug was originally reported on Sourceforge by volkersf, 2010-04-20 07:56:03:

Looks like bug #2900466 is still valid, but it has been closed for comments/feedback.
With the latest download of the Overture IDE for Mac I still get
java.lang.NullPointerException
at org.overture.ide.parsers.vdmj.internal.VdmjSourceParser.parse(VdmjSourceParser.java:57)
at org.eclipse.dltk.core.SourceParserUtil.getModuleDeclaration(SourceParserUtil.java:120)
when using File->Open.

Names of traces cannot be used in the GUI debugger

The following bug was originally reported on Sourceforge by pglvdm, 2010-12-22 11:48:13:

When you have a named trace it can be executed in VDMJ stand-alone. However, it cannot be executed in the GUI debugger from the IDE like this. For example for the VDM-SL version of the CashDispenser example it would be nice to be able to run TestCash (as in the README file).

VDMJ POG misses mutual recursion

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:49:09:

VDMJ's PO generator does not correctly identify mutually recursive functions, and so does not generate the associated POs (simply recursive functions are fine).

Type checker is too tough

The following bug was originally reported on Sourceforge by pglvdm, 2009-05-24 09:19:19:

Functions are to be considered statis so they can be used in the definition of type invariants for example. The attached example should NOT yield any type errors.

Running a spec with a breakpoint breaks

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:33:40:

If you run a specification with the "Run" button, as opposed to debug, then it still breaks at breakpoints. Usually, the Run button has the effect of disabling all the breakpoints before you start.

VDMJ always calls default constructors

The following bug was originally reported on Sourceforge by nick_battle, 2009-05-13 09:10:32:

VDMJ always calls default superclass constructors if they exist. If you explicitly call a superclass constructor, this is called in addition to (and after) the default. VDMTools is the same, though we are both probably wrong.

The test attached produces the following:

p new B()
default
integer
= B{#10, A{#7}}
Executed in 0.0 secs.

p new B()
default
integer
objref4(B):
< >

Clone as VDM-RT in RT project

The following bug was originally reported on Sourceforge by pglvdm, 2010-12-18 13:37:35:

This feature should not be enabled for VDM-RT projects since it does not really make sense.

Run time error when mapping from VDM++ to UML

The following bug was originally reported on Sourceforge by pglvdm, 2009-10-24 09:37:02:

When one takes the attached specification in VDM++ and request it to be moved to UML a run-time error appear. The details of the error says:
Translation error in specification
Run-Time Error:Precondition failure in getSpecifications

APS throws an exception when invoked with multiple VDM files

The following bug was originally reported on Sourceforge by miguel_ferreira, 2009-10-13 19:29:10:

If the APS is invoked with multiple VDM models from the command line an exception gets thrown.
The error message suggests that some necessary file wasn't supplied to the POG tool, since it reports on missing data types that are defined in the VDM file supplied last.

Invocation
gentux@blackie bin $ ./run_aps -t -vppde ~/root/opt/vdmpp/bin/vppde ~/Downloads/client.vpp ~/Downloads/association.vpp ~/Downloads/alert.vpp ~/Downloads/data.vpp

Stack trace:
org.overturetool.proofsupport.AutomaicProofSystemException: [PO-GEN] /Users/gentux/Downloads/client.vpp, l. 21, c. 15: Error[34] : Unknown identifier "Data"/Users/gentux/Downloads/client.vpp, l. 21, c. 15: Error[368] : Access violation for "Data"/Users/gentux/Downloads/client.vpp, l. 159, c. 17: Error[6] : Type name "Data" is not definedErrors: 3
at org.overturetool.proofsupport.AutomaticProofSystem.wrapException(AutomaticProofSystem.java:109)
at org.overturetool.proofsupport.AutomaticProofSystem.wrapException(AutomaticProofSystem.java:104)
at org.overturetool.proofsupport.AutomaticProofSystem.doPreparation(AutomaticProofSystem.java:73)
at org.overturetool.proofsupport.AutomaticProofSystemBatch.translateModelAndPos(AutomaticProofSystemBatch.java:28)
at org.overturetool.proofsupport.ApsMain.run(ApsMain.java:57)
at org.overturetool.proofsupport.ApsMain.main(ApsMain.java:44)
Caused by: org.overturetool.proofsupport.external_tools.pog.PoGeneratorException: /Users/gentux/Downloads/client.vpp, l. 21, c. 15: Error[34] : Unknown identifier "Data"/Users/gentux/Downloads/client.vpp, l. 21, c. 15: Error[368] : Access violation for "Data"/Users/gentux/Downloads/client.vpp, l. 159, c. 17: Error[6] : Type name "Data" is not definedErrors: 3
at org.overturetool.proofsupport.external_tools.pog.VdmToolsWrapper.analyzeErrorMessage(VdmToolsWrapper.java:52)
at org.overturetool.proofsupport.external_tools.pog.VdmToolsWrapper.validateOperation(VdmToolsWrapper.java:42)
at org.overturetool.proofsupport.external_tools.pog.VdmToolsWrapper.runPogGenerator(VdmToolsWrapper.java:31)
at org.overturetool.proofsupport.external_tools.pog.VdmToolsWrapper.generatePogFile(VdmToolsWrapper.java:21)
at org.overturetool.proofsupport.TranslationPreProcessor.generatePogFile(TranslationPreProcessor.java:79)
at org.overturetool.proofsupport.TranslationPreProcessor.prepareVdmFiles(TranslationPreProcessor.java:31)
at org.overturetool.proofsupport.AutomaticProofSystem.doPreparation(AutomaticProofSystem.java:71)
... 3 more

VDMJ permits subclasses to call private constructors

The following bug was originally reported on Sourceforge by nick_battle, 2009-07-03 11:03:26:

If a class declares a private constructor, it should only be callable from within the class (singletons). But VDMJ permits subclasses to implicitly invoke such constructors, as though they were protected. The problem is that access is checked during type-checking (not runtime), and the TC doesn't check this properly when it's calculating the inherited members of the subclass. It's complicated by the presence of an implicit (public) default constructor in all classes, and we also have to resolve what happens when the subclass makes an explicit superclass constructor call (ie. if it calls an explicit super constructor, does that mean the private default one is not called?)

Internal DLTK error

The following bug was originally reported on Sourceforge by volkersf, 2009-11-19 14:20:46:

In a VDMPP-project, I have imported the POP3 files. Select pop3test.vdmpp, right click for Debugs As -> Launch VDMJ VDM++ (pgl later showed me the correct way of running a test):

org.eclipse.dltk.dbgp.exceptions.DbgpDebuggingEngineException: Execution error 206: Expecting class name after 'new'
at org.eclipse.dltk.dbgp.internal.utils.DbgpXmlParser.checkError(DbgpXmlParser.java:122)
at org.eclipse.dltk.dbgp.internal.commands.DbgpDebuggingEngineCommunicator.communicate(DbgpDebuggingEngineCommunicator.java:93)
at org.eclipse.dltk.dbgp.DbgpBaseCommands.communicate(DbgpBaseCommands.java:43)
at org.eclipse.dltk.dbgp.internal.commands.DbgpContinuationCommands.execCommand(DbgpContinuationCommands.java:35)
at org.eclipse.dltk.dbgp.internal.commands.DbgpContinuationCommands.run(DbgpContinuationCommands.java:43)
at org.eclipse.dltk.dbgp.internal.commands.DbgpCoreCommands.run(DbgpCoreCommands.java:137)
at org.eclipse.dltk.internal.debug.core.model.operations.DbgpResumeOperation.process(DbgpResumeOperation.java:23)
at org.eclipse.dltk.internal.debug.core.model.operations.DbgpOperation$1.run(DbgpOperation.java:64)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

Different keywords in different dialects

The following bug was originally reported on Sourceforge by pglvdm, 2009-07-21 07:17:18:

If you for example make a VDM-SL project keywords specific to VDM-SL such as "state" are NOT being highlighted.

"DEADLOCK detec" showing in CT

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:46:17:

When a CT test detects a deadlock, the result text is showing as "DEADLOCK detec" (ie. truncated). Low priority :-)

Type checker reports wrong error

The following bug was originally reported on Sourceforge by pglvdm, 2009-05-24 11:03:56:

Two type errors are reported wrongly for the attached VDM++ model

Overture IDE for Windows does not create Overture projects

The following bug was originally reported on Sourceforge by npak, 2009-10-14 09:59:43:

1. Downloaded OvertureIde-1.0.0-win32.zip and unpacked it to d:\software\overture
2. Launched overture.exe, when it asked about the workspace entered D:\work\vdm\overture\OvertureDemoPpWorkspace (the demo workspace)
3. The Overture IDE opened the main window. No projects, no files, as expected. Thats fine for now.
4. Right-click in the Project Explorer, then New->Project, in the dialog selected "Overture Tool wizards -> Overture Project". An error message appears:
   The selected wizard could not be started.
   Plug-in org.overturetool.eclipse.plugins.editor.ui was unable to load class org.overturetool.eclipse.plugins.editor.internal.ui.wizards.OvertureProjectCreationWizard.
   org.overturetool.eclipse.plugins.editor.internal.ui.wizards.OvertureProjectCreationWizard

The problem is that Overture IDE ships org.overturetool.eclipse.plugins.editor.ui_1.0.0.jar that is only 99 kB. This JAR file misses package org.overturetool.eclipse.plugins.editor.internal.ui completely. There are no files in this package at all.

To resolve the problem I replaced org.overturetool.eclipse.plugins.editor.ui_1.0.0.jar in the IDE plugins/ directory with the jar from the Eclipse plugin installed from the update site. Please note the difference - it is 229 kB size. After the replacment the Overture wizards in the IDE started working.

CT for Pop3 does not work

The following bug was originally reported on Sourceforge by pglvdm, 2010-12-19 10:09:50:

If you try using CT for the POP3 example you get: Error 4034: Name 'MakeMessages(UserName)' not in scope in 'POP3Test' (C:\overturesvn\documentation\examples\VDM++\POP3\pop3test.vdmpp) at line 52:40

VDMJ reports params unused in pre/post

The following bug was originally reported on Sourceforge by nick_battle, 2009-11-07 21:29:02:

VDMJ reports that parameters are unused if they only occur in pre or postcondition expressions.

VDMJ dynamic type check problem

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:08:35:

There is an error in VDMJ's dynamic type checking, such that it cannot distinguish maps and sequences during assignments if the target type is a union of a map and a sequence. For example, the following:

op: () ==> int
op() ==
(
    dcl m:map int to bool | seq of int := {1 |-> true };
    m(2) := 123;
    return m(2);
)

This returns 123, even though internally that means the map has the value {1 |-> true, 2 |-> 123}, which is clearly an illegal value and should fail a dynamic type check at the point of the assignment. The static type check of this is OK as the type could be a seq of int, but at runtime it is actually a map int to bool.

Creating new VDM++ class does not know current project

The following bug was originally reported on Sourceforge by pglvdm, 2010-01-12 07:58:40:

When one is right-clicking inside a project and ask for a new class one would expect that the name of the project was already filled in, but unfortunately this does not happen.

NullPointerException when creating launch

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:27:50:

Create a new PP project, import the file attached, create a launch (for Run, not debug), select the project, select the "Runtime" operation. Dialog says, "Intrnal type check error: java.lang.NullPointerException" (note misspelling). Cannot seem to get out of it.

Combinatorial testing forget to type check

The following bug was originally reported on Sourceforge by pglvdm, 2009-10-24 05:46:34:

If one includes the attached files (also checked in as documentation/examples/VDM++/Alarm++traces) in a VDM++ project and one change to the CT perspective and run the selected trace it works but in the Console window one first gets "Error 4087: Cannot convert mk_token("Monday day") (mk_token("Monday day")) to (unresolved Plant`Period) in 'Test2' (C:\TEMP\projects\Alarm++\test1.vdmpp) at line 18:1" and according to Nick this kind of error comes if one have not run the type checked before invoking the CT interpreter. Thus there is a need to keep track of whether a model is type checked or not and make use of this info in the CT exclipse plug-in.

CT "run" button runs tests, but doesn't update tree

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:44:20:

If you use the green ">" run button on the top line of the CT view, it runs the tests and you can see the results on the Console and under the generated folder, but the display does not update with the results. To get the results, you have to right-click the class name and select "Full Evaluation" (or the other one).

CCE in Debug Configurations

The following bug was originally reported on Sourceforge by volkersf, 2009-11-19 14:22:58:

In a test project, I have imported the POP3 files. Right-click on pop3test.vdmpp, select "Debug Configurations".
"Browse" for the Class entry field, double click on POP3Test:

java.lang.ClassCastException: org.eclipse.dltk.internal.core.SourceType cannot be cast to org.eclipse.dltk.internal.core.SourceMethod
at org.overture.ide.vdmpp.debug.ui.tabs.VdmppMainLaunchConfigurationTab.chooseOperation(VdmppMainLaunchConfigurationTab.java:223)
at org.overture.ide.vdmpp.debug.ui.tabs.VdmppMainLaunchConfigurationTab.handleOperationButtonSelected(VdmppMainLaunchConfigurationTab.java:198)
at org.overture.ide.vdmpp.debug.ui.tabs.VdmppMainLaunchConfigurationTab$1.widgetSelected(VdmppMainLaunchConfigurationTab.java:162)
at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:228)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:3543)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1250)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1273)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1258)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1079)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3441)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3100)
at org.eclipse.jface.window.Window.runEventLoop(Window.java:825)
at org.eclipse.jface.window.Window.open(Window.java:801)
at org.eclipse.debug.internal.ui.launchConfigurations.LaunchConfigurationsDialog.open(LaunchConfigurationsDialog.java:1064)
at org.eclipse.debug.ui.DebugUITools$1.run(DebugUITools.java:398)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.debug.ui.DebugUITools.openLaunchConfigurationDialogOnGroup(DebugUITools.java:406)
at org.eclipse.debug.ui.DebugUITools.openLaunchConfigurationDialogOnGroup(DebugUITools.java:340)
at org.eclipse.debug.ui.actions.OpenLaunchDialogAction.run(OpenLaunchDialogAction.java:81)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:411)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:3543)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1250)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1273)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1258)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1079)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3441)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3100)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
at org.eclipse.equinox.launcher.Main.run(Main.java:1311)

Breakpoints in VDM-SL not wokring

The following bug was originally reported on Sourceforge by lausdahl, 2009-11-08 12:25:39:

It is not possible to set a breakpoint in the IDE when debugging a VDM-SL project. //found by PGL

Class Outline shows unresolved parameter types

The following bug was originally reported on Sourceforge by nick_battle, 2009-07-28 17:22:42:

The Outline view shows unresolved types for parameters that are not basic types. For example, the IO library shows "fwriteval(seq1 of char, @p, (unresolved filedirective))". This is because the signature is being requested before the specification has been type checked (so it does not know what filedirective is yet).

You can solve it by type checking first, but there may be errors. Perhaps it would be better to string-substitute "(unresolved %s)" for "%s" before display?

VDMJ scope hiding warnings incorrect

The following bug was originally reported on Sourceforge by nick_battle, 2009-11-07 21:26:01:

VDMJ gives warnings for names of state components being overwritten when the same name is used in parameter lists of functions. In these the state components should not be visible anyway and thus these warnings should really not be produced.

Can't select inherited operations for launch

The following bug was originally reported on Sourceforge by shinsahara, 2011-01-01 12:22:01:

In "Debug Configurations" window, I can't select overloaded operation/function.

I want to select run() operation in abstract class" TestDriver" class from ＵｎｉｑｕｅＮｕｍｂｅｒＴ class.
But, in "Class and operation/function selection" window, there is no run() in ＵｎｉｑｕｅＮｕｍｂｅｒＴ.

Unable to create an Overture project

The following bug was originally reported on Sourceforge by npak, 2009-09-15 03:11:41:

Eclipse 2.4.2
eclipse.buildId=I20090611-1540
java.version=1.6.0_14
java.vendor=Sun Microsystems Inc.
BootLoader constants: OS=win32, ARCH=x86, WS=win32, NL=ru_RU
Framework arguments: -product org.eclipse.epp.package.java.product
Command-line arguments: -os win32 -ws win32 -arch x86 -product org.eclipse.epp.package.java.product

All updates from Eclipse update sites are installed. The most recent Overture tool is installed.

When trying to create an Overture project an error message appears "Index out of bounds".

The error log is:
Problems occurred when invoking code from plug-in: "org.eclipse.jface".
java.lang.IllegalArgumentException: Index out of bounds
at org.eclipse.swt.SWT.error(SWT.java:3865)
at org.eclipse.swt.SWT.error(SWT.java:3799)
at org.eclipse.swt.SWT.error(SWT.java:3770)
at org.eclipse.swt.widgets.Widget.error(Widget.java:463)
at org.eclipse.swt.widgets.Combo.getItem(Combo.java:646)
at org.overturetool.eclipse.plugins.editor.internal.ui.wizards.OvertureProjectWizardFirstPage.createCustomGroups(OvertureProjectWizardFirstPage.java:160)
at org.eclipse.dltk.ui.wizards.ProjectWizardFirstPage.createControl(ProjectWizardFirstPage.java:959)
at org.eclipse.jface.wizard.Wizard.createPageControls(Wizard.java:170)
at org.overturetool.eclipse.plugins.editor.internal.ui.wizards.OvertureProjectCreationWizard.createPageControls(OvertureProjectCreationWizard.java:166)
at org.eclipse.jface.wizard.WizardDialog.createPageControls(WizardDialog.java:675)
at org.eclipse.jface.wizard.WizardDialog.setWizard(WizardDialog.java:1093)
at org.eclipse.jface.wizard.WizardDialog.updateForPage(WizardDialog.java:1152)
at org.eclipse.jface.wizard.WizardDialog.access$2(WizardDialog.java:1149)
at org.eclipse.jface.wizard.WizardDialog$5.run(WizardDialog.java:1138)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.jface.wizard.WizardDialog.showPage(WizardDialog.java:1136)
at org.eclipse.ui.internal.dialogs.NewWizardSelectionPage.advanceToNextPageOrFinish(NewWizardSelectionPage.java:71)
at org.eclipse.ui.internal.dialogs.NewWizardNewPage$1.doubleClick(NewWizardNewPage.java:355)
at org.eclipse.jface.viewers.StructuredViewer$1.run(StructuredViewer.java:821)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.runtime.Platform.run(Platform.java:888)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:48)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:175)
at org.eclipse.jface.viewers.StructuredViewer.fireDoubleClick(StructuredViewer.java:819)
at org.eclipse.jface.viewers.AbstractTreeViewer.handleDoubleSelect(AbstractTreeViewer.java:1419)
at org.eclipse.jface.viewers.StructuredViewer$4.widgetDefaultSelected(StructuredViewer.java:1195)
at org.eclipse.jface.util.OpenStrategy.fireDefaultSelectionEvent(OpenStrategy.java:238)
at org.eclipse.jface.util.OpenStrategy.access$0(OpenStrategy.java:235)
at org.eclipse.jface.util.OpenStrategy$1.handleEvent(OpenStrategy.java:296)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1003)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3880)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3473)
at org.eclipse.jface.window.Window.runEventLoop(Window.java:825)
at org.eclipse.jface.window.Window.open(Window.java:801)
at org.eclipse.ui.actions.NewProjectAction.run(NewProjectAction.java:117)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:411)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1003)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3880)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3473)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2405)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2369)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2221)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:500)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:493)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:194)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:368)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:559)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:514)
at org.eclipse.equinox.launcher.Main.run(Main.java:1311)

tool doesn't remember where interpreter is

The following bug was originally reported on Sourceforge by shinsahara, 2010-04-12 03:28:43:

The overture tool doesn't remember where interpreter is in Interpreter tag in Debug Configuration View.

NPE when opening closed project

The following bug was originally reported on Sourceforge by volkersf, 2010-04-20 08:12:08:

In the current Mac-build, create an empty VDM-PP project. Select "Close Project", and open it again:

java.lang.NullPointerException
at org.eclipse.dltk.internal.core.BuildpathValidation.validate(BuildpathValidation.java:68)
at org.eclipse.dltk.internal.core.DeltaProcessor.resourceChanged(DeltaProcessor.java:2019)
at org.eclipse.dltk.internal.core.DeltaProcessingState.resourceChanged(DeltaProcessingState.java:561)
at org.eclipse.core.internal.events.NotificationManager$2.run(NotificationManager.java:291)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.NotificationManager.notify(NotificationManager.java:285)
at org.eclipse.core.internal.events.NotificationManager.broadcastChanges(NotificationManager.java:149)
at org.eclipse.core.internal.resources.Workspace.broadcastBuildEvent(Workspace.java:297)
at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:136)
at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:238)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

Missing names in variables view

The following bug was originally reported on Sourceforge by pglvdm, 2010-12-19 09:59:11:

If you take the simple Alarm example in VDM++ and set a breakpoint in line 29 of the test1.vdmpp file and then try to subsequently debug new Test1().Run() it will correctly stop at the breakpoint. However, in the variables view the last part of the let (expert) is NOT shown in here. It is the same with other examples. The last one in a let with multiple definitions are not included.

NullPointerException in POG

The following bug was originally reported on Sourceforge by nick_battle, 2010-12-17 16:12:37:

I created a new SL project, imported an SL file (attached), and opened it in the editor, which correctly showed one warning (so TC ok). Then asked for POs. Resulted in an internal error, "Parse=true, TC=true, java.lang.NullPointerException".

Parser error not in problem view.

The following bug was originally reported on Sourceforge by thillemann, 2009-11-03 16:42:27:

The editor displays syntax errors and warnings dynamically (as you type), and adds TC errors when you save, also adding these TC errors to the Problems view. But if you save a spec that only has syntax errors, those errors do not appear in the Problems view.

The parser errors should be updated as well.

Latex coverage doesn't finish

The following bug was originally reported on Sourceforge by shinsahara, 2010-04-12 03:57:54:

if VDM sources includes UTF-8 chracters then
Latex coverage doesn't finish and generated PDF doesn't know UTF-8 character or font.

Breakpoints in threads are ignored

The following bug was originally reported on Sourceforge by pglvdm, 2010-04-02 12:13:23:

If one sets breakpoints inside a thread (rather than an operation that is started from a thread it is not respected so execution just continues.

debugger with run-time does not update editor window

The following bug was originally reported on Sourceforge by pglvdm, 2009-06-10 10:01:18:

If one starts the IDE debugger on something that yields a run time error it is reported as an error in the console but unfortunately the editor window is NOT updated to show the place where the error occured.

VDMJ function variable scoping error

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:11:17:

There is a bug regarding access to named function variables when the environment
also contains a function definition of the same name. Calls involving the variable
will actually be bound to the definition, even though the variable is in scope.

For example:

f(a:int) r:int == a + 1;
g(f:int->int) r:int == f(123);  -- This will call the f above, not the f arg.

You get a warning because the function parameter is not used:

Warning 5000: Definition 'f' not used in 'A' ... at line ...

A workaround is to rename the parameter.

UTF-VDM RT Realtime Log can't display UTF-8 Chars

The following bug was originally reported on Sourceforge by shinsahara, 2010-04-12 08:04:27:

UTF-VDM RT Realtime Log can't display UTF-8 Characters.

Coverage output is not for International character

The following bug was originally reported on Sourceforge by shinsahara, 2011-01-01 12:28:35:

For example, UniqueNumber.vdmppcov is like following...

class ?�?�ｉｑｕ�?��?�ｍｂ�?�?is subclass of CommonDefinition

values
?�??�?�?��ｌｔＶ??��ｕ�?= 1;

instance variables
protected UniqNum : int := ?�??�?�?��ｌｔＶ??��ｕ�? -- UniqNum of next issued

Type checker: missing exit checks

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:31:09:

The type checking of statements which handle exceptions (eg. trap) looks for whether the body of the specification covered can in fact throw exceptions, raising an error if not. This search process is limited in VDMJ. In particular, it cannot cross an operation call, assuming that all operations can raise exceptions. This leads to false negatives - not reporting a TC error, when it should.