00:00:00
so in this lecture in this short video
00:00:03
lecture I'm going to talk about
00:00:05
contracts and uh contracts um I'm going
00:00:08
to start with assertions pre and post
00:00:11
conditions now what's an assertion an
00:00:13
assertion is a statement that's either
00:00:15
true or false so it's a Boolean
00:00:17
expression that we are trying to assert
00:00:20
like for example you can say I want to
00:00:22
try to assert that X is greater than or
00:00:25
equal to zero right here so we may
00:00:27
require that X to be greater than equal
00:00:30
Z and as an assertion here a
00:00:33
precondition for a function for example
00:00:36
we may say that we require at this point
00:00:40
the Y to be greater than equal Zer so we
00:00:43
make sure that the precondition is met
00:00:45
so that function will not have
00:00:47
undesirable outcomes the post condition
00:00:50
means that we
00:00:52
ensures that some condition has come
00:00:55
true at the end of this function so we
00:00:58
there are three things that are
00:00:59
important ass
00:01:00
preconditions and post
00:01:02
conditions now Loops are really
00:01:04
important things in programming we write
00:01:07
a loop to iterate over a set of
00:01:09
statements again and again and again now
00:01:11
one of the things we need to assure that
00:01:14
the loop will terminate and also the
00:01:16
loop will produce the desired output
00:01:19
these two things are really really
00:01:22
important now so in order to get there
00:01:25
we will start with a concept called a
00:01:28
loop invariant so what is is a loop
00:01:30
invariant a loop invariant is a Boolean
00:01:33
statement that is true at the start of
00:01:35
the loop that's true one time in the
00:01:37
beginning and then at the end of each
00:01:39
iteration this means that the loop
00:01:41
invariant must be true immediately after
00:01:44
you exit the loop so why do we study
00:01:47
Loop invariance we study Loop invariance
00:01:49
to prove properties of loops and that
00:01:52
will allow us to prove the partial
00:01:54
correctness of loops and what the loops
00:01:56
will produce what the outcome is and
00:01:59
here's an example
00:02:00
so let's take this simple uh loop as an
00:02:03
example let's try to Define some Boolean
00:02:05
statements that may or may not be true
00:02:08
as a loop invariant so we can take a
00:02:11
very trivial one says 1 equals 1 which
00:02:14
is a loop invariant because it never
00:02:15
changes inside the loop so that's great
00:02:18
but it is kind of
00:02:20
useless if you take some statement like
00:02:23
I equals I which is also true inside the
00:02:27
loop because I is part of the loop but
00:02:30
again it's a trivial statement therefore
00:02:32
although it is a loop invariant but
00:02:34
they're not really
00:02:37
useful if you take a statement like I is
00:02:41
strictly less than n is that a loop
00:02:43
invariant let's try to see that we know
00:02:46
that when we start I is equal to zero so
00:02:49
if we assume that n is strictly greater
00:02:51
than zero to begin with this condition
00:02:53
is true what about after one iteration
00:02:57
so I prime is I + 1 can we prove that I
00:03:01
+ 1 is less than strictly less than n
00:03:04
the answer is no therefore this is not a
00:03:07
loop invariant what if I say I is less
00:03:11
than or equal to n well I should be able
00:03:13
to prove this now because in the
00:03:15
beginning I is z if I assume n is
00:03:18
greater than equal to Z as a
00:03:19
precondition then I know this statement
00:03:21
to be true and the I prime which is
00:03:24
equal to I + 1 is now less than or equal
00:03:28
to n since
00:03:30
I is strictly less than n so we did find
00:03:34
a loop invariant called I less than
00:03:37
equal to n now if I take the loop
00:03:39
invariant I is less than or equal to n
00:03:41
which I know is true here outside of the
00:03:43
loop and also the loop exit exit
00:03:46
condition which says I is greater than
00:03:48
or equal to n i can conclude that at the
00:03:52
end of this loop I must be equal to
00:03:56
n now let's how do we find a loop in
00:03:59
variance now this is a process that may
00:04:01
take a while so let's think about this
00:04:03
piece of cord now we do not we do not
00:04:06
know what this does it's some some piece
00:04:09
of cod that is doing something now
00:04:13
obviously we can use something like coin
00:04:15
to figure out given X we can find maybe
00:04:18
we can do a few Explorations what is g
00:04:21
of Z what is g of one what is g of two
00:04:24
and so on we can do that but that
00:04:27
doesn't give us a looping variant that
00:04:29
may give us a hint about what this
00:04:31
function produces so to find a loop
00:04:34
invariant we have to come up with a
00:04:36
statement a Boolean statement that get
00:04:39
involved get involves IGN K perhaps to
00:04:43
come up with a statement that's that we
00:04:45
can prove so there are four things in
00:04:47
this piece of cord x i j and
00:04:52
k now we do know that X is a loop
00:04:55
invariant because X never changes inside
00:04:57
the loop let's start with X to be zero
00:05:01
and we do know that initially I and K
00:05:04
are all zeros now when you go into the
00:05:07
loop the J changes to J + k + 3 I + 1
00:05:12
since J K and I are zero the J will
00:05:15
become one in the first iteration the K
00:05:18
will become k + 6 I + 3 so since K and I
00:05:21
are zero and to begin with K would
00:05:25
become
00:05:26
three and I would be incremented to
00:05:30
1 now in the second iteration of the
00:05:33
loop the J becomes J + K so we will take
00:05:36
1 + 3 that would be 4 3 * I that's 7 + 1
00:05:42
so J would become 8 and K would become k
00:05:45
+ 6 I 3 + 6 I that's 9 + 3 K would
00:05:50
become 12 and the I would become two at
00:05:54
this point the J is greater than x which
00:05:59
is
00:06:59
it's a loop invariant then I must prove
00:07:01
that this is true in the beginning
00:07:04
obviously it is true because I and J and
00:07:06
K are all three are zeros so beginning
00:07:09
one is okay but what about after one
00:07:11
iteration what about I prime Cube now
00:07:14
the I prime is the same as I + 1 because
00:07:17
I changes to i1 and I + 1 Cub is equal
00:07:22
to I Cub + 3 i^ 2 + 3 I +
00:07:28
1 and let's look at J Prime now the J
00:07:31
Prime is equal to uh J + k + 3 I + 1 so
00:07:40
the question we have is can we show that
00:07:44
the I
00:07:46
prime Cub is equal to J Prime uh well at
00:07:51
least I have two terms here 3 I = 3 I
00:07:54
and then 1 = 1 but I'm not really sure
00:07:57
then I also know this I know that this
00:08:00
is true but so if I can prove that K = 3
00:08:04
i^ 2 I will be able to prove this so
00:08:07
let's try to prove K = 3 i² 3 i s as a
00:08:10
loop in variant so to prove that I need
00:08:13
to prove that K Prime is equal to 3 * I
00:08:17
Prime 2 now what is K Prime K Prime is
00:08:20
equal to k + 6 I +
00:08:24
3 and I prime is I + 1
00:08:30
so if I do this then I'll get 3 i^ 2 +
00:08:35
uh 6 I + 3 on this side since K = 3 i^
00:08:40
2 I will get the same thing here so
00:08:44
hence I can prove that therefore that I
00:08:47
prove that this is a looping variant now
00:08:51
both of these are looping variants so I
00:08:53
can confirm that they are Loop
00:08:54
invariance
00:08:56
indeed now so the other problem that we
00:09:00
have is proving the loop termination now
00:09:02
in this case the chode if you look at
00:09:04
the chode that the J eventually because
00:09:08
J is an increasing function must
00:09:11
eventually exceed the X and since J is
00:09:16
always increasing at least by one k is
00:09:19
always increasing at least by three and
00:09:21
I is always increasing at least by one
00:09:24
so we do know that J is going to be
00:09:26
sometime going to go over X so in order
00:09:30
to prove the loop termination we say
00:09:32
that
00:09:33
since uh J
00:09:38
increases okay and the J is going to be
00:09:43
at some point greater than or equal to X
00:09:45
and the loop will terminate at that
00:09:48
point so how do we get the post
00:09:51
condition from the loop inv variant now
00:09:53
Loop invariant post condition now we
00:09:54
have two Loop invariances in this case I
00:09:57
cubal J and K = 3 I 2 now it seems to me
00:10:04
that the loop condition was that while
00:10:08
the J is less than x so it seems to me
00:10:11
that since J is equal to I Cub we are
00:10:16
testing to find the I whose cube is less
00:10:20
than
00:10:21
x and so for example when it's four one
00:10:25
was the I that we got when it it's two
00:10:30
perhaps uh if x was uh something like
00:10:33
nine we might be able to get that the uh
00:10:37
2 CU which is 8 is less than
00:10:40
9 so this is a little bit of uh we'll
00:10:44
leave that discussion for class and uh
00:10:47
we will end this uh video lecture now
