m (Update ProB2-UI link) |
|||

Line 92: | Line 92: | ||

=== ProB2-UI === | === ProB2-UI === | ||

In the [[ | In the [[ProB2-UI]] the above list of Well-Definedness POs is available in the Table view. | ||

One can also view the undischarged WD POs by running Well-Definedness checking in the "Symbolic Verification" view. | One can also view the undischarged WD POs by running Well-Definedness checking in the "Symbolic Verification" view. | ||

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)`

- taking the first, front, last, tail of an empty sequence:
- ...

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).

Hence, since the version 1.10.0 (and in the nightly version since April 2020), ProB includes a POG (proof obligation generator) for WD (well-definedness) POs (proof-obligations).

There is an article about this new POG and prover entitled Fast and Effective Well-Definedness Checking (accepted for iFM'2020).

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

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 %)

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):

In the ProB2-UI the above list of Well-Definedness POs is available in the Table view. One can also view the undischarged WD POs by running Well-Definedness checking in the "Symbolic Verification" view.

There is a package called B/ProB Language Support available for the VSCode editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to VSCode. It integrates with probcli to obtain error markers for syntax and type errors.

With the VSCode plugin you can 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:

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: