Using ProB with Atelier B: Difference between revisions

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 with the standalone Tcl/Tk Version on Atelier B projects. With this you can animate and model check B machines directly from within the IDE of Atelier-B.

Atelier B also enables to use ProB as a prover/disprover in the interactive proof window. For this you need to set the ProB_Path resource to point to probcli (command-line version of ProB). To do this you need to add the following line to the resource file of your project (replacing PATH by the the path on your machine to probcli):

ATB*PR*ProB_Path:PATH/probcli

Then you can type, e.g., the command prob(1)in the interactive proof window.

Two commands are provided within Atelier-B:

• prob(n) tries to prove the goal with the selected hypotheses (selected using rp.n as is done for th e pp command of Atelier-B)
• prob(n|t) is similar but also limits the execution time of ProB to t seconds

Atelier-B will call probcli using the commands -cbc_assertions_tautology_proof and -cbc_result_file after having encoded the proof obligation into the ASSERTIONS clause of a generated B machine.

The generated machine typically has the form:

MACHINE probNr
SETS ...
CONSTANTS ...
PROPERTIES
  << ALL HYPOTHESES >>
ASSERTIONS
  ( <<SELECTED HYPOTHESES >>
   =>
  << PROOF GOAL >>
  )
END

Differences with Atelier B

Extra Features of ProB

• 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 to use the Event-B relation operators <<->, <->>, <<->>

• 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). You also generally need to put BEGIN and END around the sequential composition operator, e.g., Op = BEGIN x:=1;y:=2 END.
• 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;

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