Is there a built-in contract for verifying that, i...

# announcements

[Sam Garfinkel]

Is there a built-in contract for verifying that, if a Map contains key k then Map[k] is non-null? Or do I need to write my own?

[Sam Garfinkel]

Actually not sure this is really possible. Doesn’t seem like a contract can imply anything about other functions you can call on a parameter.

[raulraja]

The current contract system in the compiler accepts simple boolean expression and set of specific contracts. AFAIK It’s not possible at the moment to add preconditions that are able to be set as data flow preconditions based on complex boolean expressions.

[Sam Garfinkel]

Yeah I found this SO question shortly after posting here: https://stackoverflow.com/questions/55228282/kotlin-contracts-effect-on-another-property-function

[Sam Garfinkel]

Which suggests that seems to be the case

[raulraja]

Here is an example of roughly what you want to proof over List which is simple:

[raulraja]

you can run this in https://rise4fun.com/Z3/tutorial

head is safe or unsafe

[raulraja]

so essentially this kinds of proof requires more power than most compilers have. Unless its Idris or other langs where you can encode this refinements that make access safe.

[Kroppeb]

The issue is that the key could have been removed on a different thread