Well-Definedness Checking - Revision history

Michael Leuschel: /* probcli */

2025-02-07T13:52:13Z

probcli

← Older revision		Revision as of 13:52, 7 February 2025
Line 78:		Line 78:
	</pre>		</pre>

	Note: you can also [Proving_Theorems_in_the_ProB_REPL#Calling_ProB's_WD_Prover\|call the WD prover directly in the REPL] of ProB using the <tt>:prove</tt> command.		Note: you can also [[Proving_Theorems_in_the_ProB_REPL#Calling_ProB's_WD_Prover\|call the WD prover directly in the REPL]] of ProB using the <tt>:prove</tt> command.

	=== ProB Tcl/Tk ===		=== ProB Tcl/Tk ===

2025-02-07T13:52:00Z

probcli

← Older revision		Revision as of 13:52, 7 February 2025
Line 77:		Line 77:
	WD Analysis Result: discharged 5 / 5 (100.00 %)		WD Analysis Result: discharged 5 / 5 (100.00 %)
	</pre>		</pre>

			Note: you can also [Proving_Theorems_in_the_ProB_REPL#Calling_ProB's_WD_Prover\|call the WD prover directly in the REPL] of ProB using the <tt>:prove</tt> command.

	=== ProB Tcl/Tk ===		=== ProB Tcl/Tk ===

2021-05-18T11:05:24Z

Update ProB2-UI link

← Older revision		Revision as of 11:05, 18 May 2021
Line 92:		Line 92:
	=== ProB2-UI ===		=== ProB2-UI ===

	In the [[~~ProB2_JavaFX_UI\|~~ProB2-UI]] the above list of Well-Definedness POs is available in the Table view.		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.

2020-09-23T08:36:38Z

Generating and Checking Well-Definedness Proof Obligations in ProB

← Older revision		Revision as of 08:36, 23 September 2020
Line 32:		Line 32:
	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).		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 [[Media:wd_prob.pdf\|Fast and Effective Well-Definedness Checking]].		There is an article about this new POG and prover entitled [[Media:wd_prob.pdf\|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).		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).

2020-07-09T09:23:27Z

Generating and Checking Well-Definedness Proof Obligations in ProB

← Older revision		Revision as of 09:23, 9 July 2020
Line 31:		Line 31:

	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).		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 [[Media:wd_prob.pdf\|Fast and Effective Well-Definedness Checking]].

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

2020-07-09T08:55:43Z

Generating and Checking Well-Definedness Proof Obligations in ProB

← Older revision		Revision as of 08:55, 9 July 2020
Line 30:		Line 30:
	== Generating and Checking Well-Definedness Proof Obligations in ProB ==		== 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).		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).

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

2020-07-07T05:13:42Z

ProB2-UI

← Older revision		Revision as of 05:13, 7 July 2020
Line 91:		Line 91:

	In the [[ProB2_JavaFX_UI\|ProB2-UI]] the above list of Well-Definedness POs is available in the Table view.		In the [[ProB2_JavaFX_UI\|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.

	=== VSCode ===		=== VSCode ===

2020-06-17T08:19:32Z

VSCode

← Older revision		Revision as of 08:19, 17 June 2020
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 ~~Atom~~.		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.

2020-06-17T07:46:39Z

@@ Line 98: / Line 98: @@
 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.
 === Atom ===

2020-06-17T07:42:05Z

← Older revision		Revision as of 07:42, 17 June 2020
Line 91:		Line 91:

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

			=== VSCode ===


			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 Atom.
			It integrates with probcli to obtain error markers for syntax and type errors.

	=== Atom ===		=== Atom ===