search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Non-determinism in ACSL #15

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

Is there a need for a non-deterministic constructor such as \any T x; P(x)?

pbaudin commented 6 years ago

The construct \any T x ; P(x) is similar to let x of type T such that P(x) in x.

As far as I can remember, the answer was definitely no because this construct is not part of the first order logic. We wanted to have t==t being true for any term t. That may not be the case for the equality ( \any T x; P(x)) == ( \any T x; P(x)).