eiffel: a statement for explicitly executing code when assertions are on

Question

Sometimes the checks and contract constructions need an elaboration which wants to be avoided when assertions removed to improve performances and avoid doing useless things with the "only" work of the compiler. I refer for ex. to job in loops checks or other things. Sometimes having to build a function or having to think how to build it without being executed when assertions are on goes away of the intuitive way of the contract and its sense. I refer particularly to the check structure

Is there a way to do something such as

if checks_are_enabled then do check stuff here end do_some_normal_job if checks_are_enabled then do other check stuff here end

Can you give a somewhat realistic example, specifically what isn't working? — U. Windl
– U. Windl, Commented May 24, 2021 at 16:21

Alexander Kogtenkov · Accepted Answer · 2020-08-11 10:46:52Z

Assertions can be turned on and off on a class-by-class basis, with different levels: preconditions, postconditions, invariants, etc. As a result, it would be tricky and unreliable to report when they are enabled or not (consider, for example, inherited code: the checks might be on in one case and off in another). On a methodological level it would also break the idea that a correct program works the same way regardless of assertion monitoring.

What are workarounds?

If assertions are complex, they can be factored out to dedicated queries and look like
```
check is_valid: complex_query end 
```
An alternative is to use debug statements:
```
debug ("check_this", "check_that") ... some complex code, including assertions end 
```
where "check_this" and "check_that" are debug keys that can be turned on when compiling for debugging.

There are hacks that could work now, but not in the future:

If a complex state needs to be computed and then checked after some operation, it can be saved in an object passed to some function with complex calculations and used later again:

check is_valid_before: valid_pre (state) -- The state is computed by `valid_pre`. end code_that_does_the_work check is_valid_after: valid_post (state) -- The state is checked by `valid_post`. end

Some global flag can be used to keep track about assertion monitoring:

check is_monitoring_checks end

where query is_monitoring_checks has side effects:

is_monitoring_checks: BOOLEAN -- Record whether assertion checks are turned on. do is_check_on := True Result := True end

Then, subsequent code could be written as asked in the question:

 if is_check_on then ... -- Do some complex calculations when assertions are turned on. end

Collectives™ on Stack Overflow

eiffel: a statement for explicitly executing code when assertions are on

1 Answer 1

Comments

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Related