Summary of B Syntax - Revision history

Michael Leuschel: /* Differences with AtelierB/B4Free */

2025-03-14T11:57:08Z

Differences with AtelierB/B4Free

← Older revision		Revision as of 11:57, 14 March 2025
Line 531:		Line 531:
	- for ProB the order of fields in a record is not relevant (internally the fields are		- 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		sorted), Atelier-B reports a type error if the order of the name of the fields changes
			- for ProB closure(X) = id(TypeOfX) \/ closure1(X), i.e., closure({1\|->2}) contains
			1\|->1, 2\|->2 but also 3\|->3, 4\|->4, ... This corresponds to the definition in
			Abrial's B-Book, but Atelier-B's definition does not cotain 3\|->3, 4\|->4, ...
	- well-definedness: for disjunctions and implications ProB uses the L-system		- well-definedness: for disjunctions and implications ProB uses the L-system
	of well-definedness (i.e., for P => Q, P should be well-defined and		of well-definedness (i.e., for P => Q, P should be well-defined and

Michael Leuschel: /* Comments and Pragmas */

2025-03-06T15:25:38Z

Comments and Pragmas

← Older revision		Revision as of 15:25, 6 March 2025
Line 471:		Line 471:
	introduced identifier (in VARIABLES, CONSTANTS,... section)		introduced identifier (in VARIABLES, CONSTANTS,... section)
	There are three special descriptions:		There are three special descriptions:
	/@desc memo/ to be put after identifiers in the ABSTRACT_CONSTANTS section		/@desc memo/ to be put after identifiers in the ABSTRACT_CONSTANTS section
	indicating that these functions should be memoized		indicating that these functions should be memoized
	/@desc expand/ to be put after identifiers (in VARIABLES, CONSTANTS,... section)		/@desc expand/ to be put after identifiers (in VARIABLES, CONSTANTS,... section)
	indicating that they should be expanded and not kept symbolically		indicating that they should be expanded and not kept symbolically
	/@desc prob-ignore / to be put after predicates (e.g., in PROPERTIES) which		/@desc prob-ignore / to be put after predicates (e.g., in PROPERTIES) which
	should be ignored by ProB		should be ignored by ProB
	when the preference USE_IGNORE_PRAGMAS is TRUE		when the preference USE_IGNORE_PRAGMAS is TRUE
	You can also add description to an operation at the end of the operation body.		You can also add description to an operation at the end of the operation body.
	This description can be viewed in ProB Tcl/Tk, ProB2-UI and in the HTML trace exports.		This description can be viewed in ProB Tcl/Tk, ProB2-UI and in the HTML trace exports.

Michael Leuschel: /* Comments and Pragmas */

2025-03-06T15:24:18Z

Comments and Pragmas

← Older revision		Revision as of 15:24, 6 March 2025
Line 478:		Line 478:
	should be ignored by ProB		should be ignored by ProB
	when the preference USE_IGNORE_PRAGMAS is TRUE		when the preference USE_IGNORE_PRAGMAS is TRUE
			You can also add description to an operation at the end of the operation body.
			This description can be viewed in ProB Tcl/Tk, ProB2-UI and in the HTML trace exports.
			Note: this description can contain ${Expr} template string expressions which reference parameter
			and variable values to provide a specific description for each operation execution.
	/@file PATH / associates a file for machines in SEES, INCLUDES, ...		/@file PATH / associates a file for machines in SEES, INCLUDES, ...
	put pragma after a seen or included machine		put pragma after a seen or included machine

Vella: /* Differences with AtelierB/B4Free */

2024-06-13T13:07:20Z

Differences with AtelierB/B4Free

← Older revision		Revision as of 13:07, 13 June 2024
Line 515:		Line 515:
	Here are the main differences with Atelier B:		Here are the main differences with Atelier B:
	<pre>		<pre>
	- tuples without parentheses are not supported; write (a,b,c) instead of a,b,c		- tuples without parentheses are not supported; write (a,b,c) instead of a,b,c
	- relational composition has to be wrapped into parentheses; write (f;g)		- relational composition has to be wrapped into parentheses; write (f;g)
	- parallel product also has to be wrapped into parentheses; write (f\|\|g)		- parallel product also has to be wrapped into parentheses; write (f\|\|g)
	- not all tree operators are supported		- not all tree operators are supported
	- the VALUES clause is only partially supported		- the VALUES clause is only partially supported
	- definitions have to be syntactically correct and be either an expression,		- definitions have to be syntactically correct and be either an expression,
	predicate or substitution;		predicate or substitution;
	the arguments to definitions have to be expressions;		the arguments to definitions have to be expressions;
	definitions which are predicates or substitutions must be declared before first use		definitions which are predicates or substitutions must be declared before first use
	- definitions are local to a machine		- definitions are local to a machine
	- for ProB the order of fields in a record is not relevant (internally the fields are		- 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		sorted), Atelier-B reports a type error if the order of the name of the fields changes
	- well-definedness: for disjunctions and implications ProB uses the L-system		- well-definedness: for disjunctions and implications ProB uses the L-system
	of well-definedness (i.e., for P => Q, P should be well-defined and		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)		if P is true then Q should also be well-defined)
	- ProB allows WHILE loops and sequential composition in abstract machines		- ProB allows WHILE loops and sequential composition in abstract machines
	- ProB now allows the IF-THEN-ELSE and LET for expressions and predicates		- ProB now allows the IF-THEN-ELSE and LET for expressions and predicates
	(e.g., IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END)		(e.g., IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END)
	- ProB's type inference is stronger than Atelier-B's, much less typing predicates		- ProB's type inference is stronger than Atelier-B's, much less typing predicates
	are required		are required
	- ProB accepts operations with parameters but without pre-conditions		- You can apply prj1 and prj2 without providing the type arguments, e.g., prj2(prj1(1\|->2\|->3))
	- ProB allows identifiers consisting of a single character and identifiers in single backquotes (`id`)		- ProB accepts operations with parameters but without pre-conditions
	- ProB allows to use <> for the empty sequence (but this use is deprecated)		- ProB allows identifiers consisting of a single character and identifiers in single backquotes (`id`)
	- ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings,		- ProB allows to use <> for the empty sequence (but this use is deprecated)
	and ProB allows multi-line string literals written using three apostrophes ('''string''')		- ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings,
	as well as template strings using three backquotes (e.g., ```1+2=${1+2}```)		and ProB allows multi-line string literals written using three apostrophes ('''string''')
	- ProB allows a she-bang line in machine files starting with #!		as well as template strings using three backquotes (e.g., ```1+2=${1+2}```)
	~~(If you discover more differences, please let us know!)~~		- ProB allows a she-bang line in machine files starting with #!
	- ProB allows btrue and bfalse as predicates in B machines		- ProB allows btrue and bfalse as predicates in B machines
	- ProB allows to use the Event-B relation operators <<->, <->>, <<->>		- ProB allows to use the Event-B relation operators <<->, <->>, <<->>
	- ProB allows set comprehensions with an extra expression like {x•x:1..10\|x*x}.		- ProB allows set comprehensions with an extra expression like {x•x:1..10\|x*x}.
	- The FREETYPES section and the external libraries (LibraryStrings.def, ...) do not exist in Atelier-B		- The FREETYPES section and the external libraries (LibraryStrings.def, ...) do not exist in Atelier-B
	</pre>		</pre>

Line 556:		Line 556:
	<pre>		<pre>
	- AtelierB/ProB do not allow true as predicate;		- AtelierB/ProB do not allow true as predicate;
	e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead), ProB allows btrue as ~~predicate~~.		e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead)
			ProB now allows btrue and bfalse to be used as predicates.
	- AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES		- AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES
	- AtelierB/ProB require a scalar machine parameter to be typed in the		- AtelierB/ProB require a scalar machine parameter to be typed in the
Line 562:		Line 563:
	- In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined		- In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined
	</pre>		</pre>

			If you discover more differences, please let us know!

	=== Other notes ===		=== Other notes ===

Vella: /* Other notes */

2024-06-13T12:51:06Z

Other notes

← Older revision		Revision as of 12:51, 13 June 2024
Line 565:		Line 565:
	=== Other notes ===		=== Other notes ===
	<pre>		<pre>
			ProB now supports the Unicode mathematical symbols, exactly like Atelier-B
	ProB is best at treating universally quantified formulas of the form		ProB is best at treating universally quantified formulas of the form
	!x.(x:SET => RHS), or		!x.(x:SET => RHS), or
	!(x,y).(x\|->y:SET =>RHS), !(x,y,z).(x\|->y\|->z:SET =>RHS), ...;		!(x,y).(x\|->y:SET =>RHS),
			!(x,y,z).(x\|->y\|->z:SET =>RHS), ...;
	otherwise the treatment of !(x1,...,xn).(LHS => RHS) may delay until all values		otherwise the treatment of !(x1,...,xn).(LHS => RHS) may delay until all values
	treated by LHS are known.		treated by LHS are known.
Line 574:		Line 576:
	The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B		The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B
	finite(S) operator.		finite(S) operator.
	ProB assumes that machines and STRING values are encoded using UTF-8.		ProB assumes that machines and STRING values are encoded using UTF-8.
	</pre>		</pre>

Vella: /* File Extensions */

2024-06-13T12:48:40Z

File Extensions

← Older revision		Revision as of 12:48, 13 June 2024
Line 491:		Line 491:
	=== File Extensions ===		=== File Extensions ===
	<pre>		<pre>
	.mch for abstract machine files		.mch for abstract machine files
	.ref for refinement machines		.ref for refinement machines
	.imp for implementation machines		.imp for implementation machines
	.def for DEFINITIONS files		.def for DEFINITIONS files
	.rmch for Rules machines for data validation		.rmch for Rules machines for data validation
	</pre>		</pre>

Vella: /* Comments and Pragmas */

2024-06-13T12:48:10Z

Comments and Pragmas

← Older revision		Revision as of 12:48, 13 June 2024
Line 457:		Line 457:
	<pre>		<pre>
	B supports two styles of comments:		B supports two styles of comments:
	/* ... */ block comments		/* ... */ block comments
	// ... line comments		// ... line comments
	</pre>		</pre>

Line 464:		Line 464:
	The whitespace between @ and PRAGMA is optional.		The whitespace between @ and PRAGMA is optional.
	<pre>		<pre>
	/@symbolic / put before comprehension set or ~~lambda~~ to instruct ProB		/@symbolic / put before comprehension set, lambda, union or composition to instruct ProB
	to keep it symbolic and not try to compute it explicitly		to keep it symbolic and not try to compute it explicitly
	/@label LBL / associates a label LBL with the following predicate		/@label LBL / associates a label LBL with the following predicate
	(LBL must be identifier or a string "....")		(LBL must be identifier or a string "....")
	/@desc DESC / associates a description DESC with the preceding predicate or		/@desc DESC / associates a description DESC with the preceding predicate or
	introduced identifier (in VARIABLES, CONSTANTS,... section)		introduced identifier (in VARIABLES, CONSTANTS,... section)
	There are ~~two~~ special descriptions		There are three special descriptions:
	/@desc memo/ to be put after identifiers in the ABSTRACT_CONSTANTS section		/@desc memo/ to be put after identifiers in the ABSTRACT_CONSTANTS section
	indicating that these functions should be memoized		indicating that these functions should be memoized
	/@desc prob-ignore / to be put after predicates (e.g., in PROPERTIES) which		/@desc expand/ to be put after identifiers (in VARIABLES, CONSTANTS,... section)
	should be ignored by ProB		indicating that they should be expanded and not kept symbolically
	when the preference USE_IGNORE_PRAGMAS is TRUE		/@desc prob-ignore / to be put after predicates (e.g., in PROPERTIES) which
	/@file PATH / associates a file for machines in SEES, INCLUDES, ...		should be ignored by ProB
	put pragma after a seen or included machine		when the preference USE_IGNORE_PRAGMAS is TRUE
	/@package NAME / at start of machine, machine file should be in folder NAME/...		/@file PATH / associates a file for machines in SEES, INCLUDES, ...
	NAME can be qualified N1.N2...Nk, in which case the machine		put pragma after a seen or included machine
	file should be in N1/N2/.../Nk		/@package NAME / at start of machine, machine file should be in folder NAME/...
	/@import-package NAME / adds ../NAME to search paths for SEES,...		NAME can be qualified N1.N2...Nk, in which case the machine
	NAME can also be qualified N1.N2...Nk, use after package pragma		file should be in N1/N2/.../Nk
	/@generated / can be put at the top of a machine file; indicates the machine		/@import-package NAME / adds ../NAME to search paths for SEES,...
	is generated from some other source ~~and should not be edited~~		NAME can also be qualified N1.N2...Nk, use after package pragma
			/@generated / can be put at the top of a machine file; indicates the machine
			is generated from some other source
	</pre>		</pre>

Vella: /* Definitions */

2024-06-13T12:43:14Z

Definitions

Show changes

Vella: /* Machine inclusion */

2024-06-13T12:35:37Z

Machine inclusion

← Older revision		Revision as of 12:35, 13 June 2024
Line 352:		Line 352:
	=== Machine inclusion ===		=== Machine inclusion ===
	<pre>		<pre>
	USES list of machines		USES list of machines
	INCLUDES list of machines		INCLUDES list of machines
	SEES list of machines		SEES list of machines
	EXTENDS list of machines		EXTENDS list of machines
	PROMOTES list of operations		PROMOTES list of operations
	REFINES machine		REFINES machine
	</pre>		</pre>

Vella: /* Machine inclusion */

2024-06-13T12:35:12Z

Machine inclusion

← Older revision		Revision as of 12:35, 13 June 2024
Line 352:		Line 352:
	=== Machine inclusion ===		=== Machine inclusion ===
	<pre>		<pre>
	USES list of machines		USES list of machines
	INCLUDES list of machines		INCLUDES list of machines
	SEES list of machines		SEES list of machines
	EXTENDS list of machines		EXTENDS list of machines
	PROMOTES list of operations		PROMOTES list of operations
	REFINES machine		REFINES machine
	</pre>		</pre>