In computer science, a loop variant is a mathematical function defined on the state space of a computer program having the property that each iteration of a loop strictly decreases its value with respect to a well-founded relation. A loop variant is used to prove the termination of a while loop in a computer program by well-founded descent. (See also, pp. 32–33, 174–176. ) A basic property of a well-founded relation is that it has no infinite descending chains.

PropertyValue
dbpprop:abstract
  • In computer science, a loop variant is a mathematical function defined on the state space of a computer program having the property that each iteration of a loop strictly decreases its value with respect to a well-founded relation. A loop variant is used to prove the termination of a while loop in a computer program by well-founded descent. (See also, pp. 32–33, 174–176. ) A basic property of a well-founded relation is that it has no infinite descending chains. Therefore a loop possessing a variant will terminate after a finite number of iterations, as long as its body terminates each time. A while loop, or, more generally, a computer program that may contain while loops, is said to be totally correct if it is partially correct and it terminates.
dbpprop:reference
rdfs:comment
  • In computer science, a loop variant is a mathematical function defined on the state space of a computer program having the property that each iteration of a loop strictly decreases its value with respect to a well-founded relation. A loop variant is used to prove the termination of a while loop in a computer program by well-founded descent. (See also, pp. 32–33, 174–176. ) A basic property of a well-founded relation is that it has no infinite descending chains.
rdfs:label
  • Loop variant
skos:subject
foaf:page