WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 | 2 ||

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

В двадцать первой главе перечислены основные результаты диссертационной работы, сведения об апробации и приложении этих результатов.

В Приложении даётся и анализируется результат специализации интерпретатора Машины Тьюринга по программе умножения натуральных чисел посредством суперкомпилятора SCP4.

Основные результаты.

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

2. На основе полуавтоматических процедур обобщения параметризованных конфигураций, представленных в работах В. Ф. Турчина [14], [16], [17], [19], разработаны и реализованы алгоритмы обобщения параметризованных конфигураций. Улучшены качественные характеристики этих алгоритмов с точки зрения построения более эффективных остаточных программ.

3. Разработан и реализован алгоритм построения выходных форматов компоненты факторизации F метадерева возможных вычислений в режиме online (по ходу дела суперкомпиляции); что позволяет сразу использовать построенный формат для специализации по нему как других компонент-функций, вызывающих функцию F, так и самой функции F. Показано, что на некоторых примерах этот алгоритм способен понижать временн сложность программы.

ую 4. Предложено понятие частично рекурсивного монома конкатенации.

Доказана теорема о достаточном условии частично рекурсивного монома конкатенации. Разработана стратегия выбора гипотезы мономиальности. На основании этих теоремы и стратегии разработан и реализован алгоритм, распознающий частично рекурсивные синтаксические мономы конкатенации. Показано, что на некоторых примерах этот алгоритм способен понижать временн сложность ую программы с экспоненциальной до константной O(1). Показано, что этот алгоритм может быть использован в решении задачи самоприменения для понижения порядка временн сложности ой результата самоприменения.

5. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме on-line [37].

6. Исследованы характеристики суперкомпилятора SCP4.

СПИСОК ЛИТЕРАТУРЫ [1] Конышев А. П. Компилятор из языка Рефал-графов в язык C: исходные тексты и демонстрация. 2000 [Электрон. ресурс]// http://www.botik.ru/pub/local/scp/refal5/.

[2] Корлюков А. В., Пособие по суперкомпилятору SCP4, 1999 [Электрон.

ресурс]// http://www.refal.net/supercom.htm.

[3] Корлюков А. В. Получение формул в математике.

// Тезисы докладов VIII Белорусской математической конференции, стр.178, 2000 [Электрон. ресурс]// http://www.bsu.by/Converences/konf8/Sections/Abstr14/Korlukov/Korlukov.htm.

[4] Корлюков А. В. Несколько примеров преобразований программ суперкомпилятором SCP4. 2001 [Электрон. ресурс]// http://www.refal.net/~korlukov/pearls/.

[5] Корлюков А. В. Суперкомпилируем суперагентов // Альфа, Т. 1, стр.89-98. Гродно: Гродненский государственный университет, 2001.

[6] Chmutov S. V., Gaydar E. A., Ignatovich I. M., Kozadoy V. F., Nemytykh A. P., Pinchuk V. A. Implementation of the symbol analytic transformation language FLAC // LNCS, Vol. 429, pp.276 / The Proc. of DISCO’90.

Springer-Verlag, 1990.

[7] Chmutov S. V., Nemytykh A. P., Gaydar E. A., Ignatovich, I. M., Kozadoy V. F., Pinchuk V. A. The symbol analytic transformation language FLAC: sources, executable modules, 1991. [Электрон. ресурс]// ftp://www.botik.ru/pub/local/scp/flac/flac386.zip.

[8] Ershov A. P. Mixed computation: potential applications and problems for study // Theoretical Computer Science, Vol. 18, pp.41-67.

[9] Futamura Y. Partial Evaluation of Computation Process – An Approach to a Compiler-Compiler // Systems. Computers. Controls., Vol. 2(5), pp.4550, 1971. (An updated version of the paper was republished in J. HigherOrder and Symbolic Computation, Vol. 12, pp.381-391, 1999.) [10] Glck R., Turchin V. F. Application of metasystem transition to function inversion and transformation // The Proc. of the ISSAC’90, pp.286-287.

ACM Press, 1990.

[11] Nemytykh A. P., Pinchuk V. A. Program Transformation with Metasystem Transitions: Experiments with a Supercompiler // LNCS, Vol.

1181, pp.249-260 / The Proc. of the Perspectives of System Informatics, Springer-Verlag, 1996. ftp://ftp.botik.ru/pub/local/APP/metatrans.ps.gz.

[12] Nemytykh A. P., Pinchuk V. A., Turchin, V. F. A Self-Applicable Supercompiler // LNCS, 1110, pp.322-337 / The Proc. of Partial Evaluation, International Seminar. Danvy o., Glck R., Thiemann P. (Eds.) SpringerVerlag, 1996. (ftp://ftp.botik.ru/pub/local/APP/self-appl.ps.gz).

[13] Turchin V. F. A supercompiler system based on the language REFAL // SIGPLAN Notices, Vol. 14(2), pp.46-54. 1979.

[14] Turchin V. F. The Language Refal, the Theory of Compilation and Metasystem Analysis // Courant Computer Science Report #20, New York University, 1980.

[15] Turchin V. F., Nireberg R., Turchin D. V. Experiments with a supercompiler // Conference Record of the ACM Symposium on LISP and Functional Programming, pp.47-55. ACM Press, 1982.

[16] Turchin V. F. The concept of a supercompiler // ACM Transactions on Programming Languages and Systems, Vol. 8, pp.292-325. ACM Press, 1986.

[17] Turchin V. F. The algorithm of generalization in the supercompiler // The Proc. of the IFIP TC2 Workshop, Partial Evaluation and Mixed Computation, 531-549. North-Holland Publishing Co., 1988.

[18] Turchin V. F. Refal-5, Programming Guide and Reference Manual.

Holyoke, Massachusetts: New England Publishing Co., 1989. (electronic version: http://www.botik.ru/pub/local/scp/refal5/, 2000).

[19] Turchin V. F. Metacomputation in the language Refal. 1990. (unpublished, private communication) [20] Turchin V. F. Program Transformation with Metasystem Transitions // J. of Functional Programming, Vol. 3(3), pp.283-313. 1993.

[21] Turchin V. F. Metacomputation: Metasystem transition plus supercompilation // LNCS, Vol. 1110, pp.481-509 / The Proc. of the PEPM’96.

Springer-Verlag, 1996.

[22] Turchin V. F. Supercompilation: Techniques and results // LNCS, Vol.

1181, pp.227-248 / The Proc. of Perspectives of System Informatics.

Springer-Verlag, 1996.

[23] Turchin V.F., Turchin D.V., Konyshev A.P., Nemytykh A.P.

Refal-5: sources, executable modules. [Электрон. ресурс]// http://www.botik.ru/pub/local/scp/refal5/, 2000.

ПУБЛИКАЦИИ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ [24] Лисица А. П., Немытых А. П. Работа над ошибками // Программные системы: теория и приложения. Т.

1, стр. 195-232, М: Физматлит, 2006. (доступна на ftp://www.botik.ru/pub/local/scp/refal5/psta_errors2006.pdf).

[25] Лисица А. П., Немытых А. П. Верификация как параметризованное тестирование (эксперименты с суперкомпилятором SCP4) // Программирование. Т. 33(1), стр. 22-43, M., 2007.

[26] Немытых А.П. Суперкомпилятор SCP4: Общая структура. M.: УРСС, 2007. 152 с.

[27] Korlyukov A. V., Nemytykh A. P. Supercompilation of Double Interpretation. (How One Hour of the Machine’s Time Can Be Turned to One Second) // Вестник национального технического университета „Харьковского политехнического института“, Т. 1, pp.123-150. Харьков, 2004. (электронная версия:

http://www.refal.net/~korlukov/scp2int/Karliukou_Nemytykh.pdf, исходные тексты и демонстрация:

http://www.refal.net/~korlukov/demo_scp4xslt.zip) [28] Lisitsa A., Nemytykh A. P. Verification of parameterized systems using supercompilation. A case study // The Proc. of the Third Workshop on Applied Semantics (APPSEM05) / Hofmann M., Loidl H.W. (Eds.), pp.1215. Fraunchiemsee, Germany. Ludwig Maximillians Universitat Munchen.

2005, September. Accessible via:

ftp://www.botik.ru/pub/local/scp/refal5/appsem_verification2005.ps.

[29] Lisitsa A., Nemytykh A. P. Towards verification via supercompulation // The Proc. of the 29th Annual International Computer Sofware and Applications Conference COMPSAC 2005 / Workshops and Fast Abstracts Volume, pp.9-10. IEEE 2005.

[30] Lisitsa A., Nemytykh A. P. Reachability Analysis in Verification via Supercompilation // The Proc. of the Satellite Workshops of DTL 2007 / TUCS General Publication, No. 45, Part 2, pp.53-67. Turku, Finland. June 2007.

[31] Lisitsa A., Nemytykh A. P. A Note on Specialization of Interpreters // LNCS, Vol. 4649, pp.237-248 / The Proc. of The 2-nd International Symposium on Computer Science in Russia. Springer, 2007.

[32] Nemytykh A. P. Supercompiler SCP4: Use of quasi-distributive laws in program transformation // Wuhan University Journal of Natural Sciences., Vol. 95(1-2), pp.375-382 / The Proc. of International Software Engineering Symposium. Wuhan, China. 2001, March.

[33] Nemytykh A. P. A Note on Elimination of Simplest Recursions // The Proc. of the ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp.138-146. ACM Press. Aizu, Japan. 2002.

[34] Nemytykh A. P. The Supercompiler SCP4: General Structure (extended abstract) // LNCS, Vol. 2890, pp.162-170 / The Proc.

of the Perspectives of System Informatics. Springer-Verlag, 2003.

(ftp://www.botik.ru/pub/local/scp/refal5/nemytykh_PSI03.ps.gz).

[35] Nemytykh A. P. Playing on REFAL // The Proc. of the International Workshop on Program Understanding, pp.29-39. Novosibirsk – Altai Mountains. July 2003.

(http://www.botik.ru/pub/local/scp/refal5/korlyukov.html).

[36] Nemytykh A. P. The Supercompiler SCP4: General Structure // Программные системы: теория и приложения Т. 1, стр.448-485. M.:

Физматлит, 2004. (ftp://ftp.botik.ru/pub/local/scp/refal5/GenStruct.ps.gz).

[37] Nemytykh A. P., Turchin, V. F. The Supercompiler SCP4:

sources, on-line demonstration. 2000. [Электрон. ресурс]// http://www.botik.ru/pub/local/scp/refal5/.

[38] Turchin V. F., Nemytykh A. P. Metavariables: Their implementation and use in Program Transformation // Technical Report CSc. TR 95-012. City College of the City University of New York, 1995.

Работа [25] опубликована в издании, входившем в перечень ВАК на момент публикации и имеющемся в перечне ВАК на данный момент. В этой статье автором разработан метод верификации параметризованных коммуникационных протоколов посредством суперкомпиляции интерпретаторов этих протоколов. Используя суперкомпилятор SCP4, автор успешно применил этот метод для верификации серии cache coherence протоколов.

В статье [24] автор показал, что разработанный им метод верификации параметризованных протоколов посредством суперкомпиляции может быть применён для поиска тестовых примеров, указывающих на ошибки в спецификациях.

В работах [28], [29] автором были заложены основы метода верификации, отмеченного выше.

Работа [26] является монографией автора диссертации.

В работе [27] автор показал, что использование суперкомпиляции для специализации двойной интерпретации может улучшить мультипликативную константу во временной сложности на три порядка.

В статье [30] автор построил формальную модель суперкопиляции, достаточную для успешной верификации некоторого класса параметризованных cache coherence протоколов.

В работе [31] автор показал, что верификацию коммуникационных протоколов можно рассматривать как специализацию их интерпретаторов по фиксированной части начальной конфигурации этих протоколов.

Здесь [37] представлены исходные тесты суперкомпилятора SCP4, реализованного автором.

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

Все остальные указанные работы были выполнены автором диссертации без соавторов.

Pages:     | 1 | 2 ||






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»