1
Vote

violation of declaration-quantification duality

description

Consider the following two fragments:

{
T x;
_(assert p)
}

vs

_(assert \forall T x; p)

Assuming that T is a type not requiring initialization (e.g. \integer) I believe it should be a principle that these should be equivalent. Sadly, they're not; there are cases where the first verifies and the second does not.

comments