Merge: Contract: Change mpropdef driving

Merge: Contract: Change mpropdef driving

This pr change the driving strategy to resolve the problem when the static type has no contract and the dynamic has one.

Note: now when a mpropdef has a contract after the introduction a facet is added in the intro class. Indeed, as there is no way to know the dynamic type we are going to meet, we must always direct to the facet of contract even if it only redirects to the method and executes no contract.

I change at the same time the syntax of the keywords `ensures` by `ensure` and `expects` by `expect`. The doc will arrive in the next pr.

Pull-Request: #2799