Assume and Assert in Verification Condition Part

Can we assume there will be one assume and one assert expression at most - one at the beginning and at the end ? Or should we consider that there might be assume and assert conditions at the middle of the program?

It doesn’t make a difference how many assumes and asserts there are, assuming you use the rules from the lecture.


This is correct

1 Like