A Scanner/Parser for the Overture Toolset

We implemented a scanner and parser for Overture using the open-source JFLEX and BYACC/J tools respectively. Our choice for those tools in particular is driven by the desire to reuse the know-how gained from building an industry-strength parser for VDMTools. This tool was implemented using lex and yacc in C++. Since we aim for the Eclipse platform in this open-source project, we require tools compatible to lex and yacc but capable to generate Java code, hence our choice for the forementioned tools.

This page describes the third public release of the Overture parser based on this technology. The parser has been validated against an existing database of examples, containing over 2000 files consisting of one or more VDM++ specifications each. The test suite covers the full VDM++ language, as described in Appendix A of the CSK VDMTools language reference manual. However, the build process currently still involves a number of manual steps and uses some custom build support tools (including a fix to a problem in BYACC/J), which makes maintenance of the parser a bit cumbersome. Therefore we decided to release the full set of sources as soon as we have resolved these issues and removed the manual steps. Despite this limitation, the current release already allows you to build your own back-end to the parser without any problems. The delivery contains:

• the org.overturetool.parser.jar and VDM.jar archives
• the astspec.zip and sources.zip archives

The first two are pre-compiled versions of the parser for the Java2 platform (will run on any 1.6.0 compliant JVM). The astspec.zip archive contains the source Java interface classes of the abstract syntax tree that is created by the parser. Furthermore, it contains a VDM++ description of each abstract syntax tree element and an overview file overture.ast from which the abstract syntax tree (Java code and VDM++ specification) is automatically generated. The file sources.zip contains:

• scanner.l the scanner definition file (input file to JFLEX)
• parser.y the parser definition file (input to a special patched version of BYACC/J, binary available below)
• OmlVisitor.java a template to implement your own AST visitor code (see below)
• TestParser.java a code sample to show how to invoke the parser (also contained in org.overturetool.parser.jar in compiled form)

How to invoke the parser

The parser should be invoked from the Windows command-line as follows (assuming that the jar files are in the current directory):

java -classpath "VDM.jar;org.overturetool.parser.jar" org.overturetool.parser.imp.TestParser <options> <files>

Don't forget to replace the semi-colon by a colon in the classpath when running on Linux or Mac!, such that it reads:

java -classpath "VDM.jar:org.overturetool.parser.jar" org.overturetool.parser.imp.TestParser <options> <files>

where options can be:

• -d to run the parser in debug mode, showing the complete derivation history performed by the parser
• -e to specify the encoding used in the UTF-8 input file. E.g. specify -eSJIS when parsing Japanese VDM++ specifications
• -sl to produce an abstract syntax tree as one VDM-SL value to standard output
• -pp to produce an abstract syntax tree as one VDM++ value to standard output
• -O (used in combination with -sl) generates an .asl file containing the abstract syntax tree
• -O (used in combination with -pp) generates an .app file containing the abstract syntax tree
• a list of filenames. If no filename is specified, the tool will read from standard input.

Features of the scanner / parser

• Support for Unicode characters in identifiers (see the note on the -e command-line option)
• Fully validated against the existing VDMTools test suite (courtesy of CSK)
• Support for the Timed VDM++ notation (a.k.a. VICE++) is included (time, duration, cycles, system and periodic constructs) and further extensions such as sporadic and interval bounded duration and cycles statements (work of Marcel Verhoef)
• Support for generic class types and untyped explicit functions (work of Thomas Christensen)
• Support for test trace definition (work of Adriana Sucena)
• Position information is derived for each abstract syntax tree element. Only available in the VDM++ version of the AST.
• A list of all tokens remains available after parsing (including all the comments that were parsed), e.g. for pretty printing.

Limitations of the current implementation

• Local function definitions inside let-expressions (and statements) are not supported. This is the only deviation from the core VDM++ language supported by VDMTools. Dynamic link modules (dlclass) are also not supported, since they are specific to VDMTools.
• Limited error-recovery functionality available at the moment.
• We only support "flat" UTF-8 input files. No support for rtf or latex input files (yet).
• The ability to read and write the abstract syntax trees as XML files is still lacking. Do not spend energy on this; it is on top of our priority list to fix.

Building your own back-end

There are two ways to create your own back-end to the parser. The first is to hand-code one in Java and the second is to specify it in VDM++ and use code generation. The former is only suggested for simple, light-weight, tasks such as pretty printing. The latter is strongly recommended for complex abstract syntax tree manipulations. Our abstract syntax tree implementation supports the well-known visitor pattern. But even more so, template visitors are already created for you for both approaches. The following paragraphs will expain how to do it in either case.

Coding your own back-end directly in Java

Create a new Java project in Eclipse. Add VDM.jar and org.overturetool.parser.jar to the build path of your project. Copy OmlVisitor.java from sources.zip into the destination directory of your choice inside your Eclipse Java project. Rename the class name into some meaningful name for your application, e.g. PrettyPrint. If you press "Save" then an empty visitor is compiled and ready to run! All you need to do is to fill in the body of all the visit operators in the class. Check TestParser.java on how-to couple the parser to your hand-coded visitor implementation.

Specifying your own back-end in VDM++ and code generate to Java

If you have access to the full version of VDMTools (with code generation, which is available free of charge under the academic license programme), the following method is preferable. Copy all the tex files, except VdmSlVisitor.tex, from astspec.zip into a location of your choice. Add all these files to a new project inside VDMTools. Rename the file OmlVisitor.tex into something meaningful for your application, e.g. TypeCheck.tex. Also rename the class name inside the file (don't forget to change the label at the bottom of the file as well). Syntax and type check the specification using VDMTools. If there are no errors then you are ready to specify the individual visit operations in VDM++. When you are satisfied with the specification, you can use the VDMTools Java code generator to create and build your application. Check TestParser.java on how-to couple the parser to your generated visitor implementation.

Known issues

Always use a 1.6.0 compliant version of the Java Runtime Environment. Older java versions may cause problems.

Contact us

If you find problems in the current parser release, please send us a bug-report. If you have suggestions for changes to the grammar, send us the modified versions of the files supplied in the archive, in particularly overture.ast, parser.y and scanner.l.

If you have any questions about the Overture parser please contact Marcel Verhoef

Downloads

• parser.zip: Updated parser (third public release) with position info and test trace support

• traces.zip: Example files for test trace creation

• astgen.zip: tools to generate AST classes from overture.ast file

• byaccj.zip: patched byaccj version (win32 binary) + source fixes