bearophile wrote:
But simple asserts sometimes are not enough to test more complex things. So other more serious contract systems allow for asserts that contain forall, max, min, sets, and few more simple things, this is an example from a system for Java:/*@ assert (\forall int i; 0 <= i && i < n; a[i] != null);
This does not make it simpler, it just makes things more complicated by now having two ways to do a foreach.
