Function request: Class contracts - require on class level

(Theo) #1

On method level you can check the prerequisites before the method is executed (requires) and the results after the method has executed (ensure).

On Class level, you can only check the results after a method has executed (invariants).
It would be nice to have the possibility to check the prerequisites on class level too (private / public requires).

Example usage scenarios:

  • check if the object has been disposed before executing any method.
  • check if the object is ready to respond to any action (b.e. state not correct because of still executing async code)

(marc hoffman) #2

you can use invariants for that?

(Theo) #3

No, because invariants are executed after a method is executed instead of before.

(marc hoffman) #4

right. but invariants are enforces to always be true. if they were true at the end of one call, they’ll be true before the next one, too?

(Theo) #5

I am not sure if I understand you right …

That is correct.

That is not the case when async code is still running.

A simple example:

  1. call method1 (normal method) - everything is ok
  2. call async method2 - long running method, that sets a flag halfway the execution - as soon as this flag is set, the object is not in a state that it can execute any other method, until this flag has been reset.
  3. call method3 (normal method) while method2 is still running.

With invariants, the flag is only checked when method3 finishes, not before it starts. If the flag has been reset when method3 finishes, there won’t be any assertion. The check should have been done before method3 executes.

(Theo) #6

And with the case of Dispose; the dispose method sets the IsDisposed flag. When I check on it with an invariant, it means that the dispose method itself will fail instead of any method executed after Dispose.

(SH) #7

Good Point actually :face_with_monocle:

(Theo) #8

The discussion has stopped - does this mean No?
In that case: No problem but I like to have an answer.

Function request: Class contracts - default require and ensure for type aliases
(marc hoffman) #9

No decision has been made.

(marc hoffman) #10

Ok, but methods are allowed (and often required) to invalidate invariants while they are running. So anything with threading and overlapped unprotected access to methods that mess with data protected by invariants is probably taking you down a path of pain anyways…

What I could see is, simply enforcing invariants before and after method calls (rather than just after?). how does that sound?

(Fredy Ferrari) #11

I agree with @mh regarding unprotected access. Have to check if an object is disposed or not appears to me like a design flaw.

(Theo) #12

Sounds good.

(RemObjects) #13

Thanks, logged as bugs://80830

(Theo) #14

That’s correct, and that’s why I want to check for it using the class contracts - which are only available in the Debug builds. As I see it, class contracts are there to find the flaws.

(Theo) #15

can you add the option precheck to the invariants?

private invariants
  MyField.Value > 10; precheck; //this check is done before (not after) method execution
  AnotherField = 0; //this check is done after method execution

This would solve all.