verification of existential quantifier

Mar 23, 2011 at 7:29 PM

For universal quantifier, we know we can use:

e.g. forall( unsigned k; k<max; f(k)== true) for specification contracts


How can we do so in case of existential quantifier?

for e.g. for some unsigned x; x<10; f(x) is true.


Mar 23, 2011 at 7:35 PM


  in addition to forall() there is also exists() with the same syntax as forall().

  Hope that helps, Mark

Mar 23, 2011 at 10:55 PM