search

kaist-cp / cs220

265 stars 52 forks source link

[Assignment #5] Loop invariant init #385

Open ph1025 opened 1 week ago

ph1025 commented 1 week ago

Related Issue

No response

Googling Result

I cannot find

ChatGPT Result

https://chatgpt.com/share/67029ed8-0cb0-8008-b1d5-f21c32e3e079

Your question here

    let low = ref 0 in
    let high = ref (length a) in
    while !low < !high do
      invariant { 0 <= !low < !high <= length a && 0<length a}...

I execute this code and for loop invariant initialize test, I get "0<length a" works, but "!low < !high" has questioned. I just substituted a variable but why I don't know why "!low < !high" has questioned. Can I get some advice? Thank you.

Jaewookim08 commented 1 week ago

I believe there's a mistake. I tested your code, and 0 < length's loop invariant init is not verified (nor should it be).