Is

contract

in this function correct?

I would say no, since the conversation may fail and the block may not be executed. I would make it "at most once", if there is such an option.

@Arkadii Ivanov The compiler know that any

block

might throw and doesn't assume it'd succeed, regardless of the contract. You can check the behavior by having an expression evaluating to

Nothing

in the passed block. You can also check

also

, and that applies to

apply

, let alone

let

which works the same way as well, with

with

too. All these implementations have such a contract, and you can throw from the passed lambda.

Right, but in this particular case it's not the

block

throws, but the function invocation prior

block

execution.

The important thing here is that if the function completes normally, it implies that

block

was executed once, which is in agreement with this contract.

@ilya.gorbunov so that contract is correct?

I understand what you mean @Arkadii Ivanov, now as @ilya.gorbunov said, I think it doesn't matter since the function doesn't return normally in this case (it catches an exception but throws back another one), so the compiler can still make the assumptions it makes based on the contract and let you write code around it like assigning `val`s in the

block

without breaking the code in any way.

I missed that point that function rethrows the exception. In this case the contract looks correct.