No edit summary |
(→VSCode) |
||
Line 96: | Line 96: | ||
There is a package called [https://github.com/hhu-stups/b-language-extension B/ProB Language Support] available for the VSCode editor. | There is a package called [https://github.com/hhu-stups/b-language-extension B/ProB Language Support] available for the VSCode editor. | ||
It adds syntax highlighting and snippets for the specification languages B and Event-B to | 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. | It integrates with probcli to obtain error markers for syntax and type errors. | ||
Well-definedness errors can occur in B in the following circumstances:
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:
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:
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 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
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.
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: