|
|
| Line 19: |
Line 19: |
| ** Similar to Rodin, ProB extracts typing information from all predicates. As such, <tt>xx/:{1,2}</tt> is sufficient to type <tt>xx</tt>. | | ** Similar to Rodin, ProB extracts typing information from all predicates. As such, <tt>xx/:{1,2}</tt> is sufficient to type <tt>xx</tt>. |
|
| |
|
| * DEFINITIONS: the definitions and its arguments are type 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, e.g., lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. | | * 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, e.g., lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. |
|
| |
|
| === Limitations === | | === Limitations === |
Revision as of 15:24, 8 August 2010
As of version 1.3, ProB contains a much improved parser which tries be compliant with
Atelier B as much as possible.
Atelier B Plugin
There is also a plugin for Atelier B, in order to use the standalone Tcl/Tk Version on Atelier B projects.
Differences with Atelier B
- Identifiers: ProB also allows identifiers consisting of a single letter.
- 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 left-to-right. For example, xx<:yy & yy<:NAT is sufficient to type both xx and yy in ProB.
- Similar to Rodin, ProB extracts typing information from all predicates. As such, xx/:{1,2} is sufficient to type xx.
- 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, e.g., lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions.
Limitations
- 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 sequential composition (or other uses of the semicolon).
- Well-Definedness:ProB will try to check well-definedness of your predicates during animation or model checking. For this, ProB assumes (similar to Rodin) a stricter left-to-right definition of well-definedness than Atelier B.
- closure The transitive and reflexive closure operator of classical B is not supported as defined in the B-Book by Abrial. AtelierB also does not support the operator as defined in the B-Book (as this version cannot be applied in practice). For the reflexive component of closure, ProB will compute the elements in the domain and range of the relation.
Note, however, that the transitive closure operator closure1 is fully supported, and hence one can translate an expression closure(e), where e is a binary relation over some domain d, into the expression closure1(e) \/ id(d).
- Unsupported Operators:
- fnc, rel These operators are not supported. Also, succ and pred are only supported when applied to numbers (i.e., succ(x) is supported; dom(succ) is not).
- Trees and binary trees. These onstructs are not supported (the STRING type is now supported);
- VALUES This clause of IMPLEMENTATION machines is not yet supported;