An Object Oriented Parser For B Specifications

Author

Fabian Fritz

Abstract

The parser is a very important part of a semantic aware editor. During the development of the B editor within the BE4 framework, it became clear, that the previously used jBTools-parser could not satisfy our needs. We also faced difficulties when implementing new features of ProB which used the same parser. It was very error-prone to maintain and to extend jBTools-parser. In this work we introduce a new object oriented parser for the B Method, called BParser. It was designed for seamless integration with BE4 and ProB.The main advantages of BParser are:

  • Maintainability
  • Extensibility
  • Fully-typed abstract syntax tree
  • Support for the complete syntax of B

We used SableCC to create an object oriented parsing framework. The object oriented design significantly reduces the development time of extensions for the parser by making the code easier to read, to maintain and to extend. BParser creates a fully-typed abstract syntax tree. A typed tree makes it less likely to break its integrity while performing a transformation. The jBTools-parser uses a syntax tree that has unnecessary nodes, such as parentheses. It also uses a single type for the nodes.

BParser improves the usability of the syntax tree by offering meaningful class and method names. The old parser uses generic names. Since all nodes have the same type, this leads to analysis code that is hard to read and to maintain.

We developed an extensive set of unit tests to ease later modifications. The test cases also gave us confidence that BParser is working as expected. In addition, it has been tested on a considerable number of real world specifications. It successfully parsed all files while the old parser rejected several valid specifications. BParser did not accept any invalid specification.

BParser is about six times slower than the old parser, but we believe that this loss of performance is an acceptable price for the robustness we gained.

We strongly believe that BParser helps to develop new and better analyses for BE4 by providing a robust, extensible and seamlessly integrated parser.

Advised By

Michael Leuschel, Jens Bendisposto

Download: PDF