Algorithms and correctness - Revision history

Weihe: /* Invariant */

2016-04-28T12:49:57Z

Invariant

← Older revision		Revision as of 12:49, 28 April 2016
Line 54:		Line 54:

	'''Remarks:'''		'''Remarks:'''
			# Typically, an invariant assertion is ''parameterized'', for example:
			## in case of an iteration: usually by the number of iterations performed so far;
			## in case of a recursion: the recursion depth or a dynamically changing value in the auxiliary data (e.g. the length of a sequence).
	# If an algorithm only accesses its input and its own local data, the invariant assertions are assertions about its input and these local data and nothing else.		# If an algorithm only accesses its input and its own local data, the invariant assertions are assertions about its input and these local data and nothing else.
	# The invariant of an algorithm has a specific function in the [[#Correctness proofs\|correctness proof]] for the algorithm. Typically, in a documentation, only those invariant assertions are stated that are relevant for this purpose.		# The invariant of an algorithm has a specific function in the [[#Correctness proofs\|correctness proof]] for the algorithm. Typically, in a documentation, only those invariant assertions are stated that are relevant for this purpose.

Weihe: /* Correctness proofs */

2016-04-28T11:57:25Z

Correctness proofs

← Older revision		Revision as of 11:57, 28 April 2016
Line 82:		Line 82:

	'''Caveat:'''		'''Caveat:'''
	Quite frequently, validity of the invariant for the state immediately before the first iteration is based on a separate definition of the "null case". For example, the empty sum (sum over no summands) is 0 by definition, the product is 1, the faculty of 0 is 1, the 0-th power of a number is 1, etc. To be on the safe side in such a case, the particular induction step from 0 to 1 should be checked separately.		Quite frequently, validity of the invariant for the state immediately before the first iteration is based on a separate definition of the "null case". For example, the empty sum (sum over no summands) is 0 by definition, the empty product is 1, the faculty of 0 is 1, the 0-th power of a number is 1, etc. To be on the safe side in such a case, the particular induction step from 0 to 1 should be checked separately.

	'''Remarks:'''		'''Remarks:'''

Weihe: /* Correctness proofs */

2016-04-28T11:56:53Z

Correctness proofs

← Older revision		Revision as of 11:56, 28 April 2016
Line 80:		Line 80:
	## Proving the induction basis amounts to proving that the preprocessing (initialization) establishes the invariant.		## Proving the induction basis amounts to proving that the preprocessing (initialization) establishes the invariant.
	## Proving the induction step amounts to proving that an iteration / a recursive call maintains the invariant.		## Proving the induction step amounts to proving that an iteration / a recursive call maintains the invariant.

			'''Caveat:'''
			Quite frequently, validity of the invariant for the state immediately before the first iteration is based on a separate definition of the "null case". For example, the empty sum (sum over no summands) is 0 by definition, the product is 1, the faculty of 0 is 1, the 0-th power of a number is 1, etc. To be on the safe side in such a case, the particular induction step from 0 to 1 should be checked separately.

	'''Remarks:'''		'''Remarks:'''

Weihe: /* Invariant */

2016-04-28T11:56:31Z

Invariant

← Older revision		Revision as of 11:56, 28 April 2016
Line 52:		Line 52:
	# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.		# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.
	# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately before '''or''' after each recursive call (see [[#Induction in case of a recursion\|below]]). These assertions are called the '''invariant assertions''' of this recursion.		# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately before '''or''' after each recursive call (see [[#Induction in case of a recursion\|below]]). These assertions are called the '''invariant assertions''' of this recursion.

	~~'''Caveat:'''~~
	Quite frequently, validity of the invariant for the state immediately before the first iteration is based on a separate definition of the "null case". For example, the empty sum (sum over no summands) is 0 by definition, the product is 1, the faculty of 0 is 1, the 0-th power of a number is 1, etc. To be on the safe side in such a case, the particular induction step from 0 to 1 should be checked separately.

	'''Remarks:'''		'''Remarks:'''

Weihe: /* Invariant */

2016-04-28T11:56:14Z

Invariant

← Older revision		Revision as of 11:56, 28 April 2016
Line 52:		Line 52:
	# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.		# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.
	# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately before '''or''' after each recursive call (see [[#Induction in case of a recursion\|below]]). These assertions are called the '''invariant assertions''' of this recursion.		# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately before '''or''' after each recursive call (see [[#Induction in case of a recursion\|below]]). These assertions are called the '''invariant assertions''' of this recursion.

			'''Caveat:'''
			Quite frequently, validity of the invariant for the state immediately before the first iteration is based on a separate definition of the "null case". For example, the empty sum (sum over no summands) is 0 by definition, the product is 1, the faculty of 0 is 1, the 0-th power of a number is 1, etc. To be on the safe side in such a case, the particular induction step from 0 to 1 should be checked separately.

	'''Remarks:'''		'''Remarks:'''

Weihe: /* Invariant */

2016-04-27T11:08:14Z

Invariant

← Older revision		Revision as of 11:08, 27 April 2016
Line 51:		Line 51:

	# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.		# The '''invariant''' of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the '''invariant assertions''' of this loop.
	# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately after each recursive call. These assertions are called the '''invariant assertions''' of this recursion.		# The '''invariant''' of a recursion consists of all assertions that are fulfilled immediately before '''or''' after each recursive call (see [[#Induction in case of a recursion\|below]]). These assertions are called the '''invariant assertions''' of this recursion.

	'''Remarks:'''		'''Remarks:'''

Weihe: /* Induction in case of a recursion */

2016-04-27T06:40:55Z

Induction in case of a recursion

← Older revision		Revision as of 06:40, 27 April 2016
Line 89:		Line 89:
	== Induction in case of a recursion ==		== Induction in case of a recursion ==
	In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:		In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:
	# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].		# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to be ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].
	# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Examples: [[Mergesort\|mergesort]] and [[Quicksort\|quicksort]]; in these examples, the size of the sequence is the induction variable.		# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Examples: [[Mergesort\|mergesort]] and [[Quicksort\|quicksort]]; in these examples, the size of the sequence is the induction variable.

Weihe: /* Induction in case of a recursion */

2016-04-27T06:40:33Z

Induction in case of a recursion

← Older revision		Revision as of 06:40, 27 April 2016
Line 90:		Line 90:
	In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:		In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:
	# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].		# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].
	# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. ~~Example~~: [[Mergesort\|mergesort]] and [[Quicksort\|quicksort]]; in these examples, the size of the sequence is the induction variable.		# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Examples: [[Mergesort\|mergesort]] and [[Quicksort\|quicksort]]; in these examples, the size of the sequence is the induction variable.

Weihe: /* Induction in case of a recursion */

2016-04-27T06:40:23Z

Induction in case of a recursion

← Older revision		Revision as of 06:40, 27 April 2016
Line 90:		Line 90:
	In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:		In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:
	# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].		# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].
	# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Example: [[Mergesort\|mergesort]]; the size of the sequence is the induction variable.		# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Example: [[Mergesort\|mergesort]] and [[Quicksort\|quicksort]]; in these examples, the size of the sequence is the induction variable.

Weihe: /* Induction in case of a recursion */

2016-04-27T06:35:09Z

Induction in case of a recursion

← Older revision		Revision as of 06:35, 27 April 2016
Line 88:		Line 88:

	== Induction in case of a recursion ==		== Induction in case of a recursion ==
	In principle, there are two mutually ways to define the induction. Typically, only one of these two ways is viable:		In principle, there are two, in a sense mutually opposite, ways to define the induction. Typically, only one of these two ways is viable:
	# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].		# The depth of a recursive call is the induction variable; the original call to this subroutine has to ensure the induction basis; the induction step has to ensured by every descent in the recursion tree. Example: [[Binary search\|binary search]].
	# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Example: [[Mergesort\|mergesort]]; the size of the sequence is the induction variable.		# The induction variable is some parameter of the input. The invariant simply says that the output of a recursive call is correct. In a descent in the recursion tree, that parameter must strictly decrease. The recursion anchor must ensure the induction basis. Example: [[Mergesort\|mergesort]]; the size of the sequence is the induction variable.