Объявления на уровне пакета

Эффект вызова функционального параметра непосредственно в месте вызова.

Эффект, описывающий ситуацию, когда после наблюдения другого эффекта функции некоторое условие становится истинным.

Предоставляет область видимости, в которой можно использовать функции DSL контрактов, такие как returns, callsInPlace и т. д., чтобы описать контракт функции.

Представляет эффект вызова функции: непосредственно наблюдаемый, например обычное завершение функции, или побочный эффект, например вызов лямбда-параметра функции непосредственно в месте вызова.

Эта метка обозначает экспериментальный API для объявления контрактов и используется для явного включения этой возможности при объявлении контрактов пользовательских функций.

Эта метка обозначает экспериментальный API для объявления расширенных контрактов и используется для явного включения этой возможности при объявлении расширенных контрактов пользовательских функций.

Описывает ситуацию, когда заданное условие гарантированно истинно в теле функционального параметра.

Указывает, сколько раз функция вызывает свой функциональный параметр непосредственно в месте вызова.

Описывает ситуацию, когда функция завершается обычным образом с заданным возвращаемым значением.

Описывает ситуацию, когда функция завершается обычным образом с любым ненулевым возвращаемым значением.

Эффект, который можно наблюдать после вызова функции.

Задает контракт функции.