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<T>. 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.

[dsavvinov]

...abstract function can't guarantee that its inheritors comply with the contract it wants to declare

Indeed, but we can ask inheritors to comply to its contract -- similar to how we "ask" (require, actually) inheritors to comply to the declared signature or declared type parameters bounds. In other words, contracts should be somehow "inherited": then verfier kicks in and checks that inheritor's implementation doesn't violate contract (and for verifier it is irrelevant if contract was declared or inherited).

you can't declare a contract for abstract functions because currently, a contract must be placed in a code block.

Note that the same issue appears with open methods (being abstract is actually irrelevant here, open/final is what matters). This is a primary reason of why it is currently forbidden to use contracts for member functions.