Well-Definedness Checking
Well-Definedness Errors
Well-definedness errors can occur in B in the following circumstances:
- a division by 0: r=100/0
- modulo by 0, modulo involving negative numbers: r=100 mod -2
- exponentiation using a negative exponent: 2**(-2)
- application of a function outside of its domain: f={1|->2} & r=f(3)
- application of a relation which is not a function: f={1|->2,1|->3} & r=f(1)
- application of the card operator to infinite sets: card(NATURAL)
- application of the min or max operator to empty sets: x={} & r=max(x)
- application of the inter operator to empty sets: x={} & r=inter(x)
- wrong application of sequence operators
- taking the first, front, last, tail of an empty sequence: x=<> & r=first(x)
- using negative indexes for prefix or suffix sequence: x = s /|\ -1
- using too large indexes for suffix sequence: x= s \|/ (size(s)+1)
- ...
To ensure that your models only contain well-defined formulas, the B language relies on the generation of well-definedness proof obligations. The Rodin toolset can generate them for Event-B models and Atelier-B can create them for classical B and Event-B models. ProB will check for well-definedness during constraint solving, animation and model checking. However, by default this check is not very extensive. You can force ProB to look more aggressively for well-definedness issues in your formulas by setting the following preference to true:
- TRY_FIND_ABORT
However, even with this, the search is not (yet) guaranteed to be exhaustive. Also, ProB's constraint solving does not necessarily solve formulas from left to right. Hence, the following formulas will be considered well-defined (and on can argue that they are) by ProB:
- r=1/x & x/=0
Technically speaking, for disjunctions and implications ProB uses the L-system of well-definedness (i.e., for P => Q, P should be well-defined and if P is true then Q should also be well-defined).
Generating and Checking Well-Definedness Proof Obligations in ProB
Hence, since the version 1.10.0 (and in the nightly version since beginning of April 2020), ProB includes a POG (proof obligation generator) for WD (well-definedness) POs (proof-obligations).
This POG can deal with the full B language as supported by ProB, as well as the extensions supported by ProB (such as IF-THEN-ELSE or LET for expressions and predicates). ProB also includes a light-weight prover, which tries and discharge these WD POs. If all WD POs are discharged, one also does not need to set the TRY_FIND_ABORT preferences above. In future, we plan to automatically run the POG and prover on loaded B machines, and automatically enable stricter WD checking for those parts which have not been discharged.
There are various ways you can call the POG and visualise the result of the prover. Take the following simple B machine
MACHINE WDSimpleTest CONSTANTS a,n PROPERTIES n:NATURAL & a:1..n --> 1..10 & a(1) = 1 & a(n) = max(ran(a)) END
probcli
For the command-line version of ProB you can use the -wd-check command:
probcli WDSimpleTest.mch -wd-check
! A warning occurred (source: well_def_analyser) !
! WD-PO [AXM] not discharged: 1 : dom(a)
! Line: 6 Column: 2 until Line: 6 Column: 6 in file: WDSimpleTest.mch
! A warning occurred (source: well_def_analyser) !
! WD-PO [AXM] not discharged: n : dom(a)
! Line: 7 Column: 2 until Line: 7 Column: 6 in file: WDSimpleTest.mch
! A warning occurred (source: well_def_analyser) !
! WD-PO [AXM] not discharged: finite(ran(a)) & ran(a) /= {}
! Line: 7 Column: 9 until Line: 7 Column: 20 in file: WDSimpleTest.mch
Analysis walltime: 54 ms
Stats: [discharged_po/2,not_discharged_po/3,AXM/5]
WD Analysis Result: discharged 2 / 5 (40.00 %)
After changing the predicate n:NATURAL to n:NATURAL1 one obtains:
probcli WDSimpleTest.mch -wd-check Analysis walltime: 31 ms Stats: [not_discharged_po/0,discharged_po/5,AXM/5] WD Analysis Result: discharged 5 / 5 (100.00 %)
ProB Tcl/Tk
In ProB Tcl/Tk you can use the commands in the Static Checking sub-menu of the Verify menu:
With the "Check Well-Definedness POs" commands you get a list of warnings and high-lighted locations of undischarged WD POs:
With the "Show Well-Definedness POs" commands you get a list of all the WD POs (discharged or not):
ProB2-UI
In the ProB2-UI the above list of Well-Definedness POs is available in the Table view.
Atom
There is a package language-b-eventb available for the Atom editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom. It integrates with probcli to obtain error markers for syntax and type errors.
With the Atom plugin you can now also visualize WD (well-definedness) issues in your B machines. You need to enable WD checking in the preferences of the plugin:
Then you see undischarged WD POs in the editor window and can hover over them to obtain further information:
