Tutorial Debugging Well-Definedness and Transition Errors - Revision history

Michael Leuschel at 08:34, 18 November 2015

2015-11-18T08:34:06Z

← Older revision		Revision as of 08:34, 18 November 2015
Line 2:		Line 2:
	[[Category:User Manual]]		[[Category:User Manual]]

	We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].		We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]]. You may also want to have a look at the explanation of [[Well-Definedness_Checking\|well-definedness in B]].

	== A simple example ==		== A simple example ==

Michael Leuschel at 08:32, 18 November 2015

2015-11-18T08:32:55Z

← Older revision		Revision as of 08:32, 18 November 2015
Line 40:		Line 40:

	The same technique applies for inspecting other transition errors, such as:		The same technique applies for inspecting other transition errors, such as:
	* arithmetic well-definedness errors (division by 0, modulo by 0, modulo for negative numbers, min or max of empty set)		* [[Well-Definedness_Checking\|well-definedness errors]] of expressions such as:
	* functional well-definedness errors (function applied outside of domain or applied to relation,...)		** arithmetic well-definedness errors (division by 0, modulo by 0, modulo for negative numbers, min or max of empty set)
	* sequence well-definedness errors (first, last, tail, front of empt sequence,...)		** functional well-definedness errors (function applied outside of domain or applied to relation,...)
			** sequence well-definedness errors (first, last, tail, front of empt sequence,...)
	* PRE condition errors (not for outermost preconditions, which are treated specially)		* PRE condition errors (not for outermost preconditions, which are treated specially)
	* ASSERT condition violations		* ASSERT condition violations

Michael Leuschel at 15:36, 25 July 2011

2011-07-25T15:36:18Z

← Older revision		Revision as of 15:36, 25 July 2011
Line 38:		Line 38:

	[[file:ProB_While_INV_Violation.png\|200px\|center]]		[[file:ProB_While_INV_Violation.png\|200px\|center]]

			The same technique applies for inspecting other transition errors, such as:
			* arithmetic well-definedness errors (division by 0, modulo by 0, modulo for negative numbers, min or max of empty set)
			* functional well-definedness errors (function applied outside of domain or applied to relation,...)
			* sequence well-definedness errors (first, last, tail, front of empt sequence,...)
			* PRE condition errors (not for outermost preconditions, which are treated specially)
			* ASSERT condition violations

Michael Leuschel at 15:33, 25 July 2011

2011-07-25T15:33:02Z

← Older revision		Revision as of 15:33, 25 July 2011
Line 37:		Line 37:
	Sometimes you can also have the possibility to click on a "Visualise" button, which in this case will give you a graphical visualisation of the invariant violation:		Sometimes you can also have the possibility to click on a "Visualise" button, which in this case will give you a graphical visualisation of the invariant violation:

	[[file:ProB_While_INV_Violation.png\|~~600px~~\|center]]		[[file:ProB_While_INV_Violation.png\|200px\|center]]

Michael Leuschel: Created page with 'Category:Tutorial Category:User Manual We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phas…'

2011-07-25T15:29:47Z

Created page with 'Category:Tutorial Category:User Manual We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phas…'

New page

[[Category:Tutorial]]
[[Category:User Manual]]

We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]], and have understood why animation is difficult as outlined in [[Tutorial Understanding the Complexity of B Animation]].

== A simple example ==

Let us use the following B machine as starting point:
<pre>
MACHINE WhileLoopInvariantError
VARIABLES xx
INVARIANT
xx:NATURAL
INITIALISATION xx:=1
OPERATIONS
Set(c) = PRE c:1..10 & xx<=c THEN
WHILE xx < c DO xx := xx+1
INVARIANT
xx <= c & xx:NATURAL &
xx<10 /* this is wrong */
VARIANT c-xx
END
END;
r <-- Get = BEGIN r:= xx END
END
</pre>

After loading and initialising the machine you see that ProB has found a so-called "transition error", i.e., an error that occured while computing enabled operations (which correspond to a transition from one state to the B machine to another). These errors are displayed in red in the State Properties pane:

[[file:ProB_WhileAfterLoad.png|600px|center]]

When you click on the red transition error you get presented with more details about the error:

[[file:ProB_WhileAfterErrClick.png|600px|center]]

Sometimes you can also have the possibility to click on a "Visualise" button, which in this case will give you a graphical visualisation of the invariant violation:

[[file:ProB_While_INV_Violation.png|600px|center]]