Line 39: | Line 39: | ||

* [[Well-Definedness_Checking|Well-definedness]]: ProB will try to check if your predicates are well-defined during animation or model checking. For this ProB assumes (similar to Rodin) a stricter left-to-right definition of well-definedness than Atelier B. | * [[Well-Definedness_Checking|Well-definedness]]: ProB will try to check if your predicates are well-defined during animation or model checking. For this ProB assumes (similar to Rodin) a stricter left-to-right definition of well-definedness than Atelier B. | ||

* Unsupported Operators: | * Unsupported Operators: | ||

** Trees and binary trees: most but not all tree operators (mirror, infix) are supported yet | ** Trees and binary trees: most but not all tree operators (mirror, infix) are supported yet. These operators may disappear in future version of Atelier B and may also disappear from ProB. | ||

** <tt>VALUES</tt>: This clause of the <tt>IMPLEMENTATION</tt> machines is not yet supported; | ** <tt>VALUES</tt>: This clause of the <tt>IMPLEMENTATION</tt> machines is not yet fully supported; | ||

* There are also some general limitations wrt refinements. See [[Current Limitations#Multiple Machines and Refinements]] for more details. | * There are also some general limitations wrt refinements. See [[Current Limitations#Multiple Machines and Refinements]] for more details. |

As of version 1.3, ProB contains a much improved parser which tries be compliant with
Atelier B as much as possible.

There is also a plugin for Atelier B for use withthe standalone Tcl/Tk Version on Atelier B projects.

- Identifiers: ProB also allows identifiers consisting of a single letter. ProB also accepts enumerated set elements to be used as identifiers.

- Lexing: The Atelier-B parser (
`bcomp`) reports a lexical error (`illegal token |-`) if the vertical bar (|) of a lambda abstraction is followed directly by the minus sign.

- Typing:
- ProB makes use of a unification-based type inference algorithm. As such, typing information can not only flow from left-to-right inside a formula, but also from right-to-left. For example, it is sufficient to type
`xx<:yy & yy<:NAT`instead of typing both`xx`and`yy`in ProB. - Similar to Rodin, ProB extracts typing information from all predicates. As such, it is sufficient to write
`xx/:{1,2}`to assign a type to`xx`. - the fields of records are normalized (sorted); hence the predicate
`rec(a:0,b:1) = rec(b:y,a:x)`is correctly typed for ProB.

- ProB makes use of a unification-based type inference algorithm. As such, typing information can not only flow from left-to-right inside a formula, but also from right-to-left. For example, it is sufficient to type

- DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You
**cannot**use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with`PLUS(x,y) == x+y`, the expression`PLUS(2,3)*10`will evaluate to 50 (and not to 32 as with Atelier-B).

- for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows
`LET x,y BE x=2 & y=x*x IN ... END`

- ProB allows WHILE loops and sequential composition in abstract machines

- ProB now allows the IF-THEN-ELSE for expressions and predicates:
`IF x<0 THEN -x ELSE x END`

- ProB now allows LET constructs for expressions and predicates

- ProB allows
`btrue`and bfalse as predicates.

- Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write
`r2=rel;rel`. You need to write`r2=(rel;rel)`. This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon).

- Well-definedness: ProB will try to check if your predicates are well-defined during animation or model checking. For this ProB assumes (similar to Rodin) a stricter left-to-right definition of well-definedness than Atelier B.

- Unsupported Operators:
- Trees and binary trees: most but not all tree operators (mirror, infix) are supported yet. These operators may disappear in future version of Atelier B and may also disappear from ProB.
`VALUES`: This clause of the`IMPLEMENTATION`machines is not yet fully supported;

- There are also some general limitations wrt refinements. See Current Limitations#Multiple Machines and Refinements for more details.