Answers.Body: <p>Do it in code, so that pupils can play with it. This code will throw an exception if the invariant is not met. Show how this can be useful in finding bugs in the program.</p>
  
  <p>The book a touch of class by Bertrand Meyer, is very good for teaching Object Oriented Programming and has examples (can't remember how many, but it is where I leant it).</p>
  
  <pre><code>loop_example is
     −− A loop example...
     local
        count: INTEGER
     do
        from
           count := 1
        invariant
           count &gt;= 1
           count &lt;= 101
        variant
           101 − count
        until
           count &gt; 100
        loop
           io.put_integer (count)
           io.put_new_line
           count := count + 1
        end -- loop
    end -- method
  </code></pre>
  
  <p>The book has the philosophy that exceptions are only used for program bugs. variance, invariance, preconditions, and post conditions. Everything else should be checked traditionally. You will be surprised at how much simpler this makes things. You hardly ever see or use a catch clause. The philosophy makes it easy to get things right: if you forget to check an input, or have an out by one error, then the program will tell you that you have a bug, and tell you where it is.</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-08T08:09:01.420Z
Answers.LastActivityDate: 2017-07-08T08:09:01.420Z
Answers.UserDisplayName: ctrl-alt-delor
Answers.Body: <p>Let's start with the term "Loop Invariance". It is a property of a loop that is true before and after each iteration, thus in-variant, non-changing. So then, what is the <i>purpose</i> of the loop invariance in proving algorithm correctness? That is, it is a predicate about what the loop is supposed to do. Thus with proof by induction on this predicate shows the correctness of this algorithm. I know this is still very theory heavy so let's break this down even more.</p>
  
  <p>A simple insertion sort. The <i>purpose</i> of insertion sort is to sort an array. Therefore the loop invariance would be that after each i-th iteration, the array is sorted up to the i-th element. The magic here is that instead of looking at the nested for i, j, loops of the algorithm you are choosing the loop invariance that contributes to the goal of the algorithm.</p>
  
  <p>To answer (1). There is no sure guarenteed way to choose the correct loop invariance unless you are very experienced in algorithm correctness through countless examples. The best approach is to choose the segment of code that is actually doing what the algorithm is trying to do. Such as the example above, sorted up to the i-th element.</p>
  
  <p>(2). I believe this has to do with the proof itself, rather than understanding the loop invariance. Structurally, to prove that the algorithm is correct, you would have to use proof by induction (either simple, or complete) to pove the loop-invariance and the fact that the algorithm actually terminates. Usually proof of termination is a 1 liner, such as when i > array.length, loop will terminate.</p>
  
  <blockquote>
    <p>simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement.</p>
  </blockquote>
  
  <p>I can tell you are very intelligent as this is something only someone who truly understands algorithms and proof of correctness can say. It is actually very difficult for younger students to see this as they are tunnel-visioned by the actual loops in the code instead of the bigger picture. Instead, I think what you are trying to convey is to look for "what part of the code is doing what the algorithm is meant to do"</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-07T17:51:58.587Z
Answers.LastActivityDate: 2017-07-07T17:51:58.587Z
Answers.UserDisplayName: Kaneki
Answers.Body: <p>To give an explanation of this requires a problem in which to frame the discussion. I propose the Dutch National Flag problem, likely first proposed by Dijkstra, but I'm not positive. </p>
  
  <p><strong>I'll pose the problem first and discuss the solution using invariants.</strong>   </p>
  
  <p><strong>The Problem</strong> Taken from The Science of Programming.  </p>
  
  <p>You have an array of n elements. Each element is a color, red, white, or blue. You want to "sort" the array so that all of the low index cells are red, all of the high index sells are blue, with the white cells between them. </p>
  
  <p>The number of tests should be kept to a minimum. Cells may be permuted with swap (only). The algorithm you develop should require only a single pass over the array and be linear time.</p>
  
  <hr>
  
  <p>This answer is in process and will be updated. If you want to try to solve it in the interim, the precondition is that the colors are randomly arranged and the postcondition is as described above: [red*, white*, blue*]</p>
  
  <hr>
  
  <p><strong>Discussion:</strong> There are many ways to develop a loop invariant, as discussed in Gries. One way is to weaken the postcondition. I will use [red*, white*, any*, blue*] as the weakened condition and the loop invariant. Such an array configuration can be described with three variables:  </p>
  
  <pre><code>lastRed  
  index  
  firstBlue  
  </code></pre>
  
  <p>The definition of these is as follows: Every cell from <code>0</code> through <code>lastRed</code> is RED. Every cell from <code>lastRed + 1</code> through <code>index - 1</code> is WHITE. Every cell from <code>lastBlue</code> through the end is BLUE</p>
  
  <p>To establish the invariant prior to the loop:</p>
  
  <pre><code>lastRed = -1;
  index = 0;
  firstBlue = flag.length; // flag is the array variable, initially random. 
  </code></pre>
  
  <p>With these definitions, the invariant is true with the array in state [ any* ].</p>
  
  <p><strong>Solution:</strong> The solution is to run a loop that takes the any* section from "all" to "empty". You can do that either by (a) increasing <code>index</code>, which breaks the invariant, and then re-establishing the invariant, or (b) by decreasing <code>firstBlue</code> and re-establishing. Looking at $flag[index]$ will tell you what to do. Swap two cells as needed. A three case "switch" or equivalent is the body of the loop.</p>
  
  <p>The invariant along with <code>index == firstBlue</code> is the postcondition. Therefore the while loop test condition is <code>index &lt; firstBlue</code> QED</p>
  
  <p>Note that it is a linear pass over the array, but with two variables moving toward each other from the end. Cool as a moose. </p>
  
  <hr>
  
  <p>Note 1: The Science of Programming book has many other ideas for coming up with an invariant. This was just one possibility. The book is well organized around that idea. In general, though, the invariant of a loop <em>emerges</em> somehow from the pre and/or postconditions. </p>
  
  <p>Note 2: It shouldn't take much, after doing this exercise, to convince a student that with four values instead of three it is only a bit harder to "sort" in linear time. Actually, any list/array of values from a finite set can be sorted in linear time. Radix sort works, of course, but so does this. </p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-07T19:43:51.283Z
Answers.Text: @nocomprende. See my final note. It is possible as long as the values are from a finite set. Which is nearly always the case when we sort with a (finite) computer. It is hard to realize infinity, but Buddhism teaches something about that, I think.
Answers.UserDisplayName: Buffy
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-07T17:57:41.277Z
Answers.LastActivityDate: 2017-07-08T00:19:49.947Z
Answers.LastEditDate: 2017-07-08T00:19:49.947Z
Answers.UserDisplayName: Buffy
Answers.Body: <p>Firstly, I believe that if the thought process is clear to <em>you</em>, then going through that process with your students, <strong>out loud</strong>, clearly and slowly, can help them understand what it is that you are trying to convey. </p>
  
  <p>Go through that process for a number of various examples, which show how <em>you</em> decide on a loop invariant in the varying situations (yes, that pun was intended).</p>
  
  <p>Whilst detailing every step in the thought process, you should elaborate on the things that are necessary for a loop invariant to be good. An example of what this means in the case of induction: There's the base case, and that should be relatively easy to understand. Then the hypothesis. From here the "oddities" begin. Go through the inductive step multiple times (it is a <em>loop</em>, after all <code>;)</code>), and show them, explicitly, that the invariant really is <strong>invariant</strong>. A few inductive steps should make it clear how the invariant doesn't change. </p>
  
  <p>From there it would depend on how many befuddled faces are looking at the board. If a relatively large portion of the class didn't grasp it, then repeat (note: this is kind of a loop invariant. You always check the same thing) the inductive steps' explanation. This is also useful to show how the algorithm behaves, because essentially you are debugging it<sup>1</sup>, and so it shows how the invariant dictates the behavior. </p>
  
  <p>I've seen the measure of student understanding of complex concepts being mostly <code>Confused</code> or <code>Understood</code> and there isn't much middle ground. When it looks like most students are less shocked then you can go through the last inductive step ($n-1$) and show how the loop invariant is still true, but it becomes false after going through the last step. This shows how the invariant choice no less than <strong><em>defines</em></strong> the algorithm's behavior.</p>
  
  <hr>
  
  <p><sup>1</sup>Technically you're just executing the code line by line like a computer, but the point of what I said doesn't change.</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-07T17:47:49.717Z
Answers.LastActivityDate: 2017-07-07T17:47:49.717Z
Answers.UserDisplayName: ItamarG3
Answers.Body: <p>At the CS1 level that I teach, I focus a lot on the <em>role</em> and the precise <em>meaning</em> of variables and encourage comments at the point of declaration that attempt to make these clear, especially variables that are involved in loops. Since the meaning of a variable changes as the loop body is executed, we "agree" to use the entry point as the standard point of reference.</p>
  
  <p>This is admittedly not using the post-condition to derive the invariant which in turn would be used (in principle) to derive the code itself; but it helps students understand and check their code, and I hope lays the foundation for any exposure to semi-formal methods they might encounter in the future. Combining the termination condition with the assigned meanings of the variables allows me to make reference to the idea of program proofs. Admittedly, the bottom 2/3 of the class is rather lost there, but the top 1/3 is generally tantalized.</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-06-06T21:36:13.043Z
Answers.LastActivityDate: 2017-06-06T22:01:56.370Z
Answers.LastEditDate: 2017-06-06T22:01:56.370Z
Answers.UserDisplayName: David A.
Answers.Body: <p>A great resource for the instructor to learn the max about invariants is to go to the master. </p>
  
  <p><a href="http://rads.stackoverflow.com/amzn/click/038790641X" rel="nofollow noreferrer">David Gries, The Science of Programming</a></p>
  
  <p>It isn't a book for novice learners, though. But understanding what is in this book will help you a lot in teaching programming via invariants. </p>
  
  <p>He reveals all. He and his son have an undergrad text book also, that might not be quite as deep as this. </p>
  
  <p>In particular, David shows how to develop good invariants from postconditions. </p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2017-07-07T17:10:50.463Z
Answers.LastActivityDate: 2017-07-07T17:58:24.750Z
Answers.LastEditDate: 2017-07-07T17:58:24.750Z
Answers.UserDisplayName: Buffy
Body: <p>This is in line with a <a href="https://cseducators.stackexchange.com/questions/6/teaching-induction-to-prove-the-correctness-of-algorithms">prior question I asked</a> about teaching induction, but this is specific to the loop invariant step.</p>
  
  <p>I have not had great success helping my students see how to choose a loop invariant that will (1) always be correct (ie. actually <em>be</em> a loop invariant) and (2) create the structure that will allow them to actually prove that the algorithm in question will be able to behave correctly.</p>
  
  <p>My personal mental process is simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement.  While this seems to work well enough as an idiosyncratic process for me, it does not translate into a clear thought-process for the students who don't 'get it' naturally.</p>
  
  <p>Does anyone have an idea about how to approach this with students to make it obvious?</p>
  
Comments.ContentLicense: CC BY-SA 3.0
Comments.CreationDate: 2017-06-07T10:46:05.737Z
Comments.Text: (Was an answer, but three separate people complained, so I'll make it a comment instead because I personally find pointers to authoritative sources extremely useful.) Track down a copy of David Gries' book "The Science of Programming". He has many suggestions for developing loop invariants.
Comments.UserDisplayName: Chris Okasaki
Comments.ContentLicense: CC BY-SA 3.0
Comments.CreationDate: 2017-07-07T18:08:42.640Z
Comments.Text: Some languages have `assert` statements that will allow you to express the invariant in code.
Comments.UserDisplayName: Thorbjørn Ravn Andersen
Comments.ContentLicense: CC BY-SA 3.0
Comments.CreationDate: 2017-07-07T19:51:40.110Z
Comments.Text: Whats the plus 100 in the end? how to do that?
Comments.UserDisplayName: Harry
Comments.ContentLicense: CC BY-SA 3.0
Comments.CreationDate: 2017-07-07T19:56:47.223Z
Comments.Text: @Harry That means that I wanted more answers (because I really need a good answer) and that I have put a bounty on it.  Anyone above 75 rep can put a bounty on any question after it has been around for 2 days.  At the end of the week, I will select one of the answers, and that person will receive the +100 reputation.
Comments.UserDisplayName: Ben I.
Tags: <lesson-ideas><cs-theory><induction>
Title: Teaching loop invariant choice
ThreadText: # Teaching loop invariant choice
  
  (Asked by: username_0 on 2017-06-05)
  
  This is in line with a [prior question I asked](https://cseducators.stackexchange.com/questions/6/teaching-induction-to-prove-the-correctness-of-algorithms) about teaching induction, but this is specific to the loop invariant step.
  
  I have not had great success helping my students see how to choose a loop invariant that will (1) always be correct (ie. actually *be* a loop invariant) and (2) create the structure that will allow them to actually prove that the algorithm in question will be able to behave correctly.
  
  My personal mental process is simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement. While this seems to work well enough as an idiosyncratic process for me, it does not translate into a clear thought-process for the students who don't 'get it' naturally.
  
  Does anyone have an idea about how to approach this with students to make it obvious?
  
  **Tags:** lesson-ideas, cs-theory, induction
  
  > **Comments:**
  > **username_1**: (Was an answer, but three separate people complained, so I'll make it a comment instead because I personally find pointers to authoritative sources extremely useful.) Track down a copy of username_8 Gries' book "The Science of Programming". He has many suggestions for developing loop invariants.  
  > **username_2**: Some languages have `assert` statements that will allow you to express the invariant in code.  
  > **username_3**: Whats the plus 100 in the end? how to do that?  
  > **username_0**: @username_3 That means that I wanted more answers (because I really need a good answer) and that I have put a bounty on it.  Anyone above 75 rep can put a bounty on any question after it has been around for 2 days.  At the end of the week, I will select one of the answers, and that person will receive the +100 reputation.  
  
  ---
  
  ## 6 answers
  
  ### Answer by username_5 on 2017-07-07. Score: 6
  
  Let's start with the term "Loop Invariance". It is a property of a loop that is true before and after each iteration, thus in-variant, non-changing. So then, what is the *purpose* of the loop invariance in proving algorithm correctness? That is, it is a predicate about what the loop is supposed to do. Thus with proof by induction on this predicate shows the correctness of this algorithm. I know this is still very theory heavy so let's break this down even more.
  
  A simple insertion sort. The *purpose* of insertion sort is to sort an array. Therefore the loop invariance would be that after each i-th iteration, the array is sorted up to the i-th element. The magic here is that instead of looking at the nested for i, j, loops of the algorithm you are choosing the loop invariance that contributes to the goal of the algorithm.
  
  To answer (1). There is no sure guarenteed way to choose the correct loop invariance unless you are very experienced in algorithm correctness through countless examples. The best approach is to choose the segment of code that is actually doing what the algorithm is trying to do. Such as the example above, sorted up to the i-th element.
  
  (2). I believe this has to do with the proof itself, rather than understanding the loop invariance. Structurally, to prove that the algorithm is correct, you would have to use proof by induction (either simple, or complete) to pove the loop-invariance and the fact that the algorithm actually terminates. Usually proof of termination is a 1 liner, such as when i > array.length, loop will terminate.
  
  > simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement.
  
  I can tell you are very intelligent as this is something only someone who truly understands algorithms and proof of correctness can say. It is actually very difficult for younger students to see this as they are tunnel-visioned by the actual loops in the code instead of the bigger picture. Instead, I think what you are trying to convey is to look for "what part of the code is doing what the algorithm is meant to do"
  
  
  ---
  
  ### Answer by username_6 on 2017-07-07. Score: 4
  
  To give an explanation of this requires a problem in which to frame the discussion. I propose the Dutch National Flag problem, likely first proposed by Dijkstra, but I'm not positive.
  
  **I'll pose the problem first and discuss the solution using invariants.**
  
  **The Problem** Taken from The Science of Programming.
  
  You have an array of n elements. Each element is a color, red, white, or blue. You want to "sort" the array so that all of the low index cells are red, all of the high index sells are blue, with the white cells between them.
  
  The number of tests should be kept to a minimum. Cells may be permuted with swap (only). The algorithm you develop should require only a single pass over the array and be linear time.
  
  ---
  
  This answer is in process and will be updated. If you want to try to solve it in the interim, the precondition is that the colors are randomly arranged and the postcondition is as described above: [red\*, white\*, blue\*]
  
  ---
  
  **Discussion:** There are many ways to develop a loop invariant, as discussed in Gries. One way is to weaken the postcondition. I will use [red\*, white\*, any\*, blue\*] as the weakened condition and the loop invariant. Such an array configuration can be described with three variables:
  
  ```
  lastRed  
  index  
  firstBlue  
  
  ```
  
  The definition of these is as follows: Every cell from `0` through `lastRed` is RED. Every cell from `lastRed + 1` through `index - 1` is WHITE. Every cell from `lastBlue` through the end is BLUE
  
  To establish the invariant prior to the loop:
  
  ```
  lastRed = -1;
  index = 0;
  firstBlue = flag.length; // flag is the array variable, initially random. 
  
  ```
  
  With these definitions, the invariant is true with the array in state [ any\* ].
  
  **Solution:** The solution is to run a loop that takes the any\* section from "all" to "empty". You can do that either by (a) increasing `index`, which breaks the invariant, and then re-establishing the invariant, or (b) by decreasing `firstBlue` and re-establishing. Looking at $flag[index]$ will tell you what to do. Swap two cells as needed. A three case "switch" or equivalent is the body of the loop.
  
  The invariant along with `index == firstBlue` is the postcondition. Therefore the while loop test condition is `index < firstBlue` QED
  
  Note that it is a linear pass over the array, but with two variables moving toward each other from the end. Cool as a moose.
  
  ---
  
  Note 1: The Science of Programming book has many other ideas for coming up with an invariant. This was just one possibility. The book is well organized around that idea. In general, though, the invariant of a loop *emerges* somehow from the pre and/or postconditions.
  
  Note 2: It shouldn't take much, after doing this exercise, to convince a student that with four values instead of three it is only a bit harder to "sort" in linear time. Actually, any list/array of values from a finite set can be sorted in linear time. Radix sort works, of course, but so does this.
  
  > **Comments:**
  > **username_6**: @nocomprende. See my final note. It is possible as long as the values are from a finite set. Which is nearly always the case when we sort with a (finite) computer. It is hard to realize infinity, but Buddhism teaches something about that, I think.  
  
  ---
  
  ### Answer by username_7 on 2017-07-07. Score: 3
  
  Firstly, I believe that if the thought process is clear to *you*, then going through that process with your students, **out loud**, clearly and slowly, can help them understand what it is that you are trying to convey.
  
  Go through that process for a number of various examples, which show how *you* decide on a loop invariant in the varying situations (yes, that pun was intended).
  
  Whilst detailing every step in the thought process, you should elaborate on the things that are necessary for a loop invariant to be good. An example of what this means in the case of induction: There's the base case, and that should be relatively easy to understand. Then the hypothesis. From here the "oddities" begin. Go through the inductive step multiple times (it is a *loop*, after all `;)`), and show them, explicitly, that the invariant really is **invariant**. A few inductive steps should make it clear how the invariant doesn't change.
  
  From there it would depend on how many befuddled faces are looking at the board. If a relatively large portion of the class didn't grasp it, then repeat (note: this is kind of a loop invariant. You always check the same thing) the inductive steps' explanation. This is also useful to show how the algorithm behaves, because essentially you are debugging it1, and so it shows how the invariant dictates the behavior.
  
  I've seen the measure of student understanding of complex concepts being mostly `Confused` or `Understood` and there isn't much middle ground. When it looks like most students are less shocked then you can go through the last inductive step ($n-1$) and show how the loop invariant is still true, but it becomes false after going through the last step. This shows how the invariant choice no less than ***defines*** the algorithm's behavior.
  
  ---
  
  1Technically you're just executing the code line by line like a computer, but the point of what I said doesn't change.
  
  
  ---
  
  ### Answer by username_8 on 2017-06-06. Score: 2
  
  At the CS1 level that I teach, I focus a lot on the *role* and the precise *meaning* of variables and encourage comments at the point of declaration that attempt to make these clear, especially variables that are involved in loops. Since the meaning of a variable changes as the loop body is executed, we "agree" to use the entry point as the standard point of reference.
  
  This is admittedly not using the post-condition to derive the invariant which in turn would be used (in principle) to derive the code itself; but it helps students understand and check their code, and I hope lays the foundation for any exposure to semi-formal methods they might encounter in the future. Combining the termination condition with the assigned meanings of the variables allows me to make reference to the idea of program proofs. Admittedly, the bottom 2/3 of the class is rather lost there, but the top 1/3 is generally tantalized.
  
  
  ---
  
  ### Answer by username_6 on 2017-07-07. Score: 2
  
  A great resource for the instructor to learn the max about invariants is to go to the master.
  
  [username_8 Gries, The Science of Programming](http://rads.stackoverflow.com/amzn/click/038790641X)
  
  It isn't a book for novice learners, though. But understanding what is in this book will help you a lot in teaching programming via invariants.
  
  He reveals all. He and his son have an undergrad text book also, that might not be quite as deep as this.
  
  In particular, username_8 shows how to develop good invariants from postconditions.
  
  
  ---
  
  ### Answer by username_4 on 2017-07-08. Score: 1
  
  Do it in code, so that pupils can play with it. This code will throw an exception if the invariant is not met. Show how this can be useful in finding bugs in the program.
  
  The book a touch of class by Bertrand Meyer, is very good for teaching Object Oriented Programming and has examples (can't remember how many, but it is where I leant it).
  
  ```
  loop_example is
     −− A loop example...
     local
        count: INTEGER
     do
        from
           count := 1
        invariant
           count >= 1
           count <= 101
        variant
           101 − count
        until
           count > 100
        loop
           io.put_integer (count)
           io.put_new_line
           count := count + 1
        end -- loop
    end -- method
  
  ```
  
  The book has the philosophy that exceptions are only used for program bugs. variance, invariance, preconditions, and post conditions. Everything else should be checked traditionally. You will be surprised at how much simpler this makes things. You hardly ever see or use a catch clause. The philosophy makes it easy to get things right: if you forget to check an input, or have an out by one error, then the program will tell you that you have a bug, and tell you where it is.
  
  
  ---
  
  