293 lines
6.9 KiB
Markdown
293 lines
6.9 KiB
Markdown
# Лекция 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;
|
||
}
|
||
```
|
||
|