Softpedia >Windows >Programming >Other Programming Files >Overture Tool >  Changelog

Overture Tool Changelog

What's new in Overture Tool 3.0.2

Nov 11, 2020
  • What's New:
  • Overture is now based on Eclipse 2020-09. In this version we include a strict type-checking option flag, sort several language level bugs, and solve problems with the console of external tools.
  • Bugfixes:
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/45
  • 763 closed - Running external tools opens a double console
  • 737 closed - Launch configuration Interpreter tab's checkboxes are negated before calling the interpreter
  • 736 closed - Expressions in let def and let be st statements should not allow operation calls
  • 728 closed - Set comprehensions don't propagate type constraints

New in Overture Tool 3.0.0 (Aug 29, 2020)

  • Bugfixes:
  • Please note that the interactive list is at https://githubcom/overturetool/overture/milestone/44
  • closed - Maps of Record types sometimes fail
  • closed - 17 tests failing
  • closed - Runtime predicate errors in forall/exists/iota/comprehensions mislocated
  • closed - Inconsistency between equality relation and set membership
  • closed - Type checker defines RESULT symbol for post condition of void operations
  • closed - Type checker allows a zero literal index for sequences
  • closed - "Illegal clone" "Main 206: Error evaluating code" error
  • closed - Map operation fails with "Error 4089: Can't get real value of map"
  • closed - Overture missing an order/equality warning
  • closed - Incorrect module scope for min/max function variables
  • closed - Incorrect Debug Exception Highlighting with Multiple Files of the Same Name
  • closed - Incorrect recursive function warnings, with cycles
  • closed - Incorrect recursive cycles given for pre/postconditions
  • closed - Equality test fails if a nil value is used
  • closed - Socket is closed by Overture before VDMJ finishes printing coverage
  • closed - Dialect preference shows vdm10 and errors are issued as it was checked against the classic dialect
  • closed - download error

New in Overture Tool 2.7.4 (Mar 17, 2020)

  • Bug fixes:
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/43
  • 687 closed - Java Exception when running debug on AlarmSL sample project.
  • 682 closed - Precedence inconsistency between code and documentation
  • 651 closed - PO for Cash Dispenser example in VDM-SL contains "null"
  • 632 closed - Make Overture and Language Syntax Consistent
  • 615 closed - Isagen tasks
  • 529 closed - Add facility to only check a condition if a type binding is finite
  • 444 closed - Interpreter: Internal errors are reported as "internal error" but could have displayed the real problem description
  • 249 closed - Fix copyright headers
  • 15 closed - VDMJ POG misses mutual recursion
  • 14 closed - Type checker: missing exit checks

New in Overture Tool 2.7.2 (Oct 1, 2019)

  • What's New:
  • This release contains some type checker and annotations fixes, but also introduces the new @OnFail annotation, which is useful for debugging contract violations. The @OnFail annotation is described in the Model Annotations chapter in the Overture User Guide.

New in Overture Tool 2.7.0 (Jun 7, 2019)

  • Support for VDM annotations (currently limited to the Overture
  • command-line interface)
  • Improved type checking of struct import/export (VDM-SL only)
  • Improved Java code-generation
  • Limited support for polymorphic types
  • Support for renamed constructs (VDM-SL only)
  • Several bug fixes.

New in Overture Tool 2.6.4 (Oct 30, 2018)

  • What's New:
  • This release contains some type-checker fixes and improvements for the user interface.
  • Note that Overture requires Java 8. If you're using more recent versions of Java (e.g. version 10) you may experience errors when you launch Overture. In particular, Overture, currently builds against Eclipse Oxygen, which is known to have issues related to recent versions of Java. In case you experience issues try to follow the suggestions in the FAQ (see "Q: Why can’t I open Overture using the latest versions of Java?").
  • Bugfixes:
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/40
  • closed - An example in Language manual, a strange type error occurred.
  • closed - VDMTools is not CSK or SCSK product now, but I found CSK and SCSK in message and menu.
  • closed - VDMTools died when international character is in "Path to VDM Tools" in SCSK/VDM Tools

New in Overture Tool 2.6.2 (May 21, 2018)

  • Bugfixes:
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/38
  • 665 closed - The Class/function selection in launch configurations is not sorted making it difficult to find a class
  • 681 closed - Type of record pattern not resolved
  • 676 closed - The Java bridge can't always resolve imported VDM-SL types
  • 672 closed - Support Java code-generation of setUp and tearDown
  • 679 closed - Support Java code-generation of VDMUtil`set2seq
  • 678 closed - Function values with polymorphic type parameters are not correctly instantiated
  • 673 closed - Add "-version" argument to the Overture command-line interface
  • 669 closed - let expression interprets tail of a seq1 as a seq1
  • 666 closed - Is not yet specified does not work with overloads

New in Overture Tool 2.6.0 (Feb 16, 2018)

  • Overture 2.6.0 displays error-occurred dialog
  • Type-checker allows modules to directly access state of other modules
  • Sequence Enumeration
  • Overture Codegen does not re-generate as expected
  • Type checker fails to identify invalid type

New in Overture Tool 2.5.4 (Nov 10, 2017)

  • Bugfixes:
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/36
  • Java code-generator does not handle the nondeterministic statement correctly
  • operator type errors have wrong location information
  • Extend Java code-generation support for maps
  • Interpreter fails to find object member
  • File AlarmInitUML.uml
  • Add support for code-generation of the iota expression
  • Mu expressions can miss type checking errors
  • Generating PDF with the modelOnly preference does not drop non-model text
  • When pretty printing with the option where model only is switched off one shall not generate section{ClassName}

New in Overture Tool 2.5.2 (Sep 11, 2017)

  • Performance improvements for the code coverage feature
  • Fixes for the debugger, and
  • Increased coverage of constructs that can be code-generated to Java

New in Overture Tool 2.5.0 (Aug 10, 2017)

  • In addition to the usual bug fixes, this release contains a new "equality and order relations" feature [RM39]. Details about this feature can be found in the Language Reference Manual [VDM-10 Language Manual, Section 3.4 and Section 3.5].

New in Overture Tool 2.4.8 (Aug 8, 2017)

  • This release contains a number of bug fixes covering the parser, type checker, quick interpreter and combinatorial testing. See the Bugfixes section for additional details.
  • In addition, a change has been made to Overture (see issue 613) that may give a noticeable interpreter performance improvement in specifications that internally throw several exceptions. This occurs naturally in specs with complex union types or which perform a lot of complex pattern matching. In specifications with traces a 20% performance improvement has been seen
  • Please note that the interactive list is at https://github.com/overturetool/overture/milestone/32:
  • 622 closed - Single trace test is executed using default JVM options
  • 620 closed - AccountSys VDM Class
  • 617 closed - Quick Interpreter should check for rubbish after expressions
  • 616 closed - discrepancy between VDMJ and Overture outputs
  • 613 closed - Core modules use different versions of AstCreator
  • 610 closed - Parser allows multiple consecutive access modifiers for functional descriptions
  • 609 closed - Remove abbreviated release notes
  • 603 closed - The welcome page does not work after self-update
  • 594 closed - Type checking of dlmodules should be relaxed

New in Overture Tool 2.4.6 (Mar 22, 2017)

  • Released on 03 March 2017
  • New features:
  • This release contains a number of bug fixes covering the parser, type checker, quick interpreter and combinatorial testing. See the Bugfixes section for additional details.
  • In addition, a change has been made to Overture (see issue 613) that may give a noticeable interpreter performance improvement in specifications that internally throw several exceptions. This occurs naturally in specs with complex union types or which perform a lot of complex pattern matching. In specifications with traces a 20% performance improvement has been seen.
  • Bug fixes:
  • #622 closed - Single trace test is executed using default JVM options
  • #620 closed - AccountSys VDM Class
  • #617 closed - Quick Interpreter should check for rubbish after expressions
  • #616 closed - discrepancy between VDMJ and Overture outputs
  • #613 closed - Core modules use different versions of AstCreator
  • #610 closed - Parser allows multiple consecutive access modifiers for functional descriptions
  • #609 closed - Remove abbreviated release notes
  • #603 closed - The welcome page does not work after self-update
  • #594 closed - Type checking of dlmodules should be relaxed

New in Overture Tool 2.4.4 (Mar 22, 2017)

  • Released on 02 December 2016
  • This release contains some improvements to the Java code generator, and some fixes to the VDMUtil standard library.
  • Bug fixes:
  • #607 closed - Easy access to the language manual
  • #606 closed - Add limited Java code generation support for multiple inheritance
  • #605 closed - Tempo example does not run on Windows
  • #602 closed - Copyright notice needs to be updated
  • #586 closed - VDMUtil`seq_of_char2val cannot parse record type
  • #571 closed - Enable Tempo plotting library feature

New in Overture Tool 2.4.2 (Mar 22, 2017)

  • Released on 06 October 2016
  • This release contains a prototype version of an auto-completion feature for VDM. It has been developed by Peter Mathiesen and Magnus Louvmand Pedersen in connection with an R&D project. The auto-completion feature is able to list proposals for function and operation invocations, constructors and built-in types.
  • There's a few things worth mentioning about the current version of the auto-completion feature: First, this feature only works when the model is type correct, so if you introduce parse/type errors and save the model sources, no proposals will be listed. The parser/type checker is currently not able to cope with partially correct ASTs, and the auto-completion feature does not yet cache the most recent type correct AST and use that to compute proposals. Second, auto-completion in blank spaces tries to propose "everything" -- even built-in types such as 'nat' and 'bool', and templates for functions and operations. Third, proposals on the form x.op() are not yet supported. It's only possible to list proposals for functions and operations defined in the enclosing class.
  • In addition, a new feature, called the "Overture Graphics Plugin" is now available via one of the pre-installed update sites. This plugin allows you to visualise a VDM model's instance variables over time using, for example, 2D plots. More information about how to use this plugin can be found in the Overture tool's user manual.
  • Finally, a new VDM++ model of a traffic management system has been added to the standard examples. This example is GUI-based and uses the "Overture Graphics Plugin" to visualise the model's instance variables. The model has been developed in the TEMPO (TMS Experiment with Mobility in the Physical World using Overture) project, where technologies that can reduce traffic jams have been researched.
  • Bug fixes:
  • #599 closed - Problem with function value conversion
  • #589 closed - Overture key bindings are in conflict
  • #423 closed - "Improve" auto-completion

New in Overture Tool 2.4.0 (Mar 22, 2017)

  • Released on 30 August 2016
  • Overture has been updated to include two new language features. The first language feature, which is based on Request for Modification (RM) 35, adds a set1 type constructor to the language. Second, VDM-10 now supports sequence bindings (RM 36), which allows iterating over sequences in a more concise way. For example, one can now write [ f(x) | x in seq s & P(x) ] rather than [ f(s(i)) | i in set inds s & P(s(i)) ].
  • In the previous release, Overture was upgraded to support self-update using Eclipse p2. It should therefore be possible to update Overture 2.3.8 to version 2.4.0 (this version) using p2. Make sure that the Eclipse release site is available: http://download.eclipse.org/releases/neon
  • Updating Overture to a newer version is similar to updating any other Eclipse application. From the menu choose Help -> Install New Software... Next, from the list of repositories select 'Overture Development', make sure you have 'Overture' selected, and execute the update. Finally, Overture has been updated to build against the newest version of Eclipse (Neon).
  • Bug fixes:
  • #588 closed - Overture won't open after update
  • #587 closed - VDM-RT log viewer check box is not reflecting the actual settings
  • #585 closed - VDM-RT Diagram Export crops figures
  • #584 closed - Type checker crashes when trying to call invalid CPU constructor
  • #583 closed - Upgrade Overture to build against Eclipse Neon
  • #582 closed - VDMUtil`seq_of_char2val should handle nonsense conversions gracefully
  • #579 closed - print some VDM value are strange
  • #578 closed - Output informations of "CT Test Case result" View is not enough
  • #577 closed - Repository split - disabled artifacts
  • #574 closed - Hexadecimal Values
  • #570 closed - Unexpected failure of run configuration
  • #521 closed - Inconsistent import behaviour

New in Overture Tool 2.3.8 (Mar 22, 2017)

  • Released on 04 July 2016
  • This release includes various bug fixes (see below). In addition, Overture has been upgraded to support self-update using Eclipse p2. In essence this means that once a new version of Overture has been released, it is possible to update the tool using p2.
  • Updating Overture to a newer version is similar to updating any other Eclipse application. From the menu choose Help -> Install New Software... Next, from the list of repositories select 'Overture Development' and make sure you have 'Overture' selected. Finally, you must execute the update.
  • Bug fixes:
  • #572 closed - Null pointer exception with malformed pattern binds
  • #567 closed - Type check of break point conditions is missing
  • #566 closed - could not find or load main class org.overture.interpreter.debug.DBG Reader V2
  • #565 closed - Inconsistency when type specified in export list
  • #564 closed - Suggestion: Bundle Version Control tools with Overture
  • #563 closed - Functions in state variables crash variables view
  • #562 closed - Type checking missing some polymorphic instantiation errors
  • #561 closed - Problem passing polymorphic functions as arguments
  • #559 closed - Toggle Comment Shortcut
  • #558 closed - Minor issue with trace verdicts when test is send to the interpreter
  • #470 closed - Test framework ExamplesTest can not be re-run individually
  • #438 closed - CT Send to Interpreter - breakpoints don't work for records in functions
  • #412 closed - Find hosting solution for Eclipse P2 update site
  • #308 closed - Instantiation of Polymorphic function missed by the type checker

New in Overture Tool 2.3.4 (Mar 22, 2017)

  • Released on 16 March 2016
  • This is a special release upgrading Apache Commons Collections to version 3.2.2 as version 3.2.1 has a serious CVSS 10.0 vulnerability.

New in Overture Tool 2.3.2 (Mar 22, 2017)

  • Released on 2 March 2016
  • This will be the last version of Overture that depend on JRE 7.
  • Changes:
  • Small fix to 'JavaCodeGen' (commit: 6fd1c2a) (detail / githubweb)
  • Only transform statuses that can be code generated (commit: e22328b) (detail / githubweb)
  • Update the Java code generator command-line interface to complain if no (commit: 2f4797a) (detail / githubweb)
  • Add IR construction for the narrow expression (commit: 0106e90) (detail / githubweb)
  • Test Java code generation of the 'narrow' expression (commit: c378699) (detail / githubweb)
  • Address warning caused by duplicate versions for the javadoc plugin (commit: d0c36f2) (detail / githubweb)
  • Remove warnings in the type checker (commit: b254d13) (detail / githubweb)
  • Add default cases in parser in order to remove warnings (commit: ba28369) (detail / githubweb)
  • Cleanup imports in TraceInterpreter (commit: 229bd35) (detail / githubweb)
  • Cleanup 'StaticSentinel' in the Java code generator runtime (commit: e1c3f83) (detail / githubweb)
  • Update documentation submodule pointer (commit: 6bf991a) (detail / githubweb)

New in Overture Tool 2.3.0 (Mar 22, 2017)

  • Released on 7 October 2015
  • New feature:
  • This release adds support for the new VDM pure operations feature - If an operation is declared pure it means that it is executed atomically when it is called from a functional context (from functions, invariants, pre or post-conditions). Otherwise calling a pure operation is no different to calling a normal operation, except that a pure operation has various constraints
  • Bug fixes:
  • #459 Type invariant violation incorrectly reported for the state type
  • #455 POG crash for atomic statements in VDM-SL
  • #453 Wrong template construction for implicit operations and functions
  • #452 Can't launch GUI examples in OpenJDK
  • #451 Make new code generation functionality accessible via the Overture IDE
  • #437 Command line coverage only works with absolute filenames
  • #419 fixme: only used in 1 class. Move it over.

New in Overture Tool 2.2.5 (Mar 22, 2017)

  • Released on 19 June 2015
  • Various bugfixes
  • Better performance of the CT GUI on MacOS
  • Java Code-Generation support for VDM-SL models
  • Support for JML when code-generating VDM-SL models
  • Bug fixes:
  • #450 Update of Eclipse version: The kepler Eclipse version is not longer properly mirrored
  • #449 static constructor that is new’ed
  • #448 Assignment to local constants not rejected by the type checker
  • #447 Launcher remembers entry point, even when using Console
  • #446 The interpreter fails to report a type invariant violation
  • #445 POG crash on postcondition quoting in classes with invariants
  • #443 RESULT is not really reserved
  • #442 "Could not create the view..."
  • #441 Disable Trivial PO Status
  • #440 Record with unnamed fields fails to code generate to Java
  • #439 Potential issue with addition of reals
  • #436 Re-remove vdmjc
  • #430 Overture closes with error when expanding and collapsing traces on a Mac OSX
  • #426 New function for current system time
  • #422 Standardize UI tests
  • #397 Poor message for stack overflow errors

New in Overture Tool 2.2.4 (Mar 22, 2017)

  • Released on Mar 2015
  • Bug fixes:
  • #435 Typecheck problem with forward references
  • #434 Bug tracker link in Welcome page
  • #433 Incorrect type check of "++" operator
  • #432 Subset and psubsets should give TC error if the types do not match
  • #431 Inherited definitions not visible in the launch configuration view
  • #429 JVM version misreported?
  • #428 Isagen and CG extensibility improvements
  • #425 Improvements to the Java code generator based on feedback from the INTO-CPS project
  • #424 The is_expression does not work for function types
  • #421 Improving the usability of the Java code generator plugin
  • #420 POG not implemented for while loops

New in Overture Tool 2.2.2 (Jun 15, 2015)

  • Bug fixes:
  • Problem with code generator update site
  • Problem with patterns in traces
  • Tic-tac-toe CT errors in 2.2.0
  • Problems running Overture with JDK/JRE 8 on Windows
  • Problem running the SmokkingPP examples
  • Scoping for traces does not work correctly

New in Overture Tool 2.2.0 (Jun 15, 2015)

  • Bug fixes:
  • Problem with object binds in traces
  • Internal error in the trace interpreter
  • Problems with filtering of tests in traces
  • Div rem and mod do not detect division by zero
  • scope of inherited constant values
  • Problem with type check of set ranges
  • Problem with access specifiers in traces
  • Problem with pretty printing of POs
  • Build: target JavaSE1.7 instead of 1.6
  • Type information does not seem to be fully taken into account in POG

New in Overture Tool 2.1.6 (Jun 15, 2015)

  • Bug fixes:
  • The Overture welcome page needs updating
  • Unresolved type parameters in pre-conditions
  • Code generation giving bug for the AutomatedStockBrokerPP standard example
  • Scoping problem with blocks, instance variables and values
  • Integrate guibuilder in IDE
  • Build: bundle command-line tool with releases
  • Restore vdmjc tool to current build set
  • Occasional test hang in the interpreter's ClassesRtClassicTest

New in Overture Tool 2.1.4 (Jun 15, 2015)

  • Bug fixes:
  • Code generation of the concurrency mechanisms of VDM++
  • Problem converting composed function values
  • Type check: of the || operator in traces is missing
  • Second half of implication needlessly evaluated in class invariant
  • IO`freadval uses the default character encoding
  • Problem with || operator in combinatorial tests
  • Problem with object reference compares in postconditions
  • Code generator hangs with no error
  • Choosing what classes should be code generated to Java
  • Can't generate Java code.
  • Type constraint error with unary minus
  • Interpreter crashes on evaluation of the 'is'-expression when the checked type is recursively defined
  • Java 7 dependency in the ctruntime tests
  • Removing the vdmj_compatibility_tests projects from the code base
  • Inherited definition not visible in the sync section
  • VDMTools fails to open
  • Bug of comp operator?
  • Error Object Pattern?
  • Outline Icon for functions
  • Possibly a type checking issue with bracket types
  • Changing the default language version of a VDM project to VDM10
  • Tag Assistants with Interface
  • The CyberRail Example is broken
  • Ordering of files/folders in a VDM Explorer view
  • Proof Obliagtion Explorer doesn't refresh with spec changes

New in Overture Tool 2.1.2 (Jun 15, 2015)

  • Bug fixes:
  • Socket to IDE not valid in Console execution
  • CT Overview contents are unsorted?
  • VDM keywords are not highlighted in the Proof Obligation View
  • Combinatorial problems in 2.1.0 memory issues resulting in connection reset
  • Flat SL models with multiple files don't stop at breakpoints correctly
  • Breakpoint is being ignored in forall statement
  • Getting the values from a record type does not work
  • Abstract method can be declared private
  • Type Comparator Used Statically
  • "Send to Interpreter" does not work for SL traces
  • Type checker missing some inequalities
  • Create module to test tool functionality against all VDM examples
  • NullPointerException reported in Problems view
  • Quick Interpreter fixes
  • Fix Overture Examples
  • New type checking too tough on higher order polymorphic functions
  • undefined should be of any possible type in type checking
  • Examples Crashing Combinatorial Testing
  • Map patterns not working with munion
  • Optional types masking type unions
  • Account for is_ expressions in and clauses
  • Unify VDM Library Sources
  • CT Overview sorts test ranges lexically
  • Type checking abstract classes
  • Remove periodic/sporadic from VDM++ dialect, RM #26
  • Fix Failing Interpreter Tests
  • Parser: No warning when declaring end Module name in flat specs
  • Type check: When checking frame conditions in COMPASS a wrong warning is reported due to location comparison
  • POG error: functions with curried arguments
  • Add Matching Brackets to the Editor

New in Overture Tool 2.1.0 (Jun 16, 2014)

  • This release is formally releases two major features: the new AST-based Proof Obligation Generator, and the Java code generator.
  • The new proof obligation generator uses a new internal representation for proof obligations. The previous POG utilised strings, while the new POG uses ASTs. This allows for further processing of the POs by other plugins. From a user's perspective there should be little change --- only a few additional parentheses in the PO expressions. The new POG is the first step towards supporting automatic discharging of proof obligations, which we hope to add in the near future. Because of this, the new POG no longer the discharges trivial POs.
  • The VDM++ to Java code generator is now available as a non-experimental version. It indicates to the user if a construct cannot be generated by highlighting it in the editor using a marker (similar to the way warnings are shown) and outputs messages about it in the console. Generated code is output in the `generated/java` folder with the VDM++ project in Overture.
  • The generated Java code depends on a runtime/library to represent VDM collections, VDM types, and so forth. The source code for the runtime can be found in the Overture Github repository at: .

New in Overture Tool 2.0.8 (Jun 16, 2014)

  • This release is minor bugfix release

New in Overture Tool 2.0.6 (Jun 16, 2014)

  • This release is minor bugfix release to improve the accuracy of the typechecker.

New in Overture Tool 2.0.4 (Jun 16, 2014)

  • This release is bugfix release - many old bugs have been cleared, and some interface issues have been fixed.

New in Overture Tool 2.0.2 (Jun 16, 2014)

  • This release is primarily bugfix release - our main goal was to incorporate fixes from VDMJ that had been made since we prepared v2.0.0. A list of the bugs fixed is at the end of this release note.
  • New in this release is the preliminary inclusion of a constraint solver feature that uses the ProB model checker to broaden the executable subset of VDM that we cover.

New in Overture Tool 2.0.0 (Jun 16, 2014)

  • This release is a re-engineering of the internal structure of Overture to use a single AST across all components in the system.

New in Overture Tool 1.2.4 (Apr 3, 2013)

  • Imported renamed values now hide the original name
  • Updated User Guide to cover VDMJUnit library
  • Fixed problem with measures for functions that return functions
  • Corrected PO generation for curried polymorphic functions
  • Changes to measures for curried polymorphic functions
  • Correction for non-existent source files
  • Added -path command line option
  • Correction to mk_token comparisons to include type information.
  • Correct narrow_ type check error with unknown types
  • Small fix to cmd line options for -remote
  • Tweak to allow breakpoints to be set in flat SL specifications
  • Small PO correction for numeric subtypes
  • Type check fix for narrow_
  • Improved narrow_ syntax errors
  • Fix traces, let be st definitions were hiding subsequent let definitions
  • First cut of narrow_ extension
  • Added narrow_ regression test
  • Correct set-range expressions with non-integer arguments
  • Display the number of generated tests in runtrace
  • Fix ParameterType to work with type binds
  • Corrections to PO generation for map patterns