|
|
Line 37: |
Line 37: |
|
| |
|
| * ProB allows WHILE loops and sequential composition in abstract machines | | * ProB allows WHILE loops and sequential composition in abstract machines |
| | |
| | === Differences === |
| | * for ProB the order of fields in a record is not relevant (internally the fields are sorted), Atelier-B reports a type error if the order of the name of the fields changes |
| | |
| | * [[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. |
|
| |
|
| === Limitations === | | === Limitations === |
|
| |
|
| * Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write <tt>r2=rel;rel</tt>. You need to write <tt>r2=(rel;rel)</tt>. This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon). | | * Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write <tt>r2=rel;rel</tt>. You need to write <tt>r2=(rel;rel)</tt>. This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon). |
| | * Similarly, tuples without parentheses are not supported; write (a,b,c) instead of a,b,c |
|
| |
|
| * [[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: |
Revision as of 10:09, 23 April 2020
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 for use withthe standalone Tcl/Tk Version on Atelier B projects.
Differences with Atelier B
- 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.
- 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 if the preference ALLOW_COMPLEX_LETS is set to TRUE.
- 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.
- ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings, and ProB allows multi-line string literals written using three apostrophes (string)
- ProB allows WHILE loops and sequential composition in abstract machines
Differences
- for ProB the order of fields in a record is not relevant (internally the fields are sorted), Atelier-B reports a type error if the order of the name of the fields changes
- 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.
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 the sequential composition (or other uses of the semicolon).
- Similarly, tuples without parentheses are not supported; write (a,b,c) instead of a,b,c
- 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;