Specification of loop assigns Virgile Prevosto on 6 October 2010
A simple example Broadly speaking, every location which is not mentioned in such a clause should have the same value when exiting the corresponding code as it when entering it. For instance, if we take the following declaration (extracted from ACSL by Example) /*@ assigns \ othing; */ bool equal(const...
Read More