Program Proofs and Loop Invariants

Поділитися
Вставка
  • Опубліковано 12 вер 2024

КОМЕНТАРІ • 32

  • @soobinkim9460
    @soobinkim9460 5 років тому +39

    13:57
    I can relate...

  • @kagame6524
    @kagame6524 9 років тому +4

    Thank you so much David Taylor. You have always had my back since last semester and this semester too!

  • @JohnStanley-s5u
    @JohnStanley-s5u Місяць тому

    When the chapter 2.1-2 problem of CLRS book puzzled me; This video helped me to understand Loop Invariants a lot better.

  • @omarnabil3277
    @omarnabil3277 7 років тому +7

    Amazing!! Love the explanation

  • @maximilliansbabo2099
    @maximilliansbabo2099 7 років тому +5

    I am ignorant and stupid and probably missing the significance this technique offers for later more complicated algorithms, but I cant help but just keep thinking to myself, "....... yeah. Okay?" Still took notes though!!!

    • @DavidTaylorSJSU
      @DavidTaylorSJSU  7 років тому +16

      We spend the first few weeks of class dealing with the tools of program analysis, for correctness proofs and runtime analysis. I don't kid myself to think that students are regularly going to use proofs to prove their programs correct, though perhaps on a rare occasion they will help you to debug in a much better way than "let me just haphazardly change stuff until my test cases work."
      The same sorts of attitude could be taken with lots of studies. Calculus...okay. How often will you use it? For many, not often, but it is just so freaking brilliant anyway.
      So here? We learn the tools. Maybe some of you will use them, maybe some of you won't but these aren't the type of tools that most just learn on their own. We won't use them all semester, but it will help you to understand the book's arguments that its algorithms are correct. That is, if we understand how to use the tools on simple cases, and then the book has a complex use of that tool for a more complex algorithm, we can understand what is being done. Even if you don't want to follow the book step by step, you can look at the big picture to say "Right, here they are proving this section works by loop invariant. I could follow that if I really wanted to spend the time, but just understanding the technique they are using, I know it isn't magical, but I can just skim it right now to see what they are doing, big picture, without worrying about every single line." If you keep at it longer? Then maybe sometime you will want to check out more details, or even do your own for the future, 2023 "Sbabo's Algorithm".

  • @sebascm7278
    @sebascm7278 5 років тому

    Thank you so much this helped me understand a little bit more about invariants

  • @amazinglyclueless8315
    @amazinglyclueless8315 3 роки тому

    I am confused about the loop invariant which is evaluated before the tmp increment in the first iteration (18:27). So, according to the loop invariant in the first iteration before tmp is incremented, the summation of tmpi=1 goes from j=1 to i=1-1=0?

  • @superdupe8
    @superdupe8 9 років тому

    Wow, this is an excellent video! Thank you!

  • @airamae1099
    @airamae1099 3 роки тому

    Thank you Sir David!

  • @londonstudioliving
    @londonstudioliving 3 роки тому +3

    I still don't get it :'(

  • @sherbazh
    @sherbazh 4 роки тому

    You are awesome. Thanks.

  • @multigladiator384
    @multigladiator384 3 роки тому

    Shouldn' it be tmp = the sum from j =1 to i-1 of A[j] ?
    Then the invariant also holds before the first iteration when i = 1(tmp == the sum from j =1 to 0 of A[j] == 0) and after the first iteration when i = 2 (tmp == 0 + the sum from j =1 to 1 of A[j] == A[1])
    That would be the beginning of the induction.
    After that we can state that the invariants holds for all i = i'

  • @Kc-nn8mn
    @Kc-nn8mn 3 роки тому

    this guy is amazing and funny.

  • @unev
    @unev 7 років тому +2

    Thank you, sir. Is it bad that I takes me nearly an hour to watch the 20 minutes long video?

    • @DavidTaylorSJSU
      @DavidTaylorSJSU  7 років тому +3

      If you understood everything in the video, that sounds reasonable.

  • @danielvutran
    @danielvutran 10 років тому

    Great vid!

  • @gunhound45
    @gunhound45 6 років тому

    At 7:25 where did j come from? Shouldn't it be A[i]?

    • @AlgorithmswithAttitude
      @AlgorithmswithAttitude 6 років тому +2

      tmp is the sum of many values. in that comment, j is the dummy variable: tmp is the sum of all A[j] values, where j has the values 1, 2, 3, ... , i.

    • @gunhound45
      @gunhound45 6 років тому

      Algorithms with Attitude ohhh i see. Thanks.

  • @GP9c75
    @GP9c75 5 років тому +3

    Lol, you are definitely not pedagogical minded. but i did learn something

  • @happycode4478
    @happycode4478 4 роки тому

    thanks man

  • @jbipmni8984
    @jbipmni8984 2 роки тому

    do you know loop invariant for this program
    function increment(y)
    comment Return y + 1, where y in N
    x := 0; c:= 1; d:= 1;
    while (y > 0) V (c > 0) do
    a :=y mod 2;
    if a XOR c then x=x+d;
    c:= a AND c;
    d:= 2d; y := [y/2] :
    return(x)

  • @supernerd10000000000
    @supernerd10000000000 7 років тому

    What is the Objective proofs?

    • @DavidTaylorSJSU
      @DavidTaylorSJSU  7 років тому +2

      How do you know if an algorithm correctly solves a problem? Program proofs show that the logic of a program does, in fact, solve the problem the program is supposed to solve. They give a rigorous framework to argue program correctness.

  • @davidreinke9217
    @davidreinke9217 11 років тому +2

    ow = otherwise...

  • @Doctorgeo7
    @Doctorgeo7 11 років тому

    "ow tmp == x"?

  • @WowPlusWow
    @WowPlusWow 4 роки тому

    This guy looks familiar...