update

lectures/README.md

@@ -0,0 +1,292 @@
+# Лекция 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;
+}
+```
+