Releases: overturetool/overture
The Overture Tool version 2.3.2
Overture 2.3.2 Release Notes — 2 March 2016
What's New?
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)
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
The Overture Tool version 2.3.0
Overture 2.3.0 Release Notes — 7 October 2015
What's New?
This release adds support for the new VDM pure operations feature.
VDM Pure Operations
Excerpt from the VDM language manual, page 94, defines pure operations as follows:
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...
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.3.0
- #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.
The Overture Tool version 2.2.6
Overture 2.2.6 Release Notes — 19 June 2015
What's New?
This release contains the following:
- 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
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.2.6
- #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
The Overture Tool version 2.2.4
Overture 2.2.4 Release Notes — 30 March 2015
What's New?
This release contains bugfixes and a few usability improvements.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.2.4
- #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
The Overture Tool version 2.2.2
Overture 2.2.2 Release Notes — 27 February 2015
What's New?
This is a hotfix release that fixes critical bugs in the Combinatorial Testing
plug-in.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.2.2
The Overture Tool version 2.2.0
Overture 2.2.0 Release Notes — 11 February 2015
What's New?
This release of the Overture tool marks the transition of tool to use the Java SE 7 runtime system. There are also several small fixes as recorded below.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.2.0
- #411 Problem with object binds in traces
- #410 Internal error in the trace interpreter
- #409 Problems with filtering of tests in traces
- #408 Div rem and mod do not detect division by zero
- #407 scope of inherited constant values
- #406 Problem with type check of set ranges
- #405 Problem with access specifiers in traces
- #404 Problem with pretty printing of POs
- #386 Build: target JavaSE1.7 instead of 1.6
- #289 Type information does not seem to be fully taken into account in POG
The Overture Tool version 2.1.6
Overture 2.1.6 Release Notes — 16 January 2015
What's New?
This release contains the integration of the GUI Builder functionaly into the Overture IDE, the inclusion of the command-line tool into the distribution files, and a small collection of other bugfixes.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?q=milestone%3Av2.1.6
- #403 The Overture welcome page needs updating
- #402 Unresolved type parameters in pre-conditions
- #400 Code generation giving bug for the AutomatedStockBrokerPP standard example
- #399 Scoping problem with blocks, instance variables and values
- #398 Integrate guibuilder in IDE
- #384 Build: bundle command-line tool with releases
- #351 Restore vdmjc tool to current build set
- #280 Occasional test hang in the interpreter's ClassesRtClassicTest
The Overture Tool version 2.1.4
Overture 2.1.4 Release Notes — 20 November 2014
What's New?
This release contains small bugfixes. It also includes experimental support for code generation of concurrent models (must be turned on in preferences) and live proof obligation generation.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?milestone=18&state=closed
- #396 Code generation of the concurrency mechanisms of VDM++
- #394 Problem converting composed function values
- #393 Type check: of the || operator in traces is missing
- #392 Second half of implication needlessly evaluated in class invariant
- #391 IO`freadval uses the default character encoding
- #389 Problem with || operator in combinatorial tests
- #388 Problem with object reference compares in postconditions
- #385 Code generator hangs with no error
- #382 Choosing what classes should be code generated to Java
- #381 Can't generate Java code.
- #380 Type constraint error with unary minus
- #379 Interpreter crashes on evaluation of the 'is'-expression when the checked type is recursively defined
- #378 Java 7 dependency in the ctruntime tests
- #377 Removing the vdmj_compatibility_tests projects from the code base
- #375 Inherited definition not visible in the sync section
- #373 VDMTools fails to open
- #372 Bug of comp operator?
- #371 Error Object Pattern?
- #369 Outline Icon for functions
- #365 Possibly a type checking issue with bracket types
- #361 Changing the default language version of a VDM project to VDM10
- #330 Tag Assistants with Interface
- #301 The CyberRail Example is broken
- #276 Ordering of files/folders in a VDM Explorer view
- #163 Proof Obliagtion Explorer doesn't refresh with spec changes
The Overture Tool version 2.1.2
What's New?
This release is contains many bugfixes. Notable among them are a number of improvements to the typechecker, and a significant refactoring of the way the combinatorial testing plugin expands traces. The latter fix means that combinatorial testing supports bigger tests sets in less memory than before.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- VDM Portal
- VDM Books
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?milestone=17&state=closed
- #277 Socket to IDE not valid in Console execution
- #279 CT Overview contents are unsorted?
- #290 VDM keywords are not highlighted in the Proof Obligation View
- #318 Combinatorial problems in 2.1.0 memory issues resulting in connection reset
- #319 Flat SL models with multiple files don't stop at breakpoints correctly
- #323 Breakpoint is being ignored in forall statement
- #324 Getting the values from a record type does not work
- #326 Abstract method can be declared private
- #328 Type Comparator Used Statically
- #331 "Send to Interpreter" does not work for SL traces
- #332 Type checker missing some inequalities
- #333 Create module to test tool functionality against all VDM examples
- #334 NullPointerException reported in Problems view
- #335 Quick Interpreter fixes
- #336 Fix Overture Examples
- #337 New type checking too tough on higher order polymorphic functions
- #338 undefined should be of any possible type in type checking
- #339 Examples Crashing Combinatorial Testing
- #340 Map patterns not working with munion
- #341 Optional types masking type unions
- #342 Account for is_ expressions in and clauses
- #343 Unify VDM Library Sources
- #345 CT Overview sorts test ranges lexically
- #346 Type checking abstract classes
- #347 Remove periodic/sporadic from VDM++ dialect, RM #26
- #349 Fix Failing Interpreter Tests
- #352 Parser: No warning when declaring end Module name in flat specs
- #353 Type check: When checking frame conditions in COMPASS a wrong warning is reported due to location comparison
- #356 POG error: functions with curried arguments
- #367 Add Matching Brackets to the Editor
The Overture Tool version 2.1.0
What's New?
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: https://github.com/overturetool/overture/tree/development/core/codegen-runtime.
Reporting Problems and Troubleshooting
Please report bugs, problems, and other issues with the tool at https://github.com/overturetool/overture/issues.
If you encounter a problem with the Overture IDE itself, please contact the Overture project and we will try to help. You can contact us at [email protected], or use StackOverflow — we monitor for questions using the vdm, vdm++, or vdmrt tags.
If you encounter a problem with a VDM specification, please try to make a small example that illustrates the problem before you contact us. If you are sure the bug is not already known in the GitHub issues list, you can create a new bug report.
Other Resources and Links
- Overture Community site
- VDM Tutorials
- VDM Examples
- VDM Portal
- VDM Books
- Wikipedia on VDM
- Overture Developers Wiki on GitHub
- The Old Overture Wiki for developers
Bug fixes
Please note that the interactive list is at https://github.com/overturetool/overture/issues?milestone=12&state=closed
- #321 Problem with type checking patterns
- #316 Quickfix for VDM libraries that have not yet been added to the VDM project
- #315 Latex plugin initializes with wrong settings
- #311 Polymorphic parameters are too restricted
- #310 Set intersect can fail with named types
- #307 Outline sorting of values causes exceptions to be throws
- #299 Brackets inserted in PO from experiemental POG are not correct
- #298 Tuple selection is not correct in POG backends
- #296 Implicit operations without returns yield wrong POs
- #295 Implicit op may get the experimental POG to crash
- #293 pre-condition of operation should be taken as assumption for post-condition in POG
- #292 Experimental POG yield "null" with munion
- #291 Experimental POG has "null in POs for recursive functions
- #288 POs for pattern identifiers should not be necessary
- #287 Experimental POG needs to take lhs of implies into account
- #278 Function values not showing in Variables view
- #267 Publish to Maven Central
- #263 Remove from pom.xmls
- #189 Multiple breakpoints not working in SL?
- #132 Record fields in the Variables view are sorted