Now that we have \choose (aka \some)
we can write in a specification case: old T e = (\choose T x; P(x));
which I think would be entirely equivalent to
forall T e;
requires P(e);
and as no one has claimed ever having needed forall, can we simplify matters by dropping it from JML?
Now that we have \choose (aka \some) we can write in a specification case: old T e = (\choose T x; P(x)); which I think would be entirely equivalent to forall T e; requires P(e); and as no one has claimed ever having needed forall, can we simplify matters by dropping it from JML?