We are delighted to announce Dezyne 2.10: The first standalone release of Dezyne. Dezyne no longer depends on a server to do verification or code or view generation.
Dezyne 2.10 demarcates the "core" of the Dezyne language. Its intent is to offer the essentials in terms of language features and user experience. The "core" simulation function (linking the model to state or trace and vice versa) is not yet included. Also, "core" code generation is C++ and mCRL2 only.
The documentation, which has not been fully updated for 2.10 yet, is available here: https://doc.verum.com/documentation.html.
2.11 aims to re-introduce simulation and visualization similar to 2.9. Furthermore, Dezyne supporting features such as code browsing/navigation and a modicum of code completion will be provided by means of LSP, such that you can use your personal favorite LSP-aware editor.
Here are the MD5 and SHA1 checksums:
0dc90695b938ebbc88e2b036cc75223e dezyne-2.10.0-x86_64-linux.tar.gz 23ba189775292d97983f81b3537e9dfe dezyne-2.10.0-i686-windows.zip c4e0c790922fad118c1a9dec9ae4327f26668d26 dezyne-2.10.0-x86_64-linux.tar.gz 1e567ddd4b59ff5346cf558409b26eb6bb40dcb4 dezyne-2.10.0-i686-windows.zip
[*] Use a .sig file to verify that the corresponding file (without the .sig suffix) is intact. First, be sure to download both the .sig file and the corresponding tarball. Then, run a command like this:
gpg --verify dezyne-2.10.0-x86_64-linux.tar.gz.sig
If that command fails because you don't have the required public key, then run this command to import it:
gpg --keyserver keys.gnupg.net --recv-keys 1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273
and rerun the 'gpg --verify' command.
Get informed, get involved
#dezyne on irc.freenode.net.
Changes in 2.10.0 since 2.9.1
Dezyne is now stand alone, client only, serverless, pure GNU Guile Scheme.
- Removed: server, services, dzn, dzn/daemon.
- All error messages were changed.
- "Use before declare" is no longer supported for variables.
dollar-statements used inside a namespace are now rejected.
- C++: The tracing interface was changed, notably the "dzn::trace_in" function was renamed to "dzn::trace".
- C++: Experimental state-variable tracing is now disabled.
- Other languages were dropped.
- The component simulator was removed.
Noteworthy bug fixes
Fixed a bug where function calls immediately following an
if-statement were not considered by the verifier
Fixed a bug where an
enum-fieldtest used as the expression in a reply statement would crash the verifier.
Fixed a bug where a boolean
notused as the expression in a reply statement was ignored.
Fixed a bug with precedence in deeply nested boolean expresisons in generated code.
The Verum Team
In Dezyne, you define components and their interfaces through a familiar and compact C/Java like-language. The Dezyne language is targeted at the logic or event-driven behaviour of an application. The interfaces are the specification and the components are the implementation.
Dezyne automatically verifies semantic correctness of the logic behaviour and proves that the components correctly implement the interfaces. A user can simulate the behaviour to validate whether this is as intended. Diagrams and logical views are generated automatically from the language description. As a final step code can be generated in a number of standard programming languages.
Without having to rely on a process Dezyne automatically highlights problems areas, stimulates communication about these and enforces that components work together.
verum.com is a leading developer of software design tools to create, simulate, mathematically verify and automatically generate code for embedded and cyber-physical systems.
At Verum, we help our customers and partners solve the most challenging software issues of today and tomorrow. We support customers with our product Dezyne, a software engineering toolset that enables engineers to specify, design, validate and formally verify software components for embedded systems combined with consultancy services.