Example application of a "forall"

This is an example application of a forall extension that I ran across:
 
property p = always(a -> (prev(b,N) ||
   prev(b,N+1) ||
   prev(b, N+2) ||
     ...
   prev(b, M)));
 
The user would like to use a forall construct and, make this into
a parameterized property and pass in N, M etc.
 
(I mentioned this example in the extensions meeting yesterday)
Received on Wed Nov 24 08:50:46 2004