paradigms-2026/lectures/README.md

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Например

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

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

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

/*

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

Для цикла while:

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

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

// 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 -- частный случай контракта.

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

int x;

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

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

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

int x;

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

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

А здесь:

int x;

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

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

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;
}