# P0007

Postcondition violated: an `ensures` clause of the function that returned is false, so the function broke its promise. The message names the function, quotes the clause's condition, and names the line and column of the return that broke it, counting columns in characters from 1. Spans the `ensures` clause. Every return evaluates the function's `ensures` clauses, in every build, in the order written, with `r` bound to the value being returned. That covers falling off the end of the body (the return is its last expression, or its closing brace), an early `return`, and an early exit through `?`, where `r` is the `Err` or `None` being returned. A clause sees the parameters and `self`; a method that changes `var self` shows its clauses the receiver it ends with. A contract that calls a function with contracts checks those too, and a panic while a clause is evaluated, such as an overflow, is reported as it is, not as `P0007`.

**Machine-applicable fix:** none.

## Example

This program fails with `P0007`.

```oska
fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    x
}

fn main() {
    let y = absolute(-1)
}
```

## Fixed

The same program, fixed.

```oska
fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    if x < 0 {
        0 - x
    } else {
        x
    }
}

fn main() {
    let y = absolute(-1)
}
```

Listed in the [runtime notes](/runtime.md#p0007). `oskac explain P0007` prints this entry offline.