assignment 5의 3가지 과제 중 모든 과제에서 나머지 부분은 체크 표시가 뜨면서 문제가 발생하지 않는데, 모두 loop invariant preservation(Unknown)이라는 항목은 물음표가 뜨고, 이 때문에 과제를 하나도 해결할 수 없었습니다. 이 문제를 해결하기 위해 구글링과 gpt를 사용하여 노력해보았지만 자료가 부족하여 해결할 수 없었습니다. 이 문제를 해결할 수 있는 방법을 알고 싶습니다. 또한, assignment05 과제 제출 시 다른 과제와 마찬가지로 제가 직접 수동으로 파일을 압축해서 제출해도 되는지 알고 싶습니다. 감사합니다.
Yes, you can manually create your .zip file, as long as it passes on gg.
"Loop invariant preservation" represents the proof of using the invariant in one iteration to prove the invariant in the next iteration. If Why3 cannot verify this, chances are that your invariant lacks the required information needed for the next iteration.
For your Pascal code in the GPT log, I think your invariants might be missing information for some part of the data.
Related Issue
없음
Googling Result
없음
ChatGPT Result
https://chatgpt.com/share/6707da26-7668-8003-94f9-843d980c6b01
Your question here
assignment 5의 3가지 과제 중 모든 과제에서 나머지 부분은 체크 표시가 뜨면서 문제가 발생하지 않는데, 모두 loop invariant preservation(Unknown)이라는 항목은 물음표가 뜨고, 이 때문에 과제를 하나도 해결할 수 없었습니다. 이 문제를 해결하기 위해 구글링과 gpt를 사용하여 노력해보았지만 자료가 부족하여 해결할 수 없었습니다. 이 문제를 해결할 수 있는 방법을 알고 싶습니다. 또한, assignment05 과제 제출 시 다른 과제와 마찬가지로 제가 직접 수동으로 파일을 압축해서 제출해도 되는지 알고 싶습니다. 감사합니다.