# Лекция 1. Программирование по контракту.

Мы видим следующий код: 

```java
public class Magic {
    int magic(int a, int n) {
        int r = 1;
        while (n != 0) {
            if (n % 2 == 1) {
                r *= a;
            }
            n /= 2;
            a *= a;
        }
        return r;
    }
}
```

Что это за код?

Как понять: 

1. Пристально посмотреть.
2. Написать тесты.
    * Это не поможет понять, работает ли код. Тесты могут только показать, что код **НЕ работает**.
3. Написать формальное доказательство.

Для последнего пункта нам понадобится *теорема о структурной декомпозиции*.

**Формулировка**: Любой код, который мы можем написать на каком-то языке, можно представить в виде замыкания следующих операций: 

1. Ничего
2. Последовательное исполнение операций (последовательность действий)
3. Присваивание
4. Ветвление
5. Цикл `while`

С точки зрения теоремы, этих действий достаточно, чтобы написать любую содержательную программу.

Можно ли ввести такую конструкцию при помощи примитивов выше:

```java
try {
    // some code here
} catch (...) {
    // some code here
} finally {
    // some code here
}
```

Давайте введем переменную `exitCode` и для каждого действия, в зависимости от того, успешно оно выполнилось или нет, будем обновлять `exitCode`. 

```java
if (exitCode == 0) { // без ошибок
    // делаем дальше
} else {
    // ничего не делаем
}
```

Попытаемся этим воспользоваться.

Мы хотим наложить какие-то условия на нашу функцию, так что если эти условия на вход выполняются, то мы получим гарантированно правильное значение. Чтобы это доказать, нам помогут *тройки Хоара*. 

Хоар придумал quick sort.

Тройка состоит из `P`, `C` и `Q`, где 

* `P` - пред-условие
* `C` - код,
* `Q` - пост-условие

Если у нас есть код `C`, и мы выполняем какое-то пред-условие, то после исполнения кода, у нас будет выполнено какое-то пост-условие.

Для операции *ничего*: 

```java 
/*
Pred: Condition
Code: ;
Post: Condition
*/
```

То условие, которое было до того, как мы сделали *ничего*, останется.

Для *последовательности действий*:

```java 
/*
Pred: P1
Code: ...
Post: Q1
Pred: P2
Code: ...
Post: Q2
*/
```

Таким образом из `Q1` должно следовать `P2`.

```java
/*
Pred: P1
Q1 -> P2
Post: Q2
*/
```

Для *присваивания*: 

```java 
/*
Pred: Q[x = expr]
Code: x = expr
Post: Q
*/
```

Например

```java
// Pred: (x = a + 2)[x = 6] -> a = 4
x = a + 2
// Post: x = 6
```

То есть только при `a == 4`, выполнится пост-условие.

Для операции `ветвление`: 

```java
/*

// Pred: cond && P1 || ~cond && P2
if (cond) {
    // Pred: P1
    ...
    // Post: Q1
} else {
    // Pred: P2
    ...
    // Post: Q2
}
// Q1 -> Q && Q2 -> Q
// Post: Q
*/
```

Для цикла `while`:

```java
/*
// Pred: P = I
while (cond) {
    // Pred: I
    // Post: I (инвариант цикла)
}
// Post: Q = I
*/
```

Посмотрим на примере: 

```java
// Pred: true
// Post: r = A' ^ N'
int magic(int a, int n) {
    // A' = a, N' = n -- начальные значения


    // Pred: A' == a && N' == n
    int r = 1;
    // Post: r == 1 && a ** n * r == A' ** N'


    // Pred: a ** n * r == A' ** N'
    // Inv: (a ** n) * r = A' ** N' 
    while (n != 0) {
        // Pred: a ** n * r == A' ** N'
        if (n % 2 == 1) {
            // Pred: a ** n * r == A' ** N'
            r = r * a;
            // Post: a ** (n - 1) * r = A' ** N'

            // Pred: a ** (n - 1) * r = A' ** N'
            n = n - 1;
            // Post: a ** n * r = A' ** N'
        }
        // Post: a ** n * r = A' ** N'

        // Pred: a ** n * r = A' ** N'
        n /= 2;
        // Post: a ** (2 * n) * r = A' ** N'


        // Pred: a ** (2 * n) * r = A' ** N'
        a = a * a;
        // Post: a ** n * r = A' ** N'
    }
    // Post: a ** n * r = A' ** N' && n == 0


    // Pred: r = A' ** N'
    return r;
    // Post: r = A' ** N' 
}
```

Мы формально доказали, что метод `magic()` возводит число `a` в степень `n`. Такая функция называется чистой, так как она не зависит от внешних переменных.

То, что мы написали, называется контракт. Участниками контракта являются *пользователь* и *разработчик*. 

Мы, как разработчик, требуем пред-условие, и тогда можем гарантировать, что пост-условие будет выполняться.

`interface` в java -- частный случай контракта.

Это были случаи определения контракта для *чистых* функций. А как действовать в других случаях. Приведем пример

```java
int x;

// Pred: 
// Post: 
int add(int y) {
    x = x + y;
    return x;
}
```

Определим *модель* как некоторое состояние нашего класса.

```java
/*
Model: x (целое число)
*/
```

```java
int x;

// Pred: true
// Post: x = x' + y (x' -- старый x)
int add(int y) {
    x = x + y;
    return x;
}
```

Здесь контракт соблюдается.

А здесь:

```java
int x;

// Pred: true
// Post: x = x' + y (x' -- старый x)
int add(int y) {
    x = x + y * 2;
    return x / 2;
}
```

Контракт также соблюдается. То есть нам не важны детали реализации. 
Можно даже сделать вот так: 

```java
private int x = 10;

// Post: x = 0
void init() {
    x = 1;
}

// Pred: true
// Post: x = x' + y
int add(int y) {
    x = x + y * 2;
    return (x - 1) / 2;
}

// Pred: true
// Post: R := x
int get() {
    return (x - 1) / 2;
}
```