I am a beginner of PVS.
Surprisingly, I couldn’t find a way to directly specify
a “while” loop or a “for” loop in PVS. Can anybody give
me an example if you happen to have one?
Thank you very much!