Верификация алголо-подобных программ методом индуктивных высказываний тема автореферата и диссертации по математике, 01.01.10 ВАК РФ

Введение. . . ».

• Глава I. Обзор литературы

Глава П. Логика программ.

§ I. Си®тема Хоара.

§ 2. Полнота системы Хоара.

§ 3. Модифицированная система Хоара.

Выводы..

Глава Ш. Контроль типов с использованием верификации программ.

§ I. Анализ поведения программы на совокупности типов данных.

§ 2. Система проверки правильности программ относительно структуры объектов.

§ 3. Пример построения вывода утверждения о программе.

§ 4. Непротиворечивость системы

Выводы.

Глава 17.Формализация предметных областей в автоматическом доказательстве.

§ I. Упрощающие стратегии.

§ 2. Пример формального описания: задача об испорченной" шахматной доске.

§ 3. Автоматическое доказательство.

Выводы.

Глава У. Машинный эксперимент.

§ I. Общая характеристика системы проверки утверждений о программах СПРУТ.

§ 2. Иллюстрация работы системы.

§ 3. Примеры верификации программ.

Выводы.

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

В развитии методов проверки правильности программ к середине 70-х годов были получены важные результаты, которые заложили основу для практических систем верификации. Были предложены различные способы формализации семантики языков программирования, разработаны языки спецификации программ и построены системы автоматического доказательства теорем на базе логики предикатов первого порядка.

Настоящая диссертация посвящена исследованию метода индуктивных высказываний, который состоит в следующем: в программе выбираются контрольные точки так, чтобы любой циклический путь проходил хотя бы через одну такую точку. Каждой контрольной точке сопоставляется логическое условие, называемое индуктивны м высказыванием , которое остается истинным при всех возвратах вычисления в эту точку программы. По программе с индуктивными высказываниями, входными и выходными условиями, строится конечное множество логических формул, называемых условиями правильности, тождественная истинность которых равносильна правильности программы.

В главе I дан обзор современного состояния верификации программ методом индуктивных высказываний.

В главе П описывается система Хоара для верификации ал-голо-подобных программ. Исследуются логические свойства этой системы.

В главе III рассматривается проверка правильности программ относительно структуры объектов. Описывается формальная система, средствами которой осуществляется контроль типов в алгол о-подобных программах, не содержащих описании значений переменных.

В главе 1У исследуется способ формального описания предметных областей на основе прикладного исчисления предикатов первого порядка. Описывается организация автоматического доказательства теорем в рамках выбранных средств.

В главе У дается характеристика практической системы верификации программ, реализованной с помощью языка программирования Лисп. Приводится иллюстрация ее работы.

В заключение приведем основные защищаемые положения диссертации:

1. Доказательство свойства полноты системы Хоара, не содержащей рекурсивных процедур, относительно арифметики.

2. Построение аксиоматической системы для проверки правильности программ относительно структуры объектов, не требу щей сопоставления индуктивных высказываний циклам. Доказательство свойства непротиворечивости данной системы.

3. Разработка способа формализации предметных областей программ на основе исчисления предикатов первого порядка, использующего аксиоматику процедурного характера для повышения эффективности автоматического доказательства теорем.

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

Материалы диссертации опубликованы в работах:

1. Черноброд Л.В. Правильность и эквивалентность программ.-Программирование, 1976, J3 6, с. 16-25.

2. Черноброд Л.В. Проверка правильности программ: формализация операций над множествами.- В сб.: Теория и практика системного программирования, Новосибирск, Б.й., 1977, с. 86-94.

3. Черноброд Л.В. Решение с помощью ЭВМ задачи об "испорченной" шахматной доске.- В сб.: Языки и системы программирования, Новосибирск, Б.и., 1979, с. 37-46.

4. Черноброд Л.В. Система проверки утверждений о программах СПРУТ.- Новосибирск, Б.и., 1980,- 42 с. (Препринт/ВЦ СО АН СССР; 223).

5. Черноброд Л.В. О контроле типов значений переменных с использованием доказательства свойств программ.- Программирование, 1982, IS 4, с. 14-24.

6. Черноброд Л.В. Верификация программ в системе СПРУТ,- В сб.: Первый чехословацко-советский семинар молодых ученых по математической информатике, Смоленице, Чехословакия, 1980, с. 47-54.

Выводы

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

ЗАКЛЮЧЕНИЕ

Приведем основные результаты диссертационной работы.

1. Доказана теорема о полноте системы Хоара относительно арифметики для структурированных программ, не содержащих рекурсивных процедур.

2. Предложен подход к повышению эффективности процесса ве-рификацил программ методом индуктивных высказываний посредством введения ограничений на совокупность анализируемых свойств программ. В качестве иллюстрации рассмотрена проверка правильности программ относительно структуры объектов. На совокупность анализируемых структур данных программ наложены ограничения, принятые в глобальном анализе. Построена аксиоматическая система, представляющая собой вариант логики Хоара, которая позволяет проводить верификацию программ без привлечения инвариантов циклов пользователя. Доказана теорема о непротиворечивости этой системы.

3. Выполнено расширение метода описания предметных областей программ на основе прикладного исчисления предикатов первого порядка упрощающими стратегиями процедурного характера, что позволило повысить эффективность автоматического доказательства. В качестве иллюстрации рассмотрена формализация задачи об "испорченной" шахматной доске из области искусственного интеллекта, пригодная для ее решения с помощью ЭВМ.

4. Реализована практическая система верификации программ. Построена система правил вывода для нахождения условий правильности аннотированных программ, записанных на входном языке сисусловий теглы. Разработаны алгоритмы автоматического доказательств^правильности с использованием элементарных преобразований, упрощающих стратегий и преобразований кванторов. Выполнено программирование отдельных частей системы и ее отладка, проведены машинные эксперименты по проверке правильности программ, подтвердившие работоспособность системы.

1.Hoare C.A.R. An axiomatic basis for computer programming.-GACM, 1969,v. 12,no 10, p. 576-583.

2. Floyd R.W. Assigning meaning to programs.-Proc. of American Society Symposia in Applied Math., 1967, v. 19,p.13-31.

3. Luckham D.C., Suzuki IT. Automatic program verification IV: Proof of termination within a weak logic of. programs.-Acta Informatica, 1977, v. 8, no. 1, p. 21-36.

4. Manna Z., Pnueli A. Formalization of properties of functional programs. Jacm,1970, v. 17, no. 3, p. 555-569.•Dijkstra E.W. A discipline of programming. Prentice-Hall Inc.,1976 (перевод: Дисциплина программирования.1. M.: "Мир", 1978).

5. Morris J.D., V/egbreit В. Subgoal induction. CACM, 1977, v. 20, 20, no. 4, p. 209-222.

6. Manna Z., Waldinger R. Is "sometimes" sometime better then "always"? Intermittent assertion in proving program correctness. CACM, 1978, v. 21, no 2, p. 159-172.

7. Clint M., Ho are C.A.R. Program proving: Jumps and functions.- Acta Informatica, 1972, v. 1 , p. 214-224.

8. Kovmltowski T. Axiomatic approch to side effects and general jumps. Acta Informatica, 1977, v. 7, p. 357-360. ■

9. Hoare C.A.R., V/irth 1. An axiomatic definition of the programming languagee Pascal. Acta Informatica, 1973» v. 2, p. 335-355.

10. Luckh.am D.C., Suzuki IT. Verification oriented proof rules for arrays, records, and pointers. Report SAIIj Lie mo AII.I-278, 1976, Stanford University.

11. Cartwright R., Oppen D. Unrestricted procedure calls in Hoare's logic. Proc. of the 5th АСЫ Symposium on Principles of Programming Languages, 1978, ITevr York,p. 131-140.

12. Ноаге. C.A.R. Proof of correctness of data representations. -Acta Informatica, 1972, v. 4, p. 271-281.

13. Cook S.A. Axiomatic and interpretive semantics for an Algol fragment. Comput. Sci. Dept., Univ. of Toronto, TR 79, 1975.

14. Cook S.A. Soundness and completeness of an axiom system for program verifications. SIAI.I J. Comput., 1978, v. 7, no 1, p. 70-90.

15. Черноброд Л.В. Правильность и эквивалентность программ.

16. Программирование, 1976, J8 6 с. 16-25.

17. Lipton R.J. A necessary and sufficient condition for theexistence of Hoare logics. Proc. 18th IEEE symp. on Foundations of Computer Science, Providence,R.J., 1977, p. 268-283.

18. Apt K.R. Ten years of Hoare's logic: a survey. Part I.

19. ACM Trans, on Progr. Lang, and Syst., 1981, v. 3, no 4, p. 431-483.

20. Goldblatt R. Axiomatising the logic of computer programming.- Lecture Notes in Computer Sci., 130, 1982, Springer Verlag.27. de Bakker J.Y/. Mathematical theory of program correctness.- Prentice — Hall, Englewood Cliffs, IT.tJ 1980.

21. Clarke E.LI. Programming language constructs for which it isimpossible to obtain good Hoare-like axiom systems. -Proc. 4th AC1.I Symp. on Principles of Programming Languages, 1977, p. 10-20.

22. V/irth IT. The development of programs by stepwise refinement.- САСЫ, 1971, v. 14, no 4, p. 221-227.

23. Good D.I., Ragland L.C. ITucleus a language of provableprograms. Program Test Methods , V/. Iletzel ed., Prentice - Hall, Englewood Cliffs, 1T.Y., 1973.

24. Wirth IT. Liodula: A language for modular multiprogramming.1.: Software Praxis and Experience, 1977, no 1, p. 3-87.

25. Lampson B.Y/., I-Io'rning J. J., London R.L. ,Mitchell J.G.,

26. Popen G.J. Report on the programming language Euclid. -SIGPLAH notices, 1977, v. 12, no 2, p. 1-79.

27. Y/ulf Y/.A. , London R.L., Shaw Iu. An introduction to the construction and verification of Alphard programs. IEEE Trans, on Software Engineering, SE-2, 4, 1976, p.253-2S5<

28. Ashcroft E.A. , Wadge V/.Y/. Lucid, a nonprocedural languagewith iteration. САСЫ, 1977, v. 20, no 7, p. 519-526.

29. Лавров G.C. Методы задания семантики языков программирования.- Программирование, 1978, & 6, с. 3-10.

30. Kiiig J., Floyd R.Y/. An interpretation oriented theoremprover over integers. Journal of Computer and System Sci., 6, 1972, p. 305-323.

31. Good D.L., London R.L.^ Bledsoe Y/. W. An interactive programverification, system. IEEE Trans, on Software Engineering-, SE-1, 1975, p. 59-67.

32. Igarashi S., London R.l., Luckham D.C. Automatic program verification I"; Logical basis and its implementation. -Acta Informatica, 1975, v. 4, no 2, p. 145-182.

33. Scholz S., Herrlich 0. Bemerkungen zur Generierung von Verifikationsbedingungen in Pascal Programmen. - Bei-trage. 1 izur K2TYA7T - Konferenz, Llethodik der Programmie-rung mid Programmverif illation, Teil 2, 1977, Dresden, p. 71-88.

34. Летичевский A.A., Костырко B.C. О использовании машин МИР-2для анализа программ.- Кибернетика, 1974, й 6, с. 31-40.

35. Непомнящий В.А., Черноброд Л.В. О проверке правильностипрограмм с помощью ЭВМ. В сб.: Проблемы программирования, Новосибирск, В.и., 1976, с. 63-80.

36. Gerhart S.L., blusser D.R. et al. An overview of AFFIRL1 :

37. A specification and verification system. Information Processing 80, Tokyo, 1980, p. 343-348.

38. Hoare C.A.R. Proof of program ШГО, САСЫ, 1971, v. 14, no 1,p. 39-45.

39. Henke von F.W., Luckham D.G. A methodology for verifyingprograms. Proc. of the Intern. Conf. on Reliable ■ Software, Los Angeles, 1975, p. 156-164.

40. Suzuki II. Verifying programs by algebraic and logical reduction. Proc. of Intern. Conf. on Reliable Software, Los Angeles, 1975, p. 473-481.

41. Непомнящий B.A., Чурина Т.Г. Верификация программ сортировки массивов.- В сб.: Языки и системы программирования, Новосибирск, Б.и., 1979, с. 21-36.

42. Непомнящий В.А. Доказательство правильности программ линейной алгебры.- Программирование, 1982, $ 4, с. 63-72.

43. V/a Iker B.J., Kemmerer R.A., Popek G.J. Specification andverification of the UCLA Unix Security. CACII, 1980, v. 23, no 2, p. 118-131.

44. Polak V/. Compiler specification and verification. Lecture .1.otes in Computer Sci.,124, 1981 , Springer Verlag.

45. London R.L. A view of program verification. Proc. of the1.tern. Conf. on Reliable Software, Los Angeles, 1975, p. 534-545.5J. Luckham D.C. Program verification and verification oriented programming. Information Processing 77, Toronto, 1977, p. 783-793.

46. Schwartz J.Т. A survey of program technology. Report no 1,1.ev; York University, 1978.

47. Плюшкявичюс P.A., Плюшкявичене АЛО., Гячас К.К., Мисявичюте Л.А., Сакалаускайте Ю.В., Жалдокас Р.А. О верификации программ.- В кн.: Тезисы докладов и сообщений к всесоюзной конференции, ч. I, 1980, Вильнюс, с. 34-56.

48. Barzdin J.M. The problem of reachibility and verification0£ program. Lecture Notes in Computer Sci., 74, 1979, Springer - Verlag, p. 13-25.

49. Wegbreit B. The synthesis of loop predicates. САСЫ, 1974,v. 19, no 4, p. 102-112.

50. Katz S., Manna Z. Logical analysis of programs. CACM,1976, v. 19, no 4,p. 188-206.

51. German S. Automating proofs of the absence of common runtime errors. Proc. of thr 5th ACM Symposium on Principles of Progr. Languages, 1978 , lev/ York, p. 105-118.58.- Мальцев А.И. Алгоритмы и рекурсивные функции.- М.: Наука,1965.

52. Черноброд Л.В. Проверка правильности программ: Формализацияопераций над множествами.- В сб.: Теория и практика системного программирования, Новосибирск, Б.и., 1977, с. 86-94.

53. Черноброд Л.В. О контроле типов значений переменных с использованием доказательства свойств программ.- Программирование, 1982, 4, с. 14-24.

54. Kaplan М.А., Ullman J.D. A general scheme for the automaticinference of variable types. J. of АСЫ, 1980, V. 27, no 1, p. 128-145.

55. Ершов А.П. Об операторных схемах Янова,- В кн.: Проблемыкибернетики, вып. 20, М.: Наука, 1967, с. 181-200.

56. Лавров С.С., Силагадзе Г.С. Автоматическая обработка данных. Язык Лисп и его реализация.- М.:■Наука, 1978.

57. Guttag J.У., Horning J.J. The algebraic specification ofabstract data types. Acta Informatica, 1978, v. 10, no 1, p. 27-52.

58. Tenenbaum A.M. Type definition determination for very highlevel languages. Report ITSO-3, Courant Institute of Math.Sci., ITew York University, 1974.

59. Schwartz; J.T. Automatic data structure choice in a languageof very high level. CACM, 1975, v.18,no 12, p. 722-72E

60. Черноброд Л.В. Решение с помощью ЭВМ задачи об "испорченной"шахматной доске. В сб.: Языки и системы программирования, Новосибирск, Б.и., 1979, с. 37-46.

61. McCarty J. A tough nut for proof procedures. Report SAIP

62. Memo 16, Stanford University, 1964.

63. Рафаэл Б. Думающий компьютер. М.: Мир, 1979.

64. Генцен Г. Исследования логических выводов.- Математическаятеория логического вывода, М.: Наука, 1967, с. 9-74.

65. Кангер С. Упрощенный метод доказательства .для элементарнойлогики.- В кн.: Математическая теория логического вывода, М.: Наука, 1967, с. 200-207.

66. Бет Э. Метод семантических таблиц.- В кн.: Математическаятеория логического вывода, М.: Наука, 1967, с. I9I-I99.

67. Schwartz J.Т. On programing. An interim report of the

68. SETL project, Part I,II. Courant Institute of I,lath. Sci.,New York University, 1975.

69. Левин Д.Я. Сетл язык проградлмирования весьма высокого уроня. Программирование, 1976, J& 5, с. 3-9.

70. Левин Д.Я. Система СЕТЛ. Новосибирск, Б.и., 1978, - 25 с.

71. Препринт/ВЦ СО АН СССР; 139).

72. Городняя Л.В. Описание языка программирования Лисп и интерпретирующей системы, реализованной в ВЦ СО АН СССР. Отчет ВЦ СО АН СССР, Новосибирск, 1973.

73. Курляддчик Я.М. Индивидуально-групповой текстовый архив суниверсальным выходом.- Материалы 1У кони, по эксплуатации вычислительной машины БЭСМ-6, Тбилиси, 1977, с. 83-91.

74. Черноброд Л.В. Система проверки утверждений о программах

75. СПРУТ). Руководство к пользованию. Отчет ВЦ СО АН СССР,- Новосибирск, 1978.

76. Черноброд Л.В. Система проверки утверждений о программах

77. СПРУТ.- Новосибирск, Б.и., 1980,- 42 с. (Препринт/ ВЦ СО АН СССР; 223).

78. Черноброд Л.В. Верификация программ в системе СПРУТ.- Всб.: Первый чехословацко-советский семинар молодых ученых по математической информатике, Смоленице, Чехословакия, 1980, с. 47-54.