Tips: B Idioms - Revision history

Michael Leuschel at 09:38, 2 October 2017

2017-10-02T09:38:30Z

← Older revision		Revision as of 09:38, 2 October 2017
Line 7:		Line 7:
	Event-B has no let construct whatsoever.		Event-B has no let construct whatsoever.

	=== ~~Nightly Builds~~ ===		=== ProB's Extended Syntax ===

	~~ProB nightly builds for~~ version '''1.6.1-beta''' ~~support, since the~~ 28th of April 2016, the use of the <tt>LET</tt> substitution syntax in expressions and predicates.		Since version '''1.6.1-beta''' (28th of April 2016), ProB supports the use of the <tt>LET</tt> substitution syntax in expressions and predicates.

	==== Examples: ====		==== Examples: ====
Line 65:		Line 65:
	=== Nightly Builds ===		=== Nightly Builds ===

	~~ProB nightly builds for~~ version '''1.6.1-beta''' ~~support, since the~~ 28th of April 2016, the use of the <tt>LET</tt> substitution syntax in expressions and predicates.		Since version '''1.6.1-beta''' (28th of April 2016), ProB supports the use of the <tt>LET</tt> substitution syntax in expressions and predicates.

	==== Examples: ====		==== Examples: ====

Bivab at 14:28, 6 June 2016

2016-06-06T14:28:04Z

@@ Line 12: / Line 12: @@
 ==== Examples: ====
   >>> LET a BE a = 10 IN a + 10 END
@@ Line 64: / Line 63: @@
 Classical B only has an IF-THEN-ELSE substitution (aka statement), no such construct for predicates or expressions.
 The following construct
   %((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0)

Bivab: /* Examples: */

2016-06-06T14:23:20Z

Examples:

← Older revision		Revision as of 14:23, 6 June 2016
Line 29:		Line 29:
	Predicate is TRUE		Predicate is TRUE

			>>> LET a, b BE a = 10 & b = 1 IN a + b END
			Expression Value = 11

	=== Let for predicates ===		=== Let for predicates ===

Bivab: /* Let */

2016-06-06T14:20:44Z

Let

@@ Line 6: / Line 6: @@
 Classical B only has a LET substitution, no let construct for predicates or expressions.
 Event-B has no let construct whatsoever.
 === Let for predicates ===

Michael Leuschel: /* If-Then-Else */

2016-06-01T05:54:08Z

If-Then-Else

← Older revision		Revision as of 05:54, 1 June 2016
Line 42:		Line 42:
	%((x).(x=0 & PRED\|C1)\/%(x).(x=0 & not(PRED)\|C2)) (0)		%((x).(x=0 & PRED\|C1)\/%(x).(x=0 & not(PRED)\|C2)) (0)
	encodes an if-then-else for expressions:		encodes an if-then-else for expressions:
	if PRED ~~then~~ C1 ~~else~~ C2		IF PRED THEN C1 ELSE C2 END

	It is recognised by ProB.		The former lambda-construct is recognised by ProB and replaced internally by an if-then-else construct.
			The latter syntax is actually now recognised as well by ProB 1.6 (version 1.6.0 still requires parentheses around the IF-THEN-ELSE; version 1.6.1 no longer requires them).

	== finite ==		== finite ==

Michael Leuschel: /* map */

2016-06-01T05:50:46Z

map

← Older revision		Revision as of 05:50, 1 June 2016
Line 56:		Line 56:

	== map ==		== map ==
	Given a function f and a sequence s one can map the function over all elements of s using the relational composition operator <tt>;</tt>:		Given a function f and a sequence <tt>sqce</tt> one can map the function over all elements of <tt>sqce</tt> using the relational composition operator <tt>;</tt>:
	(s ; f)		(sqce ; f)

	For example, <tt>([1,2,3] ; succ)</tt> gives us the sequence <tt>[2,3,4]</tt>.		For example, <tt>([1,2,3] ; succ)</tt> gives us the sequence <tt>[2,3,4]</tt>.

Bivab at 14:04, 31 May 2016

2016-05-31T14:04:52Z

← Older revision		Revision as of 14:04, 31 May 2016
Line 82:		Line 82:
	Observe that, even though <tt>closure1(step)</tt> is an infinite relation, ProB can compute the relational image of <tt>closure1(step)</tt> for a particular set such as		Observe that, even though <tt>closure1(step)</tt> is an infinite relation, ProB can compute the relational image of <tt>closure1(step)</tt> for a particular set such as
	<tt>{({4,5,2},[])}</tt> (provided the recursion terminates).		<tt>{({4,5,2},[])}</tt> (provided the recursion terminates).

			== Recursion using <tt>ABSTRACT_CONSTANTS</tt> ==

			Recursive functions can be declared using the <tt>ABSTRACT_CONSTANTS</tt> section in B machines. Functions declared as <tt>ABSTRACT_CONSTANTS</tt> are treated symbolically by ProB and not evaluated eagerly.

			For example, to sort a set of integers into a ascending sequence, as above, we would define a recursive function as follows:
			ABSTRACT_CONSTANTS
			Recursive_Sort
			PROPERTIES
			Recursive_Sort : POW(INTEGER) <-> POW(INTEGER*INTEGER)
			& Recursive_Sort =
			%in.(in : POW(INTEGER) & in = {} \| [])
			\/ %in.(in : POW(INTEGER) & in /= {}
			\| min(in) -> Recursive_Sort(in\{min(in)}))

			By defining <tt>Recursive_Sort</tt> as an abstract constant we indicate that ProB should handle the function symbolically, i.e. ProB will not try to enumerate all elements of the function. The recursive function itself is composed of two single functions: a function defining the base case and a function defining the recursive case. Note, that the intersection of the domains of these function is empty, and hence, the union is still a function.

Michael Leuschel: /* Let for predicates */

2016-02-03T08:42:20Z

Let for predicates

← Older revision		Revision as of 08:42, 3 February 2016
Line 18:		Line 18:
	corresponds to something like		corresponds to something like
	{x\|let y=E in P}		{x\|let y=E in P}

			One can also use the ran operator or introduce multiple lets in one go:
			dom(dom({x,y,z\|y=E1 & z=E2 &P}))
			or
			ran({y,z,x\|y=E1 & z=E2 &P})
			both encode
			{x\|let y=E1 & z=E2 in P}

	=== Let for expressions ===		=== Let for expressions ===

Michael Leuschel: /* Let for expressions */

2016-02-03T08:40:24Z

Let for expressions

← Older revision		Revision as of 08:40, 3 February 2016
Line 22:		Line 22:

	In case F is a set expression, then the following construct can be used to encode a let statement:		In case F is a set expression, then the following construct can be used to encode a let statement:
	#UNION(x).(x=E\|F)		UNION(x).(x=E\|F)
	corresponds to something like		corresponds to something like
	let x=E in F		let x=E in F

	The following construct has exactly the same effect:		The following construct has exactly the same effect:
	#INTER(x).(x=E\|F)		INTER(x).(x=E\|F)

	== If-Then-Else ==		== If-Then-Else ==

Michael Leuschel: /* If-Then-Else */

2016-02-03T08:40:05Z

If-Then-Else

← Older revision		Revision as of 08:40, 3 February 2016
Line 32:		Line 32:

	Classical B only has an IF-THEN-ELSE substitution (aka statement), no such construct for predicates or expressions.		Classical B only has an IF-THEN-ELSE substitution (aka statement), no such construct for predicates or expressions.
			The following construct
	%((x).(x=0 & PRED\|C1)\/%(x).(x=0 & not(PRED)\|C2)) (0)		%((x).(x=0 & PRED\|C1)\/%(x).(x=0 & not(PRED)\|C2)) (0)
	encodes		encodes an if-then-else for expressions:
	if PRED then C1 else C2		if PRED then C1 else C2

			It is recognised by ProB.

	== finite ==		== finite ==