Тестирование в качестве доказательства разрешимости конструктивных задач

М. Джудакизаде, А. П. Бельтюков

Аннотация


Предлагается подход к решению конструктивных задач методом построения конструктивных доказательств их разрешимости, при котором доказательство оказывается программой, а его проверка — тестированием этой программы. При этом исчерпывающее тестирование проводится за конечное время. Более того, структура тестового комплекса автоматически выводится из структуры программы. Метод сочетает подходы Д. Гильберта, Ж. Эрбрана и Г. Генцена и является развитием трёхуровневой реализации логических формул. Для полного набора логических связок и кванторов позитивной логики предикатов без функций вводятся правила тестирования секвенций в нотации f:(Γ→B):f’, где f — обосновывающая конструкция (реализация), f’ — тестирующая конструкция. Для каждого правила явно описывается операционная семантика соответствующей программы.

Ключевые слова


Конструктивная логика, синтез программ, исчисление секвенций, реализуемость, универсум Эрбрана, тестирование, трёхуровневая реализация, дедуктивный синтез, временная сложность.

Полный текст:

PDF

Литература


Alur R. et al. Syntax-guided synthesis // 2013 Formal Methods in Computer-Aided Design. Portland: IEEE, 2013. P. 1–8.

Coquand T., Huet G. The calculus of constructions. INRIA, 1986.

Constable R. L. et al. Implementing mathematics // Nuprl Proof Development System. 1986.

Curry H. B., Hindley J. R., Seldin J. P. Combinatory Logic. Volume II. North-Holland Publishing Company, 1972.

Dijkstra E. W. Guarded commands, nondeterminacy and formal derivation of programs // Communications of the ACM. 1975. V. 18, No. 8. P. 453–457.

Gentzen G. Untersuchungen über das logische Schließen. I // Mathematische Zeitschrift. 1935. V. 39, No. 1. P. 176–210.

Gentzen G. Untersuchungen über das logische Schließen. II // Mathematische Zeitschrift. 1935. V. 39, No. 1. P. 405–431.

Gödel V. K. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes // Dialectica. 1958. V. 12, No. 3‐4. P. 280-287.

Gulwani S., Polozov O., Singh R. Program synthesis // Foundations and Trends in Programming Languages. 2017. V. 4, No. 1–2. P. 1–119.

Herbrand J. Recherches sur la théorie de la demonstration // J. Dziewulski, 1930. V. 33. P. 33–160.

Hilbert D., Ackermann W. Principles of mathematical logic // American Mathematical Soc., 1999. V. 69.

Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. V. 12, No. 10. P. 576–580.

Howard W. A. The Formulae-as-Types Notion of Construction. 1995.

Joudakizadeh M., Bel'tyukov A. P. Two-level realization of logical formulas for deductive program synthesis // Bulletin of Udmurt University. Mathematics. Mechanics. Computer Science. 2024. V. 34, No. 4. P. 469–485. EDN: JLCQGU.

Kleene S. C. On the interpretation of intuitionistic number theory // The Journal of Symbolic Logic. 1945. V. 10, No. 4. P. 109–124.

Kleene S. C. Introduction to Metamathematics. Van Nostrand, Princeton, 1952.

Kohlenbach U. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Berlin, Heidelberg: Springer, 2008.

Manna Z., Waldinger R. A deductive approach to program synthesis // ACM Transactions on Programming Languages and Systems. 1980. V. 2, No. 1. P. 90–121.

Martin-Löf P., Sambin G. Intuitionistic type theory. Naples: Bibliopolis, 1984. V. 9. P. 136.

Prawitz D. Natural deduction: A proof-theoretical study. Courier Dover Publications, 2006.

Sørensen M. H., Urzyczyn P. Lectures on the Curry-Howard isomorphism. Elsevier, 2006. Т. 149.




DOI: https://doi.org/10.54708/SIIT-2026-no2-p132

Ссылки

  • На текущий момент ссылки отсутствуют.


(c) 2026 М. Джудакизаде, А. П. Бельтюков