[Assignment #5] finding good loop invariant

[brongs2]

Related Issue

No response

Googling Result

https://stackoverflow.com/questions/2935295/what-is-the-best-way-of-determining-a-loop-invariant

ChatGPT Result

https://chatgpt.com/c/66fe4982-506c-8003-abf7-9f09b1ae39bb

Your question here

To find the loop invariant of pascal's triangle
I can observe that elements of new_row is same to comb r k, but this invariant does not pass the test
loop invariant preservation error since my loop invariant is not good invariant
can anyone help what I missing?
thank you

[Jaewookim08]

I can't tell exactly what's wrong just from the description, but here is some general advice:

• Remember that the invariant must always hold at the start of the loop, even if not all elements of new_row have been assigned yet.
• The invariant must carry enough information to ensure that each iteration’s invariant, combined with the loop body code, can be used to prove the invariant for the next iteration.

If you need more help, feel free to provide additional context.

[brongs2]

Thank you for your comment,
I wonder if I need to specify the characteristic of Combination which nCr = n-1Cr-1 + n-1Cr
if it does, then why?
thank you

[Jaewookim08]

I'll have to check, but I'm fairly certain you don't need to since the lemma should already be in the library.

[brongs2]

to induce row[c] = r-1Cc,
suppose row[c] = r-1Cc if new_row[0] =rC0 , new_row[r] = rCr, if 1 <= i < c, then new_row[i] = row[i] + row[i-1], then by lemma, new_row[i] = = r-1Ci + r-1Ci-1 = rCi, so I expect that row[c] = new_row[c] = rCc for all c
then why the machine cannot induce row[c] = rCc?

[Jaewookim08]

The issue was troubleshot during office hours. It was caused by using too few steps when working with www.why3.org/try/.

For all students, try using 1,000 to 5,000 steps if Why3 is not working as expected. I'll add warnings in the instructions.