You are using the assignment rule and substitution should be going using bottom up way.
@dennisyakovlev61974 жыл бұрын
Thanks for this video all my teachers skipped this because its "trivial" for them and they just don't understand we don't get it. Really good explanations on both videos!
@beatricesloan27204 жыл бұрын
Thank you very much! This helped a lot
@yashin20685 жыл бұрын
Really thanks ;)
@KANKITHKUMAR4 жыл бұрын
I wanted to verify these thing in VCC(Verifier for Concurrent C). But unfortunately, I'm not able to install VCC on my system. Therefore, I request you to help me to install VCC on my Ubuntu system if you have any idea about this.
@TruongNguyen-qp8hs5 жыл бұрын
excuse me, I don't know that where "P ^ -B" is, and why do you have the statement " a=y" ?
@matthewhennegan8395 жыл бұрын
So P is the invariant (z = a*x), Since we just proved that doesn't change throughout the loop, that must be still true after the loop. The other thing which is true after the loop is the opposite of the loop condition. If we call the loop condition B, then (not) B must be true after the loop. The loop condition was while(a != y) - so we know for sure that after the loop ends, a = y must be true - otherwise we'd still be in the loop. So in summary P ^ -B is the common way of saying that after a while loop, any invariants are still true, and the opposite of the loop condition is true.
@sowmyakudva86495 жыл бұрын
waste of 13 mins!! really annoying when you erase and rewrite..
@matthewhennegan8395 жыл бұрын
You can pause and rewind if you're still having trouble understanding there buddy