Package-level declarations

An effect of calling a functional parameter in place.

An effect of some condition being true after observing another effect of a function.

Provides a scope, where the functions of the contract DSL, such as returns, callsInPlace, etc., can be used to describe the contract of a function.

Represents an effect of a function invocation, either directly observable, such as the function returning normally, or a side-effect, such as the function's lambda parameter being called in place.

This marker distinguishes the experimental contract declaration API and is used to opt-in for that feature when declaring contracts of user functions.

Specifies how many times a function invokes its function parameter in place.

Describes a situation when a function returns normally with a given return value.

Describes a situation when a function returns normally with any non-null return value.

An effect that can be observed after a function invocation.

Specifies the contract of a function.