Mathematical Language Evolution Design

Introduction

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 will not be recognized if version is V1. It is accepted only from version V2. Conversely, KPRJ1 is accepted for V1 but not for V2.

Parsing

FormulaFactory has new parse() methods with a parser version argument. Existing methods default to the latest version. To cope with version problems, parsing is done in several steps:

• try to parse with the given version (or latest by default)
• if parse succeeds, the result is returned as usual
• else, try to parse with older versions incrementally
  • if no version succeeds, return the failed result of the parse call with the latest version
  • else propose upgrading from the highest succeeding version to the latest

Multiple Predicates / Partition

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

Visitors

IVisitor has three more methods:

• enter KPARTITION
• continue KPARTITION
• exitKPARTITION

ISimpleVisitor has one more method:

• visitMultiplePredicate

Sequent Prover

TODO

Affected client code

TODO