Binary search tree: remove node - Revision history

Weihe: /* Abstract View */

2017-03-03T13:39:53Z

Abstract View

← Older revision		Revision as of 13:39, 3 March 2017
Line 25:		Line 25:

	'''Break condition:''' It is <math>p'</math>.right.right = void.		'''Break condition:''' It is <math>p'</math>.right.right = void.

			'''Remark:''' For example, the height of the subtree rooted at the node to which <math>p</math> points may be chosen as the induction parameter. For conciseness, the induction parameter is omitted in the following.

	== Induction Basis ==		== Induction Basis ==

2015-07-07T16:35:29Z

Induction Step

← Older revision		Revision as of 16:35, 7 July 2015
Line 46:		Line 46:
	## Set <math>p</math>.key := <math>p'</math>.right.key.		## Set <math>p</math>.key := <math>p'</math>.right.key.
	## Set <math>p'</math>.right := <math>p'</math>.right.left.		## Set <math>p'</math>.right := <math>p'</math>.right.left.
	# Terminate the algorithm.		## Terminate the algorithm.
			# Set <math>p':=p'</math>.right.

	'''Correctness:''' Obvious.		'''Correctness:''' Obvious.

2015-07-07T16:34:10Z

Induction Step

← Older revision		Revision as of 16:34, 7 July 2015
Line 40:		Line 40:

	== Induction Step ==		== Induction Step ==
	'''Abstract view:''' If <math>p'</math>.right is the immediate predecessor of <math>K</math>, overwrite <math>K</math> by its immediate predecessor and terminate; otherwise, let <math>p</math> descend one level deeper.		'''Abstract view:''' If <math>p'</math>.right.key is the immediate predecessor of <math>K</math>, overwrite <math>K</math> by its immediate predecessor and terminate; otherwise, let <math>p'</math> descend one level deeper.

	'''Implementation:'''		'''Implementation:'''

2015-06-26T08:08:42Z

Abstract View

← Older revision		Revision as of 08:08, 26 June 2015
Line 20:		Line 20:
	'''Invariant:'''		'''Invariant:'''
	# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.		# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.
	# It is <math>p'</math>.right $\neq$ void.		# It is <math>p'</math>.right <math>\neq</math> void.

	'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right.		'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right.

2015-06-26T08:08:17Z

Abstract View

← Older revision		Revision as of 08:08, 26 June 2015
Line 20:		Line 20:
	'''Invariant:'''		'''Invariant:'''
	# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.		# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.
	# It is <math>p'</math>.right = void.		# It is <math>p'</math>.right $\neq$ void.

	'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right.		'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right.

2015-05-18T14:21:32Z

Induction Step

← Older revision		Revision as of 14:21, 18 May 2015
Line 40:		Line 40:

	== Induction Step ==		== Induction Step ==
	'''Abstract view:''' If <math>p'~~.right~~</math> is the immediate predecessor of ~~'''''~~K~~'''''~~, overwrite ~~'''''~~K~~'''''~~ by its immediate predecessor and terminate; otherwise, let ~~'''''~~p~~''''''~~ descend one level deeper.		'''Abstract view:''' If <math>p'</math>.right is the immediate predecessor of <math>K</math>, overwrite <math>K</math> by its immediate predecessor and terminate; otherwise, let <math>p</math> descend one level deeper.

	'''Implementation:'''		'''Implementation:'''
Line 48:		Line 48:
	# Terminate the algorithm.		# Terminate the algorithm.

	'''Correctness:''' ~~Obvoius~~.		'''Correctness:''' Obvious.

	== Complexity ==		== Complexity ==

2015-05-18T14:20:21Z

Induction Step

← Older revision		Revision as of 14:20, 18 May 2015
Line 43:		Line 43:

	'''Implementation:'''		'''Implementation:'''
	# If <math>p'.right.right = void~~</math>~~:		# If <math>p'</math>.right.right = void:
	## Set <math>p.key := p'.right.key~~</math>~~.		## Set <math>p</math>.key := <math>p'</math>.right.key.
	## Set <math>p'.right := p'.right.left~~</math>~~.		## Set <math>p'</math>.right := <math>p'</math>.right.left.
	# Terminate the algorithm.		# Terminate the algorithm.

2015-05-18T14:18:39Z

Induction Basis

← Older revision		Revision as of 14:18, 18 May 2015
Line 31:		Line 31:

	'''Implementation:'''		'''Implementation:'''
	# If <math>p.left.right = void~~</math>~~:		# If <math>p</math>.left.right = void:
	## Set <math>p.key := p.left.key~~</math>~~		## Set <math>p</math>.key := p.left.key.
	## Set <math>p.left := p.left.left~~</math>~~.		## Set <math>p</math>.left := p.left.left.
	## Terminate the algorithm.		## Terminate the algorithm.
	#Otherwise, set <math>p' := p.left~~</math>~~.		#Otherwise, set <math>p'</math> := p.left.

	'''Proof:''' Obvious.		'''Proof:''' Obvious.

2015-05-18T14:17:17Z

Abstract View

← Older revision		Revision as of 14:17, 18 May 2015
Line 20:		Line 20:
	'''Invariant:'''		'''Invariant:'''
	# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.		# The [[Directed Tree#Immediate Predecessor and Successor\|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes\|range]] of <math>p'</math>.
	# It is <math>p'.right = void~~</math>~~.		# It is <math>p'</math>.right = void.

	'''Variant:''' The pointer <math>p'</math> descends one level deeper to <math>p~~'.right~~</math>.		'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right.

	'''Break condition:''' It is <math>p'.right.right = void~~</math>~~.		'''Break condition:''' It is <math>p'</math>.right.right = void.

	== Induction Basis ==		== Induction Basis ==

2015-05-18T08:32:55Z

General Information

← Older revision		Revision as of 08:32, 18 May 2015
Line 11:		Line 11:
	'''Algorithmic problem:''' See the [[Binary Search Tree#Remark\|remark clause]] of [[Binary Search Tree]]; pointer <math>p</math> as defined there is the input.		'''Algorithmic problem:''' See the [[Binary Search Tree#Remark\|remark clause]] of [[Binary Search Tree]]; pointer <math>p</math> as defined there is the input.

	'''Prerequisites:''' <math>p.left \neq ~~void~~</math>		'''Prerequisites:''' <math>p</math>.left <math>\neq</math> void.

	'''Type of algorithm:''' loop		'''Type of algorithm:''' loop

	'''Auxiliary data:''' A pointer <math>p'</math> of type "pointer to a binary search tree node".		'''Auxiliary data:''' A pointer <math>p'</math> of type "pointer to a binary search tree node of type <math>\mathcal{K}</math>."

	== Abstract View ==		== Abstract View ==