Kotlin Contracts

[dsavvinov]

This is issue for discussion of the proposal to introduce Kotlin Contracts in language

Pull-request: #140

[Wasabi375]

What proposal?

Edit:
Yeah, now there is a link 😊

[dsavvinov]

@Wasabi375 I've updated op-post -- because pull-request with proposal and corresponding issue mutually reference each other, something (in this case, issue) has to be created with placeholder and then edited later :)

[pakoito]

Is there any existing body of work that implements the same effect system? I wanna check it :D

[pakoito]

Great work on the proposal! It's clear and understandable on scope and implementation. My question is whether these contracts are statically checked, for example would these fail on the compile step:

inline fun <R> run(block: () -> R): R {
    contract {
        callsInPlace(block, InvocationKind.EXACTLY_ONCE)
    }
    val _ignore = block()
    return block()
}

inline fun <R> run(block: () -> R): R {
    contract {
        callsInPlace(block, InvocationKind.EXACTLY_ONCE)
    }
    throw RuntimeExcaption("Boom!")
}

The proposal seems to focus on contract annotation as external information, although nothing prevents the implementor from committing a mistake that breaks the contract.

EDIT: Found it!

Verification of the contracts: how compiler should check if written contract contradicts function's actual semantics?

I'd say the feature is incomplete without this requirement as it opens another door to unsoundness.

EDIT2: I removed an old reply mentioning deprecation and binary compatibility because I missed that this'd be part of metadata and you already solved that issue.

[rjhdby]

fun test() {
    val x: Int
    run {
        // Next line is reported as 'val reassignment', because compiler
        // can't guarantee that lambda won't be invoked more than once
        x = 42
    }

Maybe I say some stupid thing, but why not to allow reassign "val" with same constant value?

[Wasabi375]

This would just mean that the compiler needs to track all known values of any val just to do this. Also this does not help much, because in about 99% of the cases the code is not x = 42 but x = calculateX() instead and you have no way of checking that calculateX() returns the same result every time.

---

What a about contracts for pure functions? That way results of pure functions can be cached if they are called with the same arguments.

[rjhdby]

Contracts may be very userful for DSL description.
For example HTML-DSL

html{
    head{}
    body {}
}

In this case good to have possibility to set constraints for html-lambda body:

1. html-lambda must contains calls of head and body
2. head and body must occurs once

In scope of proporsal it may be looks like:

class Html{
    [dsl(EXACTLY_ONCE|REQUIRED)]
    function head(head:Head.()->Unit){
    }

[dsavvinov]

@pakoito

I'd say the feature is incomplete without as it opens another door to unsoundness.

Indeed, that's why we're going to release contracts in several steps: first as exclusive feature for stdlib (where we have control over what we're writing in contract-section), then, when verification will be ready, we will release it completely, allowing everyone to annotate their functions with contracts.
I'll correct proposal, emphasizing that we treat verification as necessity for the contracts-annotation release.

Is there any existing body of work that implements the same effect system? I wanna check it :D

Do you mean alternative implementations of the proposed effect system, or particular part of Kotlin compiler source code which is responsible for it? If it's the former, then I don't know about similar systems. Proposed one has unique flavor because of Kotlin language specifics: present analyses, namely, smartcasts and sound initialization; pragmatic requirements, such as performance and ability to work well in IDE; etc.

[dsavvinov]

@rjhdby Yes, we're actively researching applications of contracts in DSLs at the moment, but it's too early to announce something specific yet.

[qwwdfsad]

Contracts primarily consider the behavior of methods rather than the properties of values. Properties of values should be handled by the type system rather than contracts.

Could you please clarify this statement? E.g. how a (hypothetical) contract fun List.get(index: Int) { contract { Returns -> index < this.size } } can be expressed in a type system?

fun returns(value: ConstantValue): Effect

So how [Returns -> value == true] can be expressed with this DSL? What ConstantValue should be used?

Binary representation (in Kotlin Metadata) is stable enough and actually is a part of stdlib already

Is it accessible through reflection? Can it be used for e.g. KDoc generation?

Awkward “first-statement” restriction

Is it actually a disadvantage? IMO, it makes everything easier, e.g. you everything know the contract of the method without examining the whole function body.

Contracts are allowed only on functions, which are: Top-level (because inheritance not implemented yet)

Why aren't they allowed on non open functions? How can one write contracts to interfaces with current DSL?

6. Implementation details: are contracts propagated to the call site and can be exploited by the compiler backend? Can I assist compiler in producing more optimized code using contracts?

E.g. can (in the current implementation) K/N compiler possibly eliminate range check in the following code?

inline fun require(value: Boolean): Boolean {
  contract {
    returns() implies value
  }
  return true
}

fun myInternalListGet(index: Int): Any? {
  require(index >= 0)
  require(index < array.length)
  return array[index] // <- range check 
}

7. What's about accessibility rules?
   Can I write contract inline fun foo(arg: SomeInterface): Boolean { contract { Returns(true) implies arg is SomeSpecificInternalImplementation } } if SomeSpecificInternalImplementation is internal or private and is not used from function body?

Verification of the contracts: how compiler should check if written contract contradicts function's actual semantics?

Can we have some global debug flag which is enabled in tests by default or with specific compiler flag? Roughly, it's compile-time analogue of Java assert. It's not a formal verification, but at least it would help to catch most of the bugs during unit testing.
Some conditional runtime checks are required anyway or K/N will silently segfault on every contract breach.

9. Value contracts concerns as libraries writer.
   Consider I'm writing high-performant library and want to use contracts to assist compiler and to make code more readable, but I don't want to pay additional runtime checks cost. E.g.

private fun stateMachineTransition(state: Any, index: Int) {
  require*(state is Started || state is Starting)
  require*(index >= 0 || index < size)
}

Can I have both verification in tests, function which I don't have to copy-paste from library to library and absence of runtime checks? Or value semantics are completely out of the scope of current proposal?

10. It's worth adding section "Similar API" with C++ contracts spec.
    E.g. they solve inheritance problem via A virtual function overrider inherits the contracts from the base class function it is overriding

[zarechenskiy]

Should effect callsInPlace(f, InvocationKind.EXACTLY_ONCE) affect initialization order check as well? For example, it'd be nice to report something here (at least a warning):

class Foo {
    val a: String = run {
        b
    }

    val b: String = run {
        a
    }
}

[voddan]

we treat verification as necessity for the contracts-annotation release

Not all algorithms can be statically analysed. Will you limit contracts only to functions simple enough for the analiser?

Do you plan to add runtime asserts that fail if a contract is broken? Such asserts could probably be controlled by the existing -enableassertions flag.

[dsavvinov]

1. E.g. how a (hypothetical) contract fun List.get(index: Int) { contract { Returns -> index < this.size } } can be expressed in a type system?

I'm not really sure that there is a way in type systems to express that, especially for variable-size collections (there are some vaguely similar constructions, like Vec in Agda, with some notable differences, but I would like to not dive into type theory here, unless absolutely necessary :) ).

Generally, idea of this point is: due to broad nature of contracts, it is theoretically possible to do some madness, like giving up on types altogether and writing only contracts, like:

fun getString(): Any {
    contract { returns<String>() }
    return "Hello"
}

Obviously, it's a wild exaggeration, but it shows that type systems and contracts have to share responsibilities -- abusing either one leads to highly cumbersome constructions.
We don't know yet where lies the dividing line between areas of their responsibilities, but we felt that it's important to note that we will try to find that line.

One of the useful but arguable use cases is strings validations. Consider following code:

// Behavior if receiver isn't a valid URL is undefined
val String.urlSchemeSubstring: String = ...

val String.isValidUrl: Boolean = ...

// Obviously, user input can contain malformed URL 
fun parseUrlFromUserInput(input: String): URL? {
    input.urlSchemeSubstring // Potentially unsafe

    if (input.isValidUrl) {
        input.urlSchemeSubstring // safe!
    }
}

On the one hand, it would be certainly nice to have such kind of static checks.

On the other hand, I'm personally concerned that contracts essentially imitate type system (opaque type aliases in particular) here: in my opinion, proper solution for this is:

• introduce opaque typealias UrlString = String
• write urlSchemeSubstring as extension to UrlString rather than String
• teach compiler to understand that if input.isValidUrl then input is UrlString, so that input.urlSchemeSubstring in if body above is safe thanks to smartcast.

We're going to research that area further.

2. What ConstantValue should be used?

Actually, in prototype returns accepts Any?, but only true, false, null constants are correct. I'll fix the description, thanks.

3. Is it accessible through reflection? Can it be used for e.g. KDoc generation?

Contracts are an ordinary part of Kotlin metadata, meaning that you can access it via reflection, but you'll have to somehow parse it (FYI, we have an experimental library for working with Kotlin metadata)

4. Is actually a disadvantage? IMO, it makes everything easier, e.g. you everything know the contract of the method without examining the whole function body.

Sure, and we're not going to allow writing contract anywhere in function body. Rather, it is possible that, in future, contracts-annotations will get even more dedicated and clearly distinguishable place. Actually contract is a part of function "external contract" in a sense of collection requirements and guarantees, same as signature, modality, visibility, etc -- however, function body usually contains details of implementation of that "external contract".
There are also some complications in tooling support connected with current placement of contract-annotations.

5. Why aren't they allowed on non open functions?

Sorry, I think you mean "non final" functions? If so, then the reason is that inheritance isn't designed yet.

How can one write contracts to interfaces with current DSL?

Do you mean contracts to interface members? If yes, then it falls under previous point: contracts for open functions are not allowed yet (actually, restriction is even stricter: contracts for members are disallowed).

6. Implementation details: are contracts propagated to the call site and can be exploited by the compiler backend? Can I assist compiler in producing more optimized code using contracts?

First of all, yes, cooperation of programmer and compiler (and assisting compiler in producing more optimized code in particular) is one of the main goals of Kotlin Contracts.

Now, about support in compiler:

• currently, Kotlin compiler doesn't collect static information about collections size. FYI, at some point Kotlin team tried to collect such information and use it for warnings about possible IndexOutOfBoundException and stuff like that, but it was found that there were a very little demand on such diagnostics in real-life projects, so, given complexity of such analysis, it was abandoned
• however, if at some point Kotlin compiler will start collecting information about collections sizes, contracts will naturally integrate into that without much effort. This is because contracts are, actually, stupid source of information -- they don't perform any analysis on their own, they just provide information to compiler

7. What's about accessibility rules?

Currently, contract-block is resolved as if it were a part of function's body (with a few little exceptions), so anything that applies to function body, applies to contract-block as well. At the moment, we don't see any concerns regarding that decision -- if you have some, please, share them :)

8, 9. Maybe I'm not following you, but I have an impression that you're talking about some runtime assertions, which should check contract integrity. If so, then I can assure you that, currently, we have no plans to bring any part of contracts to run-time, including verification.

10. It's worth adding section "Similar API" with C++ contracts spec.

Yep, nice idea, thanks!

[dsavvinov]

@voddan

Not all algorithms can be statically analysed. Will you limit contracts only to functions simple enough for the analiser?

Exact design isn't known yet, because we don't have a prototype of contracts checker, and we can't estimate which cases it will cover, and which won't. One of the options is to allow "unchecked contract", similarly to how you can make unchecked as-cast or !!-nullability assertion, if smartcasts system weren't "smart" enough :)

Do you plan to add runtime asserts that fail if a contract is broken? Such asserts could probably be controlled by the existing -enableassertions flag.

This is an interesting idea, but we have no near-time plans on implementing it.

[dsavvinov]

@zarechenskiy

Should effect callsInPlace(f, InvocationKind.EXACTLY_ONCE) affect initialization order check as well?

Yes, I think it should

[qwwdfsad]

Sorry, I think you mean "non final" functions?

No, I meant final functions. Inheritance is not designed, but contracts are still not allowed in final member functions for some reason.

Do you mean contracts to interface members?

Yes. I was speculating about "how it would work if inheritance was designed". Currently, a contract can be declared only in a function body, so contracts on interface members cannot be reasonably expressed.
It doesn't look nice to write something like

interface I {
  fun foo() { 
    contract {}
    fooImpl()
  }
  fun fooImpl() // what I want to protect with contract
}

Maybe I'm not following you, but I have an impression that you're talking about some runtime assertions, which should check contract integrity.

Yes and no. Let me explain by example.
Consider method

private fun DataStructure.addElement(element: Any?) {
  requireNonNull(state)
  addNonNull(element)
}

This is an internal method and I know that element is never null, so I write requireNonNull.
But now (as I'm a smart programmer and I know what I'm doing) I want to get rid of this null-check at runtime, so I write my own requireNonNull as inline fun requireNonNull(value: Any?): Unit { contract { returns() implies value !== null } } and my code becomes faster.
But I'm not that smart and have a bug at some point (maybe in unrelated place of code).
null sneaks into my data structure and lately it segfaults my K/N code which read that data structure and I have no idea what's happening and where is the source of a bug.
Same can be applied to is checks and putting checked element into a generic collection (and getting CCE somewhere later) or more complex values check such as require { index >= 0 }.

It would be nice to have a flag which actually compiles contracts restrictions, so one can debug these cases.

[dsavvinov]

contracts are still not allowed in final member functions.

Yes, this is intended temporary limitation.

Currently, a contract can be declared only in a function body, so contracts on interface members cannot be reasonably expressed.

Ah indeed, that's a limitation of the current approach, which was missed in the description. I'll add it to proposal, thanks!

About runtime assertions: thanks, use-case is clear, but it has to be discussed

[zarechenskiy]

Awkward “first-statement” restriction
As a consequence, functions with expression body can't have a contract

Seems that it's also true for constructors without body

[LouisCAD]

An open question need to be added: support for suspend fun.
Here's an example: you could initialize an outer scoped val from a withContext { … } lambda, which could also be in a measureNanoTime { … } lambda, and maybe more nested lambdas that run exactly once.

[Dico200]

I know annotations are quite limited in Java, but wouldn't it be possible to implement an annotation like this:

@Contract({
   callsInPlace(block, InvocationKind.EXACTLY_ONCE)
})
inline fun hello(block: () -> Unit) = block()

With source retention, the compiler should be able to make a special case for such an annotation. However, it kinda violates scope access rules too.
On the other hand, it doesn't require a block body.

To be honest, I don't think that's such a big deal, but it's important to be extra careful when you're about to implement something into a language as a guaranteed feature.

EDIT: you could do callsInPlace("block", InvocationKind.EXACTLY_ONCE)
which removes the scope access violation.

[Wasabi375]

Theoretically of cause, you could probably implement any syntax. The question is what the best way of expressing contracts is. I don't think this can be easily answered yet as there is no available prototype yet (afaik). Also this depends on some parts of the design which are not final yet, eg inheritance and which other kinds of contracts we can reasonably expect to use.
I think the current way for the prototype is the best choice as it takes the least effort and let's the team developing contracts focus on the implementation rather than on some syntax, which will probably have to change anyways.
As to your idea of using annotations like that. I like the idea of maybe having annotations expressing the contract of a function (outside of the Metadata annotation) as this would allow for java projects to add contracts as well. If annotations get their own special syntax though I would prefer the example syntax used in the KEEP. It's expressive and stands out from the rest of the code so you notice it as part of the external function contract and see that it's not part of the implementation.

[Returns(true) -> x is String]
fun isString(x: Any?): Boolean = x is String

[mikehearn]

Great effort, here are some initial thoughts.

Static verification of contracts may take you in the direction of Whiley (whiley.org) which statically verifies code using the Z3 constraint solver. That's hard! These sorts of constraint solver based static analyses seem to require a lot of hints to prove very trivial things.

It'd probably be easier for the first versions of this feature to generate code at runtime to verify the contracts, for example, if a contract states a lambda is used exactly once, the compiler frontend could then immediately wrap it in an object that has a boolean flag tracking whether it was invoked. A good JIT compiler would realise the wrapper never escapes and scalar replace it to a boolean on the stack, then go further and prove the assertion can never fire because the lambda is in fact invoked only once, and optimize out the entire overhead of the wrapper. So it'd be zero overhead once warmed up.

The justification for the proposed syntax all makes a lot of sense but it's unfortunate that the proposed syntax looks exactly like code that will execute at runtime even though it's not. People will cmd-click through and be confused to discover the functions apparently do nothing, they are skipped over during debugging etc. I wouldn't be averse to a small bit of new syntax or a new modifier that made it clear the code was compile-time only, with there being no implementation viewable in the stdlib (i.e. IntelliJ could be special cased to not allow navigation or stepping into it). Something like:

fun foo(bar: () -> Unit)) {
    nocompile contract {}
}

A nocompile modifier that changes the rules such that (A) the block won't appear in the generated bytecode and (B) might be syntax highlighted differently and (C) would only allow usage of definitions marked "expect" so there's no empty body to confuse other tools, might be useful for other projects that want to embed similar metadata-like DSLs into Kotlin.

[mikehearn]

Oh, another random thought - you're designing your own binary format here, though the actual input is a more limited form of regular code. Why not generate JVM bytecode and then embed that into your reflective protobufs or new annotations? Of course you don't have to actually support full bytecode, just recognising patterns emitted by the compiler is fine, but it'd make the "embed code-that-is-not-code" pattern more general and usable by others outside the Kotlin team.

Alternatively perhaps emit a pattern where the pseudo-bytecode is always dead (jumped over immediately), as an alternative to using annotations. That way decompilers can pick up the contracts DSL too. There don't need to be any definitions to actually go to on the classpath, because the code will never be invoked, and thus the JVM will never try to link the call sites.

I realise it may be a bit late to discuss the binary format because the blog post implies it's already stabilised.

[Xfel]

I recently tried to use the new contract system in M2 to make a smart-casting version of isArrayOf.
Unfortunately, this is currently not possible. I would need to write implies (a is Array<T>), and the compiler then complains about generics erasue.

Since the compiler behaviour should not be changed, we need a method like impliesIsInstance<Array<T>>(a) to handle those cases.

[dsavvinov]

@mikehearn thanks a lot for the detailed feedback!

About verification: yes, one of the possible options is that contracts generally should be checked at the runtime, and omitting those checks (in case it is possible to prove correctness at compile-time) can be viewed as compiler optimization.

About syntax: indeed, it's kinda awkward that it looks like code which will be executed, though it's not. It will be most certainly re-worked in future. In such case, nocompile is viable, but, probably, not the best option for contracts specifically.

About binary format: as been discussed, it's not really a code, even though we resort to use code to imitate contracts declarations. This is one of the reasons why we've decided to design our own binary format here. (Some) others are:
a) Kotlin isn't only JVM, so using JVM-like pseudocode would look awkward for other platforms
b) contracts is a part of function signuatre, so it looks right to place it somewhere near other parts of function signature (in Kotlin metadata) rather than in body
c) dealing with code at compile-time looked like an overkill for our use-case

P.S. It seems to me (I'm guessing here, so excuse me if I'm wrong :) ) that you have some particular use-case in mind which could be covered by mechanisms similar to those used for supporting contracts -- you've mentioned "external usages" several times. If that's the case, we'd be very curious to hear about it, so feel free to reach me through any channel you like (kotlinlang slack, my email, Kotlin YouTrack, etc.)

[dsavvinov]

@Xfel this restriction is intended, and support for cases like impliesIsInstance is TBD. The reason
may not be obvious from the first glance, but actually, introduction of such contracts will noticeably complicate support of the language in IDE. We're not rejecting it immediately, but we need much more time to consider it.

[tieskedh]

is there a way to express the following at once:

fun containsNoNull(
    first : Any? = '', 
    second: Any? = '', 
    third : Any? = '', 
    fourth : Any? = '') : Boolean{
    contract{
        returns(true) implies (first != null && second != null && third != null && fourth != null) 
     } 
     return first != null && second != null && third != null && fourth != null
} 

If this can be changed to the following:

fun containsNoNull(
    first : Any? = '', 
    second: Any? = '', 
    third : Any? = '', 
    fourth : Any? = ''
) = contractedIf{
        (first != null && second != null && third != null && fourth != null) 
}

Then you know at compile-time that it works, and you can't make mistakes due to boilerplate.

[dsavvinov]

How to avoid writing boilerplate for short functions is an open question indeed.

Omitting explicit contracts has various downsides, major being support in IDE -- it's impossible to know if the function has contract until we resolve it's body, and it's a huge complication (note that currently situation is kinda the same, and it's one of the main reasons for declaration syntax redesign).

Another approach is to band-aid it by smart tooling support: IDE could infer contract for such a simple function automatically and suggest to insert it for you (relieving the burden of manually copy-pasting it), as well as somehow hide/fold "trivial" contracts (solving the issue of boilerplate).

That's not an ideal solution too, obviously, so yeah, it's an open question :)

[Dico200]

Maybe it's worth considering that an abstract function can't guarantee that its inheritors comply with the contract it wants to declare.
Just a thought about the issue that was put forward - you can't declare a contract for abstract functions because currently, a contract must be placed in a code block.

[LouisCAD]

@volo-droid Looks like regression to report on kotl.in/issue

[chachako]

Can the contract do more powerful things?

For example, limit the input of parameters:
I designed

function(val data: Any) {
  require(data is String && data is Int) { ... }
}

but I only want data to receive String and Int. In this case, it is obviously better to report errors when coding than to throw exceptions at runtime

[chachako]

@rjhdby Yes, we're actively researching applications of contracts in DSLs at the moment, but it's too early to announce something specific yet.

#139 (comment)

Sorry to interrupt, I want to know if this kind of contract is planned? I think this is really helpful for DSL, because now in DSL we can’t force users to call certain api.

[AhmedMourad0]

I'm here for the same reason @rinorz just mentioned, which is comment #139, This would be massively helpful to ensure compile-time type-safety for many DSL-oriented APIs.

[AhmedMourad0]

but I only want data to receive String and Int. In this case, it is obviously better to report errors when coding than to throw exceptions at runtime

@rinorz This would be better handled with Union types instead of contracts, there is a shelved issue for that on Kotlin's YouTrack.

[volo-droid]

Can we add a possibility to decrease the scope of this smart casts with contracts?
Consider the following use-case:

@DslMarker
annotation class BddDsl

@BddDsl
class DslBlock

@BddDsl
interface BddBuilder

@BddDsl
interface BddGivenBuilder

@BddDsl
interface BddWhenBuilder

@BddDsl
interface BddThenBuilder

@BddDsl
class BddFullBuilder : BddBuilder, BddGivenBuilder, BddWhenBuilder, BddThenBuilder

data class Given(val data: Any)

fun bdd(block : BddBuilder.() -> Unit) {
    BddFullBuilder().apply { block() }
}

inline fun BddBuilder.given(givenBlock: DslBlock.() -> Given) {
    contract {
        returns() implies (this@given is BddGivenBuilder)
    }

    DslBlock().givenBlock()
}

inline fun BddGivenBuilder.When(whenBlock: DslBlock.() -> Unit) {
    contract {
        returns() implies (this@When is BddWhenBuilder)
        returns() implies (this@When !is BddBuilder)
    }

    DslBlock().whenBlock()
}

inline fun BddWhenBuilder.then(thenBlock: DslBlock.() -> Unit) {
    contract {
        returns() implies (this@then is BddThenBuilder)
        returns() implies (this@then !is BddGivenBuilder)
    }

    DslBlock().thenBlock()
}

fun test() =
    bdd {
        val this0: BddBuilder = this        // OK

        given {
            Given(2)
        }
        val this1: BddGivenBuilder = this   // OK

        When {
            "method is called"
        }
        val this2: BddWhenBuilder = this    // OK

        then {
            "assertThat"
        }
        val this3: BddThenBuilder = this    // OK


        // Ideally, the following statements should fail, but they're compiled currently

        val this4: BddBuilder = this
        val this5: BddGivenBuilder = this
        val this6: BddWhenBuilder = this
        given {
            Given("ideally, should not compile")
        }
        When {
            "ideally, should not compile"
        }
    }

The idea is to have a DSL that allows calls only in the specific order (given -> When -> then).
Currently, contracts work only partially, disallowing When to be called before given, and then before either When or given). But they don't prevent us from calls like: given -> When -> given -> then -> When, even though there's an explicit !is contract in the method definitions.

[demiurg906]

@volo-droid Actually you just described completely different type of contracts -- safe builders contracts (which would serve to checking that functions in DSL was invoked in exact order and specific number of times). We are considering to add such contracts to Kotlin but I can't say when it will be done

You can check samples of my old prototype of such contracts here

[way-zer]

May add new syntax to @contract,like

@Contract("_->this")
 fun A.doSomethingA():A{
   return this
 }

For invoke, if A is open. and B extend A.

val b:B
b.doSomethingA().xxx()
//compiler output (b.doSomethingA() as B).xxx()

Discuss on https://discuss.kotlinlang.org/t/self-types/371/82

[fvasco]

I have two concern regarding the current proposed syntax.

The contract is present inside the function's body, however the contract should be part of first part, so it isn't an implementation details, but it specify the function's behaviour, therefore the contract should be visible in the documentation, also.
The function's contract isn't subject to change, while implementation may.
Dokka should be able to render the contracts.

While the current contract's syntax is a valid Kotlin code, some rules may look innatural.
Kotlin use an imperative syntax, so if (condition) return, while contracts defines rules like returns() implies condition.

Maybe these two issues can be addressed togheter, for example:

fun foo(condition:Boolean)
    contract { if (condition) returns() }
    body { /* function body */ }

or

contract { if (condition) returns() }
fun foo(condition:Boolean) { /* function body */ }

[demiurg906]

We are considering a new syntax for contracts (it is even implemented in K2 compiler), which will look like this:

fun require(condition: Boolean) contract [ returns() implies condition ] {
    // body
}

Syntax is not final, so some adjustments can be made (like replacing [] with {})

As for your second proposal, then IMO it reads much more innatural. if (condition) returns() reads like if condition is true then function returns without exception, but on the call side contract is used contrariwise: if function returns without exceptions then condition is true, so it can be used for smartcasts

[BenWoodworth]

Useful to note, from the Declaration Syntax section: https://github.com/Kotlin/KEEP/blob/3490e847fe51aa6deb869654029a5a514638700e/proposals/kotlin-contracts.md#declaration-syntax Conclusion: this is a nice option to experiment with contracts, as it leaves enough room for future extensions and modifications and provides out-of-the-box tooling and compiler support. Declaration syntax is a bit awkward, but this is acceptable for purposes of the prototype.

[fvasco]

Double negation can be fixed with an adequate syntax, like

if (!condition) throws()

or

if (!condition) throws(IllegalArgumentException)`

Avoiding the mental switch should reduce the error-rate, hopefully.

Regarding the [] or {} debate, I mentally associate:
( ) -> parameter/argument
[ ] -> list/map
{ } -> code
< > -> generics

IMHO, the debate should be {} or ().

[gmale]

This seemed useful in 2018 but I couldn't incorporate it because it was experimental. Just checked back almost 5 years later and, sadly, it still seems experimental. In contrast, coroutines were introduced as experimental around the same time and have since become the de facto standard.

Is there an opportunity to reduce the scope of Kotlin Contracts and deliver a subset of functionality that can be considered non-experimental?

[demiurg906]

@gmale Work on contracts was suspended because of focusing on K2 compiler development. We plan to stabilize contracts right after the K2 release

Also, contracts themselves are quite stable, and there is no plan to change the behavior of existing contracts. The main thing which is not stable is the contract declaration syntax. The new syntax passed pre-design and is already prototyped, so there is a big possibility that it will be out in the next release after K2

[eupp]

We are considering a new syntax for contracts (it is even implemented in K2 compiler), which will look like this:

fun require(condition: Boolean) contract [ returns() implies condition ] {
    // body
}

Syntax is not final, so some adjustments can be made (like replacing [] with {})

As for your second proposal, then IMO it reads much more innatural. if (condition) returns() reads like if condition is true then function returns without exception, but on the call side contract is used contrariwise: if function returns without exceptions then condition is true, so it can be used for smartcasts

Your description of returns() implies condition semantics sounds similar to the description of a post-condition of a function. Is it the case?

Regarding the returns() implies condition syntax, have you considered an alternative syntax using ensures keyword?

fun require(condition: Boolean) contract [ ensures(condition) ] {
    // body
}

The requires and ensures terminology is quite common in contract-based programming to express pre- and post- conditions of functions correspondingly.
Just a few examples from other languages:

• .Net contratcs
• Dafny language
• Eiffel language

Besides that, pre/post conditions have sound theoretical basis (i.e. Hoare Logic), and there is a potential of integrating third-party tools (e.g. Viper) in the future to optionally verify pre/post conditions.

[demiurg906]

I agree that the current DSL may be a bit verbose, but ensures(condition) is not such flexible as returns() implies condition. The thing is there are four different variations of this contract

• returns()
• returns(true)
• returns(false)
• returnsNotNull()

And ensures(condition) covers only the first one

[demiurg906]

BTW we have in mind a design for special syntax for the contracts composition, so it will be possible to define your own shortcuts for contracts dsl:

contract fun ensures(condition: Boolean) = [returns() implies condition]

fun someMyRequire(condition: Boolean) contract [ensures(condition)] { ... }

Note that this syntax is also not final

[eupp]

I agree that the current DSL may be a bit verbose, but ensures(condition) is not such flexible as returns() implies condition. The thing is there are four different variations of this contract

* `returns()`

* `returns(true)`

* `returns(false)`

* `returnsNotNull()`

And ensures(condition) covers only the first one

In other contract-based languages, the ensure is often more powerful and usually also takes the return value as a parameter. Translating this to Kotlin-like syntax, it might look as follows:

fun foo(x: Int): Int contract [ ensures { r -> r > 0 } ] {
    // body ...
}

Here the post-condition states that return value should be greater than zero (I realize that currently returns(value) in Kotlin supports only true, false, or null --- this is just an example of the syntax).

With this kind on ensures one can express all of 4 cases you mentioned, e.g. for true:

fun isString(x: Any?): Boolean contract [ ensures { r -> (r == true) implies (x is String) } ] = 
    x is String

where implies can be defined as ordinary function:

infix fun Boolean.implies(other: Boolean): Boolean = !this || other

I realize that this form of ensure { r -> ... } with lambda is very general and might be out of scope for what you try to achieve with Kotlin contracts. Just wanted to point out how similar ideas are expressed in other contract-based programming languages.

[demiurg906]

From what I saw, other languages have much more complex effects systems (potentially with dependent types) or use effects declaration to inject runtime checks into start/end of functions. In Kotlin, contracts are needed only to provide some information about the function which is not expressible just with signature to the compiler (at least at this point), so contracts like ensures { r -> r > 0 } are more or less meaningless

But anyway, thank you for those examples. They might be helpful when we continue to work on the contract syntax

[leanderBehr]

As far as I can tell, the current implementation (1.8.21-release-380) does not support the use case in the second example of the KEEP:

fun test() {
    var x: Int? = 42
    run {
        // Smartcast is forbidden here, because compiler can't guarantee
        // that this lambda won't be executed concurrently with 'x = null'
        // assignment
        if (x != null) println(x.inc)
    }
    x = null
}

Is this correct and if so, are there plans to support this? I think it would require a change in the spec to sink stability to take the callsInPlace effect into account.

More broadly, it seems like the callsInPlace effect is currently never useful for smartcasts or am I missing something?

[demiurg906]

@leanderBehr This case is already supported in the K2 compiler

You can check it by setting language version to 2.0 with 1.8.21 or 1.9.0-Beta compilers

[leanderBehr]

Is there no updated specification text yet? I checked develop but it seems to be the same as the current spec in this regard.

[demiurg906]

@leanderBehr no, there isn't. Adding contracts to specification will be handled together with contracts stabilization after 2.0 release

[gmk57]

Contracts for extension functions inside a class don't work. Seems this@functionName gets resolved to outer class, not to receiver. 😢 Is this by design? Is there some other way to reference receiver?

[demiurg906]

@gmk57 This is a bug which is already fixed in K2 compiler

[Jolanrensen]

Will contracts ever support implication of nested types?
For instance:

fun List<Any?>.isStringList(): Boolean {
    contract { 
        returns(true) implies (this@isStringList is List<String>)
    }
    return all { it is String }
}

fun test(x: List<Any?>) {
    if (x.isStringList()) {
        x.first().length // Should compile
    }
}

[demiurg906]

@Jolanrensen There is a KT-45683 for that request