Mathematical Language Evolution Design

From Event-B
Revision as of 07:48, 1 April 2009 by imported>Nicolas (→‎Parsing)
Jump to navigationJump to search


This document describes the modifications that occur to the Event-B mathematical language from the developer point of view. The old language will still be recognized, in order to provide backward compatibility.

Syntax Tree

Deprecated nodes (becoming atomic expressions):

  • KPRJ1
  • KPRJ2
  • KID

New nodes:

  • KPARTITION that represents the new partition predicate (relational predicate)
  • KPRJ1_GEN that represents the atomic version of the first projection
  • KPRJ2_GEN that represents the atomic version of the second projection
  • KID_GEN that represents the atomic version of the identity

Parser Changes

The new parser has a version attribute. Depending on the version, formulas are parsed differently. Thus, the KPARTITION node is illegal if version is V1. It is accepted only from version V2. Concerning, identity and projections, they are recognized as non-generic with V1 and generic with V2. The following table summarizes how tokens are processed depending on the parser version:

Token Recognition
Parser V1 Parser V2
"partition" illegal KPARTITION
"prj1" KPRJ1 KPRJ1_GEN
"prj2" KPRJ2 KPRJ2_GEN


FormulaFactory has new parse() methods with a parser version argument. Existing methods default to the first version (ParserVersion.V1), while becoming deprecated. Thus, one now has to know, before parsing a formula, the version of the language it has been written with.

TODO: How to get the version from the file

Multiple Predicates / Partition

A new predicate class is introduced: MultiplePredicate that is abstract and superclasses Partition. A MultiplePredicate is a predicate that applies to a list of two or more expressions. In a Partition, all expressions must have the same type, that is the type of the partitioned set (first child).




IVisitor has three more methods:

  • enter KPARTITION
  • continue KPARTITION

ISimpleVisitor has one more method:

  • visitMultiplePredicate

Sequent Prover


Affected client code