| fun baz(num: Int?, element: MyElement, block: () -> Unit): Int contract [ | |
| callsInPlace(block, InvocationKind.EXACTLY_ONCE), | |
| returns() implies (num != null), | |
| returns() implies (element != null) | |
| ] { | |
| require(num != null) | |
| require(element != null) | |
| block() | |
| if (num >= 0) { | |
| return 1; | |
| } | |
| return 0 | |
| } |