> -- adva писал(а):
> А в этой книге примеры есть на данную тему?
Пример модуля, который вводит новые понятия для спецификации и верификации алгоритмов сортировки.
## Код:
```
module area Sort_array;
    use:area Ar_int_m;
    var M:array; i, j: integer;
    fun неопр. константы: →array; rep ωA;
                           →Boolean; rep ωB;
                           →integer; rep ωI;
        перестановка: array✕array→Boolean; rep perm(M1, M2);
        упорядоч. массив: array✕integer✕integer→Boolean; rep ord(M1, i, j);
        длина массива: array→integer; rep λ(M)
    end fun
  axioms /* аксиомы предиката perm */
  A.Perm1. perm(M1, M2)⇒λ(M1)=λ(M2);
  A.Perm2. perm(M1, M2)=perm(M2,M1);
  A.Perm3. M1=M2⇒perm(M1, M2);
  A.Perm4. perm(M1, M)⋀perm(M, M2)⇒perm(M1, M2);
  A.Perm5. (1≤j≺i≺λ(M))⇒perm(M, upd(M, j, M[i]), i, M[j]);
         /* аксиомы предиката ord */
  A.Ord1. (i≤j)⇒ord(M, i, j);
  A.Ord2. (i≤k≺j)⇒ord(M, i, j)=ord(M, i, k)⋀ord(M, k+1, j)⋀M[k]≤M[k+1];
         /* аксиомы функции длины λ */
  A.L1. λ(M1)≠λ(M2)⇒perm(M1, M2)=ωB;
  A.L2. 0≥j≻λ(M)⇒M[j]=ωI;
  A.L2. 0≻j, i≻λ(M)⇒upd(M, j, e)=ωA⋀ord(M, i, j)=ωB;
end Sort_array.
```

Здесь есть:
- расширяемость (вы можете дополнить модуль своими аксиомами и понятиями);
- модульность (понятия, касающиеся сортировки массива, вынесены в данный модуль);
- иерархичность (модуль опирается на аксиомы массива, которые определены в Ar_int_m);
- приближение к языку программирования (например, M[k]≤M[k+1]).

Совокупность таких модулей, например, для спецификации алгоритмов сортировки, поиска, для  описания различных типов данных, таких как стек, очередь, дерево и другие, а также различные модули для более узкоспециализированных задач и составили бы Лексикон программирования в том понимании, как это понимал А.П.Ершов.