Add facility to only check a condition if a type binding is finite

[paulch42]

When type bindings are employed, a specification cannot in general be executed by an interpreter. The Runtime tab of the Run Configurations in Overture allows pre-condition, post-condition, invariant etc checks to be turned on or off which allows a specification to be executed even if it has infinite type bindings. Unfortunately, if say invariant checks are turned off, they are turned off for the entire model, preventing checks on invariants that do not have infinite type bindings.

Suggested improvement:
The interpreter through static analysis determines, where type bindings are used, if the range is infinite. If so the check is skipped, if not the check is performed. This would allow the interpreter to perform maximal constraint checking while not discourage the use of type bindings.

Doubt the interpreter can always decide if a type binding is finite or infinite, but in that case err on the side of caution and only perform the check if the interpreter can confirm the type binding has a finite range.

[nickbattle]

Type binds can occur anywhere in a specification, not just in pre/post/inv constraints. So turning off (say) invariant checks may avoid problems with invariants, but type bind executions would still fail in the bodies of functions or operations.

I would be a bit uncomfortable about the tool "passing" constraints that otherwise should fail, simply because it knows that it cannot execute them. I can see that it is similar to turning off pre/post/inv checks, but the side effects may be more insidious - besides, a normal function body that includes a comprehension generated from a type bind has to return something, it cannot "skip" that comprehension or return {} or [] etc.

You're right that, in general, we cannot be statically sure about finiteness. The problem cases are infinite types with invariants that make them finite.

Other views?

[paulch42]

I see, I was only thinking about condition checks outside of the body of a function, without realising the full consequences. I can certainly now see the problems in what I proposed.

[nickbattle]

We can see whether others think it's worth doing anything in this area, but if not, close this issue.

We should note the "feature" (that I didn't know about!) where Overture will allow you to set an integer range specifically to allow integer type binds to return a finite set of values. That worries me too, though it's an interesting approach. It would need to be generalised, if we go this route.

[ldcouto]

I do not support disabling the checks internally. When the user disables the checks or sets an integer bound, they are doing so explicitly and that is the key point, to me.

As for (not) executing type binds, I agree that it's a limitation. There was some work done on connecting the interpreter to a model checker for executing implicit functions. I suppose a similar approach could be tried for type bindings. I'm in favour of any efforts in that direction.

[nickbattle]

I think this idea was effectively rejected, closing.