What is the best way of determining a loop invariant?

It has already been pointed out that one same loop can have several invariants, and that Calculability is against you. It doesn’t mean that you cannot try.

You are, in fact, looking for an inductive invariant: the word invariant may also be used for a property that is true at each iteration but for which is it not enough to know that it hold at one iteration to deduce that it holds at the next. If I is an inductive invariant, then any consequence of I is an invariant, but may not be an inductive invariant.

You are probably trying to get an inductive invariant to prove a certain property (post-condition) of the loop in some defined circumstances (pre-conditions).

There are two heuristics that work quite well:

  • start with what you have (pre-conditions), and weaken until you have an inductive invariant. In order to get an intuition how to weaken, apply one or several forward loop iterations and see what ceases to be true in the formula you have.
  • start with what you want (post-conditions) and strengthen until you have an inductive invariant. To get the intuition how to strengthen, apply one or several loop iterations backwards and see what needs to be added so that the post-condition can be deduced.

If you want the computer to help you in your practice, I can recommend the Jessie deductive verification plug-in for C programs of Frama-C. There are others, especially for Java and JML annotations, but I am less familiar with them. Trying out the invariants you think of is much faster than working out if they work on paper. I should point out that verifying that a property is an inductive invariant is also undecidable, but modern automatic provers do great on many simple examples. If you decide to go that route, get as many as you can from the list: Alt-ergo, Simplify, Z3.

With the optional (and slightly difficult to install) library Apron, Jessie can also infer some simple invariants automatically.

Related Posts:

  1. What is the difference between range and xrange functions in Python 2.X?
  2. what does +=, -=, *= and /= stand for in Python?
  3. How to iterate over a JavaScript object?
  4. Traverse a list in reverse order in Python
  5. While Loop in Mips (New to Mips)
  6. When to use “while” or “for” in Python
  7. While, Do While, For loops in Assembly Language (emu8086)
  8. Angular 2 Cannot find control with unspecified name attribute on formArrays
  9. python “TypeError: ‘numpy.float64’ object cannot be interpreted as an integer”
  10. Guess a number program with Java
  11. Why does Lua have no “continue” statement?
  12. How do you write code to do factorials in MIPS?
  13. Printing from a declared array in MIPS
  14. For-each over an array in JavaScript
  15. Python – TypeError: ‘int’ object is not iterable
  16. Why there is no do while loop in python
  17. Python – TypeError: ‘int’ object is not iterable
  18. What is a loop invariant?
  19. What is a loop invariant?
  20. Loop through an array in JavaScript
  21. Accessing the index in ‘for’ loops?
  22. Loop through an array in JavaScript
  23. Accessing the index in ‘for’ loops?
  24. Good input validation loop using cin – C++
  25. How to avoid “RuntimeError: dictionary changed size during iteration” error?
  26. How to avoid “RuntimeError: dictionary changed size during iteration” error?
  27. Loop through an array php
  28. Iterate through a HashMap [duplicate]
  29. Loop through an array of strings in Bash?
  30. Iterate through a HashMap [duplicate]
  31. foreach vs someList.ForEach(){}
  32. Pythonic way to combine FOR loop and IF statement
  33. How do I loop through or enumerate a JavaScript object?
  34. Why is using “for…in” for array iteration a bad idea?
  35. Subplot for seaborn boxplot
  36. What is the best way to iterate over a dictionary?
  37. How do I apply the for-each loop to every character in a String?
  38. Correct way of looping through C++ arrays
  39. Java compressing Strings
  40. What is an invariant?
  41. Sentinel while loop for C++
  42. Batch script loop
  43. Emulating a do-while loop in Bash
  44. Exit while loop in Python
  45. What condition does while(true) test? When is it true and false?
  46. Fill array with random numbers within a specified range (C++)
  47. Pythonic way to iterate through a range starting at 1
  48. illegal use of break statement; javascript
  49. What is Innermost loop in imperfectly nested loops?
  50. Loop backwards using indices in Python?
  51. Why does using from __future__ import print_function breaks Python2-style print?
  52. How can I loop through all rows of a table? (MySQL)
  53. simple Haskell loop
  54. Bubble sort algorithm in MIPS
  55. Breaking out of nested loops
  56. Is there a “do … until” in Python?
  57. extended initializer lists only available with
  58. error: ‘for’ loop initial declarations are only allowed in C99 mode [duplicate]
  59. How to break out of jQuery each loop?
  60. Bank Account Java Program
  61. MySQL foreach loop
  62. Iterating over a 2 dimensional python list [duplicate]
  63. Infinite for loops possible in Python?
  64. How would I use a while loop to keep requesting user input
  65. python: restarting a loop
  66. What is a loop invariant?
  67. Iterator Loop vs index loop
  68. how to loop through JSON array in jQuery?
  69. Create a two dimensional string array anArray[2][2]
  70. How to use a Do-while loop that continuously prompts a user?
  71. What is the “right” way to iterate through an array in Ruby?
  72. How do I break out of nested loops in Java?
  73. How to iterate through table in Lua?
  74. do-while loop in R
  75. PHP array printing using a loop
  76. How to make music autoplay and loop in background
  77. Python loop counter in a for loop
  78. Get a Try statement to loop around until correct value obtained
  79. How to loop over something a specified number of times in JSTL?
  80. How to make a Java Main Menu Loop after using a case
  81. Python: Continuing to next iteration in outer loop
  82. Difference between “while” loop and “do while” loop
  83. how to stop a loop arduino
  84. How to enumerate an enum
  85. Exclude Featured Posts in WordPress ‘Recent Posts’ Function

Leave a Comment