Пример. Решение системы линейных уравнений Система автоматизации доказательства PVS Язык спецификаций PVS Описания типов, констант, переменных, формул, - презентация

1 Пример. Решение системы линейных уравнений Система автоматизации доказательства PVS Язык спецификаций PVS Описания типов, констант, переменных, формул, утверждений, рекурсивные определения Проверка типов (typechecking) Выражения, декларации, теории Библиотеки теорий PVS Лекция 9 Предикатное программирование

2 type STR = array (char, M..N); (7.39) STR S; nat n = 0; for (int j = m; ;) { for (; ;) { if (j > p) return char e = S[j]; j = j + 1; if (цифра(e)) break } nat v = val(e); for (;j

3 Имеется недостаток программы (7.39): если строка s завершается цифрой, то проверка исчерпания строки реализуется дважды. Чтобы исправить недостаток, следует вместо предиката числоВстроке(e, r: v, t) использовать гиперфункцию числоВстроке1(e, r: v1: v2, t), в которой первая ветвь реализуется при исчерпании входной строки r. Возможен другой более простой алгоритм. На очередном шаге вычисляется значение очередного числа в строке в виде предиката числоВстроке(s: v, t), где v значение очередного числа, а t остаток непустой строки s. Если первый элемент s не является цифрой, то v = 0. Реализация данного алгоритма дает более короткую программу, чем (7.39), однако менее эффективную. По сравнению с (7.39) лишними действиями являются операторы v = 0 и n = n + v для каждого символа, отличного от цифры.

4 int n=0, j=0; while (j < N) { e=S[j++]; w = 0; while (j < N && String.IsNumber(e)) { w = int.Parse(e) + w * 10; e = S[j++]; } n = n + w; }

5 Система линейных уравнений type VEC(nat k) = array (real, 1.. k); type MATR(nat k) = array(real, 1..k, 1.. k); formula SUM(nat n, predicate(nat: real) f: real) = n=0? 0: SUM(n-1, f) + f(n); formula LinEq(nat n, MATR(n) a, VEC(n) b, x) = forall i=1..n. SUM( n, predicate(nat j: real) {a[i, j] * x[j]} ) = b[i]; Lin(nat n, MATR(n) a, VEC(n) b: VEC(n) x : ) pre 1: not det(a) 0 { TriangleMatr(n, a, b: MATR(n) c, VEC(n) d : #2); Solution(n, c, d: VEC(n) x ) #1 } post 1: LinEq(n, a, b, x); алгоритм Гаусса (метод Жордано) LinEq(a, x, b)

6 formula postLin(nat n, MATR(n) a, VEC(n) b, MATR(n) c, VEC(n) d) = forall VEC(n) x, y. LinEq(a, b, x) & LinEq(c, d, y) x = y formula triangle(nat n, MATR(n) a) = ( i=1..n. a[i, i] = 1) i,j=1..n. (i > j a[i, j] = 0) TriangleMatr(nat n, MATR(n)a, VEC(n) b: MATR(n) a, VEC(n) b : ) pre n > 0 pre 1: det(a) != 0 {Jord(n, a, b, 1: a, b : ) } post 1: postLin(n, a, b, a, b) & triangle(n, a); Спецификация неоднозначна ! Для верификации Lin применяются правила RS9 RS13 для общего случая

7 formula triaCol(nat n, k, MATR(n) a) = i=1..k-1. (a[i, i] = 1) i = 1..n,j=1..k-1. (i > j a[i, j] = 0) Jord(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b : ) pre 1 k n & triaCol(n, k, a) pre 1: det(a) != 0 {diagEl(n, a, b, k: MATR(n) c, VEC(n) d : #2); norm(n, k, c, d: MATR(n) e, VEC(n) f); subtrLines(n, k, e, f: MATR(n) g, VEC(n) h); if (k = n) { a = g || b = h #1 } else Jord(n, g, h, k + 1: a, b #1 : #2) } post 1: postLin(n, a, b, a, b) & triangle(n, a);

8 diagEl(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b : ) pre 1 k n & triaCol(n, k, a) pre 1: det(a) != 0 { if (a[k, k] != 0) {a = a || b = b #1} else perm(n, a, b, k, k+1: a, b #1 | #2) } post 1: a[k, k] != 0 & postLin(n, a, b, a, b)

9 perm(nat n, MATR(n) a, VEC(n) b, nat k, m: MATR(n) a, VEC(n) b : ) pre 1 k n & kn) #2 else if (a[m, k] != 0) { b = b for (j) {case k: b[m] case m: b[k]}; a = a for (i, j) {case (k, k..n): a[m, j] case (m, k..n): a[k, j]} #1 } else perm(n, a, b, k, m + 1: a, b #1 : #2) } post 1: a[k, k] != 0 & postLin(n, a, b, a, b)

10 norm(nat n, k, MATR(n) a, VEC(n) b: MATR(n) a, VEC(n) b) pre 1 k n & a[k, k] != 0 & triaCol(n, k, a) { b = b for (j) {case k: b[k] / a[k, k] }; a' = a for (i, j) {case (k, k..n): a[k, j] / a[k, k]} } post a[k, k] = 1 & postLin(n, a, b, a, b) subtrLines(nat n, k, MATR(n) a, VEC(n) b: MATR(n) a, VEC(n) b) pre 1 k n & a[k, k] = 1 & triaCol(n, k, a) { b = b for (i) {case k+1..n: b[i] - b[k] a[i, k]}; a' = a for (i, j) {case (k+1..n, k..n): a[i, j] - a[k, j] a[i, k] } } post triaCol(n, k+1, a) & postLin(n, a, b, a, b)

11 Solution(nat n, MATR(n) a, VEC(n) b: VEC(n) x ) pre n > 0 & triangle(n, a) {uniMat(n, a, b, n: VEC(n) x ) } post LinEq(n, a, b, x) formula nulColl(nat n, k, MATR(n) a) = j=k+1..n. i=1..j-1. a[i, j] = 0 uniMat(nat n, MATR(n) a, VEC(n) b, nat k: VEC(n) x ) pre n > 0 & triangle(n, a) & nulCol(n, k, a) {if (k = 1) x = b else { subtrCol(n, a, b, k : MATR(n) c, VEC(n) d); uniMat(n, c, d, k-1: VEC(n) x ) } } post LinEq(n, a, b, x)

12 subtrCol(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b) pre n > 0 & triangle(n, a) & nulCol(n, k, a) {b = b for (i) {case 1..k-1: b[i] - b[k] a[i, k]}; a' = a for (i, j) {case (1..k-1, k): 0 } } post nulCol(n, k-1, a) & postLin(n, a, b, a, b) На первом этапе трансформации реализуется склеивания. Lin: a

13 На втором этапе реализуется замена хвостовой рекурсии циклами. Результатом проведения двух этапов трансформации является следующая программа: Lin(nat n, MATR(n) a, VEC(n) b: VEC(n) b : ) { TriangleMatr(n, a, b: MATR(n) a, VEC(n) b : #2); Solution(n, a, b: VEC(n) b ) #1 } TriangleMatr(nat n, MATR(n) a, VEC(n) b: MATR(n) a, VEC(n) b : ); {Jord(n, a, b, 1: MATR(n) a, VEC(n) b : ) }

14 Jord(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b : ) {for(;;) { diagEl(n, a, b, k: MATR(n) a, VEC(n) b : #2); norm(n, k, a, b: MATR(n) a, VEC(n) b); subtrLines(n, k, a, b: MATR(n) a, VEC(n) b); if (k = n) #1 else k = k + 1 } diagEl(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b : ) {if (a[k, k] != 0) #1 else perm(n, a, b, k, k+1: a, b #1 | #2) }

15 perm(nat n, MATR(n) a, VEC(n) b, nat k, m: MATR(n) a, VEC(n) b : ) {for(;;) { if (m>n) #2 else if (a[m, k] != 0) { b = b for (j) {case k: b[m] case m: b[k]}; a = a for (i, j) {case (k, k..n): a[m, j] case (m, k..n): a[k, j]} #1 } else m = m + 1 } norm(nat n, k, MATR(n) a, VEC(n) b: MATR(n) a, VEC(n) b) { b = b for (j) {case k: b[k] / c[k, k] }; a = a for (i, j) {case (k, k..n): a[k, j] / a[k, k]} }

16 subtrLines(nat n, k, MATR(n) a, VEC(n) b: MATR(n) a, VEC(n) b) { b = b for (i) {case k+1..n: b[i] - b[k] a[i, k]}; a = a for (i, j) {case (k+1..n, k..n): a[i, j] - a[k, j] a[i, k] } } Solution(nat n, MATR(n) a, VEC(n) b: VEC(n) b ) {uniMat(n, a, b, n: VEC(n) b ) } uniMat(nat n, MATR(n) a, VEC(n) b, nat k: VEC(n) b ) {for(;;) { if (k = 1) return; subtrCol(n, a, b, k : MATR(n) a, VEC(n) b); k = k - 1 } subtrCol(nat n, MATR(n) a, VEC(n) b, nat k: MATR(n) a, VEC(n) b) {b = b for (i) {case 1..k-1: b[i] - b[k] a[i, k]}; a = a for (i, j) {case (1..k-1, k): 0 } }

17 На третьем этапе проведем подстановку следующую серию подстановок тел определений на место вызовов: perm -> diagEl; subtrLines, norm, diagEl -> Jord -> TriangleMatr -> Lin; subtrCol -> uniMat -> Solution -> Lin;

18 Lin(nat n, MATR(n) a, VEC(n) b: VEC(n) b : ) {for(nat k = 1; ; k=k+1) { if (a[k, k] != 0) #M1; nat m; for(m = k +1;;m = m + 1) { if (m>n) #2; if (a[m, k] != 0) break } b = b for (j) {case k: b[m] case m: b[k]}; a = a for (i, j) {case (k, k..n): a[m, j] case (m, k..n): a[k, j]} M1:b = b for (j) {case k: b[k] / c[k, k] }; a = a for (i, j) {case (k, k..n): a[k, j] / a[k, k]} b = b for (i) {case k+1..n: b[i] - b[k] a[i, k]}; a = a for (i, j) {case (k+1..n, k..n): a[i, j] - a[k, j] a[i, k] } if (k = n) break } for(nat k = n; k != 1; k = k - 1) { b = b for (i) {case 1..k-1: b[i] - b[k] a[i, k]}; a = a for (i, j) {case (1..k-1, k): 0 } } #1 }

19 Lin(nat n, MATR(n) a, VEC(n) b: VEC(n) b : ) {for(nat k = 1; ; k=k+1) { if (a[k, k] != 0) #M1; nat m; for(m = k +1;;m = m + 1) { if (m>n) #2; if (a[m, k] != 0) break } real t = b[k]; b[k] = b[m]; b[m] = t; for (nat j=k; k

20 Нетривиальным является устранение неиспользуемых вычислений : Lin(nat n, MATR(n) a, VEC(n) b: VEC(n) b : ) {for(nat k = 1; ; k=k+1) { if (a[k, k] != 0) #M1; nat m; for(m = k +1;;m = m + 1) { if (m>n) #2; if (a[m, k] != 0) break } real t = b[k]; b[k] = b[m]; b[m] = t; for (nat j=k; k

21 7. Технология предикатного программирования 7.5. Система автоматизации доказательства PVS

22 Система PVS Платформа: SUN 4(Spark) + Solaris, PC + Redhat Linux Реаизована: на Common Lisp, Lisp Allegro Окружение: редактор Emacs. Интерфейс с PVS реализован с помощью команд Emacs. Спецификация для PVS: набор файлов с расширением pvs, каждый файл содержит набор теорий Ассоциированные файлы: доказательство с раширением prf, бинарное представление с расширением bin, контекст Схема работы PVS - ввод спецификации в редакторе Emacs - parsing - typechecking - proving, набор команд для интерактивного доказательства, стратегии и тактики.

23 Описания типы, переменные, константы, формулы, утверждения (judgements), приведения Описания типов неинтерпретированные: T: TYPE T1, T2, T3: TYPE - типы разные; для использования в аксиомах // … // подтипа: S: TYPE FROM T s: TYPE FROM t s_pred: [t -> bool] s: TYPE = (s_pred) интерпретированные: T: TYPE = int intfun: TYPE = [int -> int] subrange(m, n: int): TYPE = { i: int | m

24 пустота – непустота типов NONEMPTY TYPE TYPE+ CONTAINING константы проверка непустоты типа Описания переменных x: VAR bool f: FORMULA (FORALL (x: int): (EXISTS (x: nat): p(x)) AND q(x)) области локализации переменной x Описания констант интерпретированные, неинтерпретированные n: int c: int = 3 f: [int -> int] = (lambda (x: int): x + 1) g(x: int): int = x + 1 эквивалентная форма

25 f: [int -> [int, nat -> [int -> int]]] = (LAMBDA (x: int): (LAMBDA (y: int), (z: nat): (LAMBDA (w: int): x * (y + w) - z))) эквивалентно f(x: int)(y: int, z: nat)(w: int): int = x * (y + w) - z Другая форма: x, y, w: VAR int z: VAR nat f(x)(y, z)(w): int = x * (y + w) – z смешанные формы

26 f(x: {x: int | p(x)}): int = x + 1 эквивалентно f(x: (p)): int = x + 1 эквивалентно f((x: int | p(x))): int = x + 1 odd: [nat -> bool] = (LAMBDA (n: nat): EXISTS (m: nat): n = 2 * m + 1) эквивалентная теоретико-множественная форма odd: [nat -> bool] = {n: nat | EXISTS (m: nat): n = 2 * m + 1}

27 Рекурсивные определения TCC – type consistency condition – условие совместимости типов Определяемая функция должна быть тотальной well-founded TCC – условие правильной организации функции factorial(x: nat): RECURSIVE nat = IF x = 0 THEN 1 ELSE x * factorial(x - 1) ENDIF MEASURE (LAMBDA (x: nat): x) terminationTCC мера (MEASURE) определяет функцию m(x) и порядок < Условие m(y) < m(x) выступает как обобщение механизма доказательства по индукции y = x - 1 factorial_TCC2: OBLIGATION FORALL (x: nat): NOT x = 0 IMPLIES x - 1 < x MEASURE x - более компактное определение меры MEASURE s BY

28 Макросы N: MACRO nat = 100 реализуется безусловная подстановка тела макроса на место любых его вхождений

29 Typechecking -- анализ семантической согласованности объектов спецификации Теория типов PVS алгоритмически неразрешима. Согласованость типов реализуется доказательством теорем, называемых TCCs - type-correctness conditions Теоремы TCCs прикрепляются к внутреннему представлению спецификации в bin-файле Статус теории: changed, parsed, typechecked, proved fac(n: nat): RECURSIVE nat = IF n = 0 THEN 1 ELSE n * fac(n - 1) ENDIF MEASURE n Function fac is well-typed if n /= 0 => n – 1 >= 0 (the argument is a nat) n /= 0 => n – 1 < n (termination). The type checker (M-x tc) generates type correctness conditions (TCCs)

30 Описания формул Виды формул: аксиомы (axioms), допущения (assumptions), теоремы (theorems) и утверждения- облигации (obligations) Команда lemma работает со всеми видами формул AXIOM, POSTULATE – аксиомы CHALLENGE, CLAIM, CONJECTURE, COROLLARY, FACT, FORMULA, LAW, LEMMA, PROPOSITION, SUBLEMMA, THEOREM - теоремы ASSUMPTION – допущения Свободные переменные – под квантором FORALL

31 Типы языка спецификаций PVS сильная типизация структурная эквивалентность Базисные типы: bool, number (real, rat, int, nat) - в стандартной библиотеке Subtypes: A: TYPE = {x: B | p(x)} Function types: [number -> number] Record types: [# flag: boolean, value: number #] Tuple types: [boolean, number] Enumeration types: {red, green, blue}

32 Подтипы A: TYPE = {x: B | p(x)} A: TYPE = (p) nat: TYPE = { n: int | n >=0 } subrange(n, m: int): TYPE = { i: int | n = 0 AND j > i)) можно записать короче FORALL (i:nat): (EXISTS (j:nat): j > i)) где определен в prelude.pvs следующим образом: naturalnumber: NONEMPTY TYPE = {i:integer | i >= 0} CONTAINING 0 nat: NONEMPTY TYPE = naturalnumber

33 existence TCC при наличии константы f: [ int -> {x:int | p(x)} ] с: f порождает existence TCC f_TCC1: OBLIGATION (EXISTS (x: int): p(x)) Чтобы гарантировать непустоту типа, применяется t: TYPE = {x: int | 0 < x AND x < 10} CONTAINING 1 Для леммы div_form: FORMULA (FORALL (x,y: int): x /= y IMPLIES (x - y)/(y - x) = -1) генерируется subtype TCC: div_form_TCC1: OBLIGATION (FORALL (x,y: int): x /= y IMPLIES (y - x) /= 0)

34 Типы функций Три эквивалентных формы: [t 1,..., t n -> t] FUNCTION[t 1,..., t n -> t] ARRAY[t 1,..., t n -> t] Тип предиката pred[t] и тип множества setof[t] есть тип [t -> bool]. Тип функции [t 1,...,t n -> t] есть подтип типа [s 1,...,s m -> s] t – подтип s, n = m и s i = t i для i =1,..., n. Генерируются TCC, называемые domain mismatch TCCs p,q: pred[int] f: [{x: int | p(x)} -> int] g: [{x: int | q(x)} -> int] h: [int -> int] eq1: FORMULA f = g eq2: FORMULA f = h

35 p,q: pred[int] f: [{x: int | p(x)} -> int] g: [{x: int | q(x)} -> int] h: [int -> int] eq1: FORMULA f = g eq2: FORMULA f = h Генерируются TCC: eq1_TCC1: OBLIGATION (FORALL (x1: {x : int | q(x)}, y1 : {x : int | p(x)}) : q(y1) AND p(x1)) eq2_TCC1: OBLIGATION (FORALL (x1: int, y1 : {x : int | p(x)}) : TRUE AND p(x1))

36 Типы произведения (tuples), n-ки [t 1,..., t n ], где t i – изображение типа (типовое выражение). Нульмерные тупли запрещены. (1, TRUE, (LAMBDA (x:int): x + 1)) – выражение типа [int, bool, [int -> int]]. Функции проекции: `1, `2,..., (или proj 1, proj 2,... ) i-ая проекция имеет тип [[t 1,..., t n ] -> t i ]. Тип тупля пустой, если тип одной из компонент пустой [t 1,..., t n -> t] и [[t 1,..., t n ] -> t] эквивалентны;

37 Тип записи [# a 1 : t 1,..., a n : t n #] a i – поле t i – тип поля (изображение типа). x a i – операция взятия поля Тип записи пуст, если тип одной из компонент пуст Порядок указания полей несущественен

38 Зависимые (dependent) типы Функции, тупли и записи могут быть зависимыми – одна из компонент может зависеть от предыдущих rem: [nat, d: {n: nat | n /= 0} -> {r: nat | r < d}] pfn: [d:pred[dom], [(d) -> ran]] stack: [# size: nat, elements: [{n:nat | n t] #] subp(i: int, (j: int | i >= j)): RECURSIVE int = (IF (i=j) THEN 0 ELSE (subp(i, j+1)+1) ENDIF) MEASURE i - j

39 Виды выражений Logic: TRUE, FALSE, AND, OR, NOT, IMPLIES, FORALL, EXISTS, = Arithmetic: +, -, *, /,, >=, 0; 1; 2; : : : Function application, abstraction ( -expression), and update Coercions - приведение Record construction, selection, and update Tuple construction, projection, and update: id WITH [(0):=42,(1):=12] IF-THEN-ELSE, COND: IF c THEN e1 ELSE e2 ENDIF CASES: COND c1->e1, c2->e2, c3->e3 ENDCOND Tables, Inductive definitions

40 IF-THEN-ELSE выражения IF cond THEN expr1 ELSE expr2 ENDIF полиморфное выражение АРИФМЕТИЧЕКИЕ выражения (0, 1, 2,... ), унарный -, ^, +, -, *, /. Числа имеют тип real. Неявные подтверждения (judgements) для чисел; 0 – является типа real, rat, int и nat;, >=. ПРИМЕНЕНИЯ ФУНКЦИЙ f(x) также, в инфиксной и префиксной нотации f(0)(2,3)

41 Операции (применения функций) Таблица приоритетов Операция Ассоциативность FORALL, EXISTS, LAMBDA, IN None | Left |-, |= Right IFF, Right IMPLIES, =>, WHEN Right OR, \/, XOR, ORELSE Right AND, &, &&, /\, ANDTHEN Right NOT, ~ None =, /=, ==,, >=, >, >=, Left WITH Left WHERE # Left ##, || Left +, -, ++, Left, /, **, // Left - None o Left :, ::, HAS TYPE Left [], None ^, ^^ Left ` Left

42 Связывающие (binding) выражения FORALL, EXISTS, LAMBDA Ламбда-выражения – безымянные функции (LAMBDA (x: int): x + 3) Подкванторные переменные могут быть зависимыми FORALL (x: int), (y: {z: int | x < z}): p(x, y)

43 LET и WHERE выражения LET x: int = 2, y: int = x * x IN x + y x + y WHERE x: int = 2, y: int = x * x значение = 6 для каждого выражения. транслируются в ламбда-выражения (LAMBDA (x: int) : (LAMBDA (y: int) : x + y)(x * x))(2)

44 SET выражения Множество есть предикат – функция типа [t -> bool], pred[t], или setof[t], (LAMBDA (x: t): p(x)) или {x: t | p(x)} - эквивалентны Tuple- выражение Выражение типа [t 1,...,t n ] имеет форму (e 1,...,e n ).

45 В ыражение проекции t: [int, bool, [int -> int]] ft: FORMULA t`2 AND t`1 > t`3(0) ft_deprecated: FORMULA PROJ_2(t) AND PROJ_1(t) > (PROJ_3(t))(0) В ыражение-запись Выражение (# a 1 := e 1,..., a n := e n #) имеет тип [# a 1 : t 1,..., a n : t n #], где e j имеет тип t j. все компоненты должны присутствовать Для зависимых типов R: TYPE = [# a: int, b: {x: int | x < a} #] r: R = (# a := 3, b := 4 #) генерируется недоказуемое TCC: 4 < 3.

46 Поле записи Переменная r имеет тип записи [# x, y: real #] Доступ к полю x реализуется конструкцией r`x или x(r ). Модификация структурного значения Override Expression для функций, записей и туплей identity WITH [(0) := 1, (1) := 2] (id WITH [(0) := 1]) WITH [(1) := 2] (LAMBDA x: IF x = 1 THEN 2 ELSIF x = 0 THEN 1 ELSE id(x)) R: TYPE = [# a: int, b: [int -> [int, int]] #] r1: R r2: R = r1 WITH [`a := 0, `b(1)`2 := 4] f WITH [(-1) |-> 0] с расширением области аргументов

47 Теории Specication ::= { Theory | Datatype } + Theory ::= Id [ TheoryFormals ] : THEORY [ Exporting ] BEGIN [ AssumingPart ] [ TheoryPart ] END Id TheoryFormals ::= [ TheoryFormal++',' ] TheoryFormal ::= [ ( Importing ) ] TheoryFormalDecl TheoryFormalDecl ::= TheoryFormalType | TheoryFormalConst TheoryFormalType ::= Ids : { TYPE | NONEMPTY TYPE | TYPE+ } [ FROM TypeExpr ] TheoryFormalConst ::= IdOps : TypeExpr

48 Пример теории groups [G : TYPE, e : G, o : [G,G->G], inv : [G->G] ] : THEORY BEGIN ASSUMING a, b, c: VAR G associativity : ASSUMPTION a o (b o c) = (a o b) o c unit : ASSUMPTION e o a = a AND a o e = a inverse : ASSUMPTION inv(a) o a = e AND a o inv(a) = e ENDASSUMING left_cancellation: THEOREM a o b = a o c IMPLIES b = c right_cancellation: THEOREM b o a = c o a IMPLIES b = c END groups IMPORTIHG groups[int, 0, +, -]

49 Алгебраические типы Abstract Datatypes Datatype ::= Id [ TheoryFormals ] : DATATYPE [ WITH SUBTYPES Ids ] BEGIN [ Importing [ ; ] ] [ AssumingPart ] DatatypePart END Id InlineDatatype ::= Id : DATATYPE [ WITH SUBTYPES Ids ] BEGIN [ Importing [ ; ] ] [ AssumingPart ] DatatypePart END id DatatypePart ::= { Constructor : IdOp [ : Id ] } + Constructor ::= IdOp [ ( {IdOps : TypeExpr }++',' ) ] datatype -- набор конструкторов с ассоцированными полями и распознавтелями

50 Алгебраические типы на примере списков list [T: TYPE]: DATATYPE BEGIN null: null? cons(car: T, cdr: list): cons? END list null и cons – конструкторы, null? и cons? – распознаватели, car и cdr – поля выражение CASES: length(s): RECURSIVE nat = CASES s OF null: 0, cons(x, y): length(y) + 1 ENDCASES MEASURE reduce_nat(0, (LAMBDA (x: T), (n: nat): n + 1)) Генерируются 3 теории: list_adt, list_adt_map и list_adt_reduce. Перечисления

51 Библиотеки теорий PVS Стандартная библиотека prelude.pvs booleans, numbers (real, rational, integer), strings, sets, including definitions and basic properties of finite and infinite sets, functions and relations, equivalences, ordinals, basic definitions and properties of bitvectors, mu calculus, LTL booleans: THEORY BEGIN boolean: NONEMPTY_TYPE bool: NONEMPTY_TYPE = boolean FALSE, TRUE: bool NOT: [bool -> bool] AND, &, OR, IMPLIES, =>, WHEN, IFF, : [bool, bool -> bool] END booleans

52 NASA Libraries algebra: groups, monoids, rings, etc analysis: real analysis, limits, continuity, derivatives, integrals calculus: axiomatic version of calculus complex: complex numbers co structures: sequences of countable length defined as coalgebra datatypes directed graphs: circuits, maximal subtrees, paths, dags float: floating point numbers and arithmetic graph theory: connectedness, walks, trees, Menger's Theorem ints: integer division, gcd, mod, prime factorization, min, max interval: interval bounds and numerical approximations lnexp: logarithm, exponential and hyperbolic functions lnexp_fnd: foundational definitions of logarithm, exponential and hyperbolic functions

53 NASA Libraries (cont) orders: abstract orders, lattices, fixedpoints reals: summations, sup, inf, sqrt over the reals, abs lemmas scott: Theories for reasoning about compiler correctness series: power series, comparison test, ratio test, Taylor's theorem sets_aux: powersets, orders, cardinality over finite sets sigma_set: summations over countably finite sets structures: bounded arrays, finite sequences and bags topology: continuity, homeomorphisms, connected and compact spaces, Borel sets/functions trig: trigonometry definitions, identities, approximations trig_fnd: foundational development of trigonometry: proofs of trig axioms vectors: basic properties of vectors while: Semantics for the Programming Language "while"