О термальном аспекте автоматизации программирования

Уточняются основные положения немонотонного синтеза программ с переприсваиваниями. Такой синтез рассматривается с использованием теоретико-модельного подхода. Для изучения программистской и декларативной семантики предлагается использовать многоосновные алгебры термов при представлении опер...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2006
1. Verfasser:	Приходько, П.П.
Format:	Artikel
Sprache:	Russisch
Veröffentlicht:	Інститут програмних систем НАН України 2006
Schlagworte:	Теоретичні та методологічні основи програмування
Online Zugang:	https://nasplib.isofts.kiev.ua/handle/123456789/2325
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:	О термальном аспекте автоматизации программирования / П.П. Приходько // Проблеми програмування. — 2006. — N 1. — С. 3-16. — Бібліогр.: 11 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

_version_	1860246335532302336
author	Приходько, П.П.
author_facet	Приходько, П.П.
citation_txt	О термальном аспекте автоматизации программирования / П.П. Приходько // Проблеми програмування. — 2006. — N 1. — С. 3-16. — Бібліогр.: 11 назв. — рос.
collection	DSpace DC
description	Уточняются основные положения немонотонного синтеза программ с переприсваиваниями. Такой синтез рассматривается с использованием теоретико-модельного подхода. Для изучения программистской и декларативной семантики предлагается использовать многоосновные алгебры термов при представлении операций над данными в синтезируемых программах. Для изучения путей эффективного автоматического синтеза программ применяются сети Петри. Уточнюються основні положення немонотонного синтезу програм з переприсвоюваннями. Такий синтез розглядається з використанням теоретико-модельного підходу. Для дослідження прорамістської та декларативної семантики запропоновано використовуати многоосновні алгебри термів при представленні операцій над даними в програмах, що синтезуються. Для дослідження шляхів ефективного автоматичного синтезу програм використовуються мережі Петрі. Substantive provisions of nonmonotonic synthesis of programs with reassignments are specified. Such synthesis is considered with use of the approach with models theory. For studying programmer and declarative semantics it is offered to use the multibasic algebras of terms at representation of operations above the data in synthesized programs. Petri nets are applied to studying ways of effective automatic synthesis of programs.
first_indexed	2025-12-07T18:37:04Z
format	Article
fulltext	Теоретичні та методологічні основи програмування © П.П. Приходько, 2006 ISSN 1727-4907. Проблеми програмування. 2006. № 1 3 УДК 681.3.06 П.П. Приходько О ТЕРМАЛЬНОМ АСПЕКТЕ АВТОМАТИЗАЦИИ ПРОГРАММИРОВАНИЯ Уточняются основные положения немонотонного синтеза программ с переприсваиваниями. Такой синтез рассматривается с использованием теоретико-модельного подхода. Для изучения программистской и дек- ларативной семантики предлагается использовать многоосновные алгебры термов при представлении опе- раций над данными в синтезируемых программах. Для изучения путей эффективного автоматического син- теза программ применяются сети Петри. Введение В исследованиях и практических раз- работках по автоматизации программирова- ния приходится обращать особое внимание на его термальный аспект [1, с. 25 -28]. Ведь практическая ценность какой-либо програм- мы определяется прежде всего ее соответст- вием некоторой проблемной области. Всякий практически ценный результат выполнения программы является конструктивным объек- том в такой области. Из [2, с.15-22] следует, что конструктивность объекта может истол- ковываться как возможность его представле- ния некоторым термом. Рассмотрим выполнение программы как процесс построения такого терма. Будем отслеживать соответствие между составляю- щими указанной проблемной области и кон- струкциями образуемого терма. Это даст воз- можность исследовать механизм соотнесения программистской семантики и семантики проблемной области. Программа образуется как следствие такого соотнесения. Эффектив- ность автоматизации программирования оп- ределяется эффективностью воспроизведения указанного механизма. Покажем возможные подходы к такому воспроизведению. 1. Основные понятия и определения Используем определения и обозначе- ния, упоминавшиеся или предложенные в [3]. Составляющие какой-либо предметной об- ласти конкретной программы будем пред- ставлять тройкой ( )X , ,ε X , где X - множест- во программных объектов; { }ε = ∈E x Xx : - семейство частично упорядоченных мно- жеств значений этих объектов ( )Ex x x X ,⊆ ∈ ; X - булева алгебра множеств - наборов про- граммных объектов. Состояния наборов программных объ- ектов представляют элементы множества ( ) ( ){ }W W X C C ≡ = ∪ ∈∏, , :ε εX X , для которых установлено отношение частич- ного порядка ⊆: для ( )u v W X, , ,∈ ε X ( ) ( )( )u v X X x X u x v xu v u x⊆ ⇔ ⊆ ∀ ∈ ⊆& . Это отношение индуцирует на W операции взятия точных верхней и нижней граней, а также отношения равенства и строгого по- рядка. Возможные состояния моделируемого объекта представляют элементы множества ( ) ( ),,,,, XX εε XWXWW возмвозм ⊆≡ (1) удовлетворяющего следующему условию: { } ( ).,, &: wW wvWvvWw возм возм ⊆∩∪∈∩∪∃ ⊆∈⊆∀∈∀ UUUU U (2) При этом для A X⊆ ( ) ( ) ( ){ },&,,: ,,, AXXWww AXWAW w Df ⊆∈= =≡ X X ε ε ( ) ( ) ( ){ },&,,: ,,,** AXXWww AXWAW w Df =∈ =≡ X X ε ε ( ) ( ) ( ){ },&,,: ,,, AXXWww AXWAW w Df ⊇∈ =≡ X X ε ε ( ) ( ) ( ) ,,,, ,,, возм Df возмвозм WAXW AXWAW ∩= =≡ X X ε ε Теоретичні та методологічні основи програмування 4 ( ) ( ) ( ) ,,,, ,,, * ** возм Df возмвозм WAXW AXWAW ∩= =≡ X X ε ε ( ) ( ) ( ) .,,, ,,, возм Df возмвозм WAXW AXWAW ∩ =≡ X X ε ε Средой поддержки программ (СПП), как и в [3], будем называть пятерку ( )X Wвозм, , , , ,ε µX где ( )X , ,ε X – пред- ставление составляющих предметной области описанного выше вида; Wвозм – множество возможных состояний наборов программных объектов вида (1)-(2); µ – конечное множест- во процедурных представлений отношений, выражающих знания о предметной области функциями вида ( ) ( )f W A W Bf f: ,* → где A Bf f, ,∈X а ( ) ( ) ( ),:, * wfwfwwAWww fвозм ′′⊆′′′⊆′∈′′′∀ причем для B f установлено его единствен- ное разбиение на наборы ′ ′′ ∈B Bf f, X , для которых B B Bf f f= ′ ∪ ′′, ′ ∩ ′′ = ∅B Bf f и ( )∀ ∈ ∃ ∪       ∈′′w W A w f w Wвозм возмf B f A f . Будем использовать следующие обо- значения. Пусть для любой СПП ( )X Wвозм, , , , ,ε µX функции f ∈µ и со- стояния ( )w W X∈ , ,ε X ( )F w f w если w W A w для всех остальных w f fB Aff возм≡ ∪       ∈     ′′ , , а для множества µ { }U + Df nn Z∈= :* µµ , { }U N∈=+ nn Df :µµ , { }µ λ0 = Df , где λ – отсут- ствие символа, и для цепочки символов f f df =    =f i i j , ,1 и f = df j , а для натуральных m,n [ ] ( )f m df f i i m j = = , , , если m j≤ , и [ ] ( )f n df fi i n= =, ,1 , если n j≤ , а [ ] ( )f m n df fi i m n= =, , , если m n j≤ ≤ , и ( )f i Df if= для натурального i ≤ f , а ( ) ( ){ }.&&: fff ≤∈== iiffr iDf N Пусть при этом для ( )w W X∈ , ,ε X ( )G w w Df λ , ,= (3) а для f ∈µ* ( ) [ ]G w G F w Df ff f, ,=       2 1 (4) и ( ) [ ]( )G w F G w D n f fn f f, , ,= −1 (5) если f ≤ 2, и ( )G ,w F w Df ff = (6) для f ∈µ . Для какой-либо цепочки функ- циональных символов f ∈µ* { },:U ff ≤∈= i&iAA ifDf N { },:U ff ≤∈= i&iBB ifDf N { },:U ff ≤∈′′=′′ i&iBB ifDf N ′ = ′′B B B Dff f f\ , [ ] ,:\ 1U       ≤∈= − f ff &iiBAA iifDf N причем A A Bλ λ λ= = = ∅ . Все данные о со- стоянии объекта, моделируемого СПП ( )X Wвозм, , , , ,ε µX которые можно полу- чить исходя из определенного состояния на- бора программных объектов ( )w W X∈ , ,ε X , представляет выражение ( )F G w Df Bµ µ= ∈         ′′f f f , : .U Выполнение любой программы, под- держиваемой в какой-либо СПП ( )возмWX ,,,, µε X , представляется цепочкой функциональных символов-элементов µ , со- ответствующих действиям программы в их очередности. Теоретичні та методологічні основи програмування 5 Для каких-либо f , g ∈µ и N∈n при n ≤ f ( )( ( ( ) [ ] ) [ ] .\& \&& 1:&1& &&, 1 1 11 1 ,1 1 1   ∅≠′′∅≠ ≠′′∩< ≤<∈∀+−≤ =⇔ + − +− − = − LmLg km km BB BBAmm LkknL nmf kgkg Lkkm kk n f f f =g N fg[ Результат выполнения последователь- ности действий, представляемых цепочкой функциональных символов f ∈µ, заведомо не зависит от выполнения n-го действия, если не существует цепочки g ∈µ, для которой g f[ n ( теорема 3 в [3] ). Обозначим S совокупность всех цепо- чек из µ, в которых нет звеньев, представ- ляющих действия, заведомо не влияющие на конечный результат выполнения соответст- вующих последовательностей действий: { gff µµ ∈∃<∈∀∈≡ nn Df :&: NfS }.fg n [ Для каких-либо A B, ∈X обозначим ( )z A B, совокупность всех цепочек из S , представляющих последовательное опреде- ление состояния набора программных объек- тов B исходя из данных о состоянии набора A: ( ) { &&&:, ffff BBAABA Df ′⊆⊆∈= Sz ( &::& ff ≤∈∃≤∈∀ kknn NN [ ] ) ( ::\& 1 N∈∃∈∃∅≠′′ − mBA k k ff g µ )( )},& ∅≠∩′= BBgf nn gfg k [ через ( )Z A B, обозначим совокупность цепо- чек из ( )z A B, , каждая из которых включает все функциональные символы, входящие в цепочки из ( )z A B, , т.е. ( ) ( ){ &,:, BABA Df zZ ∈= ff ( ) ( ) ( )},,& fgg rrBA ⊆∈∀ z а ( )Z1 A B, – совокупность цепочек из µ, представляеющих первые или единственные вхождения функциональных символов в со- ответствующую цепочку из ( )Z A B, : ( ) { ( ) ( ) ( ) ( ) ( )&,&&& &&:, ,1 1 g df =fffgf gff = == ∈∈= jj f frrr A,BBA D ZZ µ ( )(( ⇒=<∈∃≤∈∀ ji ggjiigjj &::& NN ) ( )( ⇒≠<∈∀=⇒ jij ggjiif :& Nλ ))}.jj gf = В [3] показано, что знания о проблем- ной области, представляемые СПП, можно использовать для построения программ, а существование непустого множества ( )Z1 A B, составляет необходимое условие возможно- сти построения программы определения зна- чений параметров, соответствующих набору программных объектов B, исходя из значений входных параметров, соответствующих набо- ру A. 2. Математические представления про- граммистской семантики Суть предыдущего раздела заключает- ся в том, что в СПП функциональные симво- лы представляются вместе с их интерпрета- циями, выражающими все знания о свойствах соответствующих исполнимых программных составляющих. В [3] привлекаются только важнейшие свойства, которые определяют очередность выполнения действий и соотнесение с управ- ляющими операторами. Соответственно про- граммистская семантика представлена лишь функциональностью отношений и наличием “затираемых” или “дописываемых” значений. Соответственно, абстрагируясь от второсте- пенных обстоятельств, были получены отве- ты на основные вопросы. Сохраняя приемле- мый уровень абстрагирования, используем адекватные формализмы для представления программистской семантики в ее термальном аспекте. Отработанным и удобным средством для формализованного представления преоб- разований данных в программах признаны Теоретичні та методологічні основи програмування 6 многоосновные алгебры [4]. Как и в [4], под семейством α объек- тов-элементов какого-либо класса A будем понимать функциональное отношение между элементами некоторого множества S и объек- тами-элементами A. При этом α называется S-индексированным семейством: ( )α α= ∈s s S, . Под сигнатурой понимают пару ( )S , ,Ω где S – множество имен основ; Ω – S S* × -индексированное семейство множеств знаков операций. Тогда многоосновной ал- геброй сигнатуры ( )Σ Ω= S , можно назвать тройку ( )M , , ,Σ r где ( )M M= ∈ df Sα α, – се- мейство множеств, называемое носителем ал- гебры; ( )r s s s s S S = →      ∈ ×αu u u: , , Ωu M M – семейство функций, а M Mu u u =       =∏ df ii , ,1 . Сигнатура в значительной степени оп- ределяет важные свойства многоосновной алгебры. Для каждой заданной сигнатуры ( )Σ Ω= S , определяются алгебра базисных термов WΣ с этой же сигнатурой Σ , в кото- рой для каждой основы s S∈ ( )( )Ω Ω Σs s s W≡ ⊂λ M , а для кортежа основ u ∈S и функциональ- ного символа ω ∈Ωus , кортежа базисных термов ( )( )t u ∈ M WΣ ( ) ( )( )' ' ,ω t ∈ M W sΣ ( )( )( ) ( )α ω ωu t ts =' ' . Если задано еще и S-индексированное семей- ство множеств переменных X , то определяет- ся алгебра термов с переменными ( )W XΣ также с сигнатурой Σ и для каждой основы s S∈ ( )( )( )X W Xs s∪ ⊂Ω ΣM , а для кортежа основ u ∈S* и функциональ- ного символа ω ∈Ωus , кортежа термов с пе- ременными ( )( )( )t u ∈ M W XΣ ( ) ( )( )( )' ' ,ω t ∈ M W X sΣ ( )( )( ) ( )α ω ωu t ts =' ' . Наличие функций оценки, сопостав- ляющих переменным их значения, позволяет определить интерпретации для таких термов, “интерпретированные” алгебры термов, уста- навливающие для термов с переменными значения базисные термы и элементы мно- жеств семейства-носителя. Для какой-либо определенной сигнатуры ( )Σ Ω= S, и S- индексированного семейства множеств X к множеству ( )I W XΣ, относится всякая мно- гоосновная алгебра ( )M , , ,Σ r для которой ( )( )M M= W XΣ , ( )r df s s s s S S = →      ∈ ×αu u u: , , Ωu M M и существует семейство функций ( )( )( ) ( )( )r r M M= →     ∈s s s s SW X W: , ,Σ Σ для которых ( ) ( )( )r Ms s s X W⊆ Σ и ( )rs t t= для ( )( )t W s ∈ M Σ , а для u ∈S , функцио- нального символа ω ∈Ωus и кортежа ( )( )t u ∈ M WΣ ( )( ) ( )( ) ( )( )( ) ( ) ( )( ).,...,1 uu u u ttW tt s ss uu rr r 1 ωα ωωα Σ= == Для определенной сигнатуры ( )Σ Ω= S , и определенной многоосновной алгебры ( )M , , ,Σ r где ( )( ),,: , SSssssr ×∈ →Ω= uu uMMuα интерпретацию термов реализует многоос- новная алгебра ( ) ( )i r ri iM M, , , ,Σ Σ= , где ( )r i s i s s s S S = →      ∈ ×αu u u: , , , Ωu M i M i для s S∈ ( )( )M M Ms s s iW∪ ⊆Σ и существует S-индексированное семейство Теоретичні та методологічні основи програмування 7 функций r i , для которых r M Mi s i s: → и для t s∈M ( )rs i t t= ; ( ) ( ) ( )rs i s st t t= ≡α αλ , если t s∈Ω , для u ∈S* , функционального символа ω ∈Ωus и набора термов t u∈M i ( )' ' ,ω t ∈M s i ( )( )( ) ( )( ) ( )( ) ( ) ( ) ( )( ).,, 1 ,, uu u u ttt tt ii s i s i s Df r uu M rr r 1 Kωα ωωαω = ===Σ Для какой-либо определенной сигнатуры ( )Σ Ω= S , , многоосновной алгебры ( )M , ,Σ r с этой сигнатурой и S- индексированного се- мейства множеств переменных X к множест- ву ( )I M , , ,Σ r X относится всякая многоос- новная алгебра ( )M , , ,Σ r где ( )( ),,: , SSssssr ×∈→Ω= uu uMMuα такая, что существует S-индексированное смейство множеств r такое, что для s S∈ ( )( )M M Mi s s sW∪ ⊆Σ , r r Ms s i s i ≡ , ( )r Ms s sX ⊆ , а для u ∈S , функционального символа ω ∈Ωus и кортежа термов t u∈M ( )' ' ,ω t ∈M s ( )( ) ( )( ) ( ) ( ) ( )( ).,, 1 uu u u tt tt ii s i s i s uu rr r 1 Kωα ωωα = == Введение логического типа позволяет устанавливать для термов общие условия. Всякую сигнатуру ( )Σ Ω= S , можно расши- рить “логическим” основанием и перейти к сигнатуре ( )Σ Ωлог лог логS= , , где { }S S логлог = ∪ ' ' , { },,фальшістина‘”‹ =Ω { }Ω лог лог = ¬ ∨' ' , '& ' , ' ' , { }Ω лог лог2 = = ∨ →' ' , '& ' , ' ' , ' ' , ' '= ∈Ω s лог2 для любого s Sлог∈ и для како- го-либо натурального n > 2 { }.'','&' , ∨=Ω логлогn Кроме того, можно условиться реализовывать “логические” функциональные символы лишь соответствующим образом. Иными словами, если с какой-либо сигнатурой ( )Σ Ω= S, со- отнести “логическую” сигнатуру =Σлог ( ),, ‘”‹‘”‹S Ω= то с какой-либо многоосновной алгеброй ( )M , ,Σ r можно соотнести “логиче- скую” многоосновную алгебру ( )M лог лог логr, , ,Σ для которой M лог лог лог= Ω , а для s S∈ M Ms лог s= и ( )( )∀ ∈ = ⇔ =     t t t t t ts s лог1 2 1 2 1 22, ' ' , ,M α а ( ) ( )( ) ( )( ).tt t ωωα ω ⇔ Ω∈∀∈∀∈∀ + логлог логлог nлог лог n nZn M Поэтому, не теряя общности, каждую сигнатуру можно считать “логической” и рас- сматривать только “логические” многооснов- ные алгебры. Таким образом, для каждой “логиче- ской” сигнатуры ( )Σ Ω= S , можно ввести “логическую” алгебру базисных термов ( )Wлог Σ , для которой ( )( ) ( )M MW Wлог Σ Σ= , ( )( )Σ Σ ΣWлог = и существует S-индексированное семейство функций r таких, что для s S∈ ( )( ) ( )( )r M Ms s s W W: Σ Σ→ и для u ∈S* , функционального символа ω ∈Ωus , набора базисных термов ( )( )t u ∈ M WΣ Теоретичні та методологічні основи програмування 8 ( )( )( )( ) ( )( ) ( )( )( ) ( ) ( )( ),,,11 uu u u tt ttW W uuлогs sлогs rr r Kωα ωωα Σ= ==Σ причем ( )( ) ( )( ) ( ) ( )( ) ,',,' ''&'' 1 * 1 uu t t tt логs uus лог rrr Kωω ω =⇒ ⇒=≠Ω∉∨≠ (7) а если t ∈Ω лог * и s лог=' ' , то ( )( ) ( )rлог ω ωt t= ; (8) для базисных термов t t1 2, основы s, если t s1 ∈Ω и t s2 ∈Ω , то ( )rлог t t t t' ' ,1 2 1 2= ⇔ = (9) иначе если ' ' ' ' ,t t1 2= то ( )rлог t t iстина' ' ' ' ,1 2= = (10) а если ' ' ' ' ,t t1 2≠ то ( ) ( )( )r Mлог лог t t t t W' ' ' ' .1 2 1 2= = = ∈ Σ (11) Для какой-либо логической сигнатуры ( )Σ Ω= S , и S-индексированного семейства множеств переменных X можно определить алгебру термов с переменными той же сигна- туры ( )W Xлог Σ, такую, что для любой осно- вы s S∈ ( )( )( ) ( )( )( )M MW X W X s лог sΣ Σ⊆ , , а для семейства функций r ( )( )( ) ( )( )( )r M Ms лог s лог s W X W X: , , ,Σ Σ→ причем для какого-либо терма ( )( )( )ϕ ∈ M W Xлог s Σ, и переменной x X s∈ ( )( )( )' : ' , ' : ' , ,∀ ∃ ∈x s x s W Xлогϕ ϕ M Σ а ( ) ( ) ( )( )r r Mлог лог x W x s x s ' ; ' & , ,∀ =            ∈ϕ ϕ Σ ( ) ( ) ( )( )r r Mлог лог x W x s x s ' ; ' , ,∃ = ∨            ∈ϕ ϕ Σ причем для каких-либо термов ( )( )( )t t W Xлог s1 2, ,∈ M Σ выполняются усло- вия (9)-(11); для u ∈S* , функционального символа ω ∈Ωus , набора термов t ∈ ( )( )( )∈ M W Xлог Σ , u ( ) ( )( )( )' ' ,ω t ∈ M W Xлог s Σ и ( )( ) ( )( )( ) ( )( K,, 11 tXW u‘”‹ss rr ωαω Σ= ut ( ))uu tur,K причем выполняются условия (7)-(8). Для какой-либо сигнатуры ( )Σ Ω= S, , много- основной алгебры ( )M , ,Σ r и S-индексиро- ванного семейства множеств переменных X можно определить многоосновную алгебру логических интерпретаций термов ( ) ( )i r rX df i iX XM M, , , , ,Σ Σ= где ( )r df s s s s S S = →      ∈ ×αu u u u: , , , Ω M M а ( )r i df s i s s i s S S X X X iX = →       ∈ ×αu u u u: , , Ω M M . Для этой алгебры ( )i rX M , ,Σ ∀ ∈ ⊆s S s i s i XM M и существует S-индексированное семейство функций r i X такое, что для s S∈ r M Ms i s i s X X: ,→ r r Ms i s iX s i = , а для какого-либо логического терма ( )( )( )ϕ ∈ M W Xлог лог Σ , со свободной пере- менной типа s , иначе говоря, для такого тер- ма ϕ , что ( )( ) ( )( ) [ ]( ) ( )( ) , :, лог логлогs W axXWWa Σ Σ ∈=Σ∈∀ M rM ϕ и для x X s∈ ' : ' , ' : ' ,∀ ∃ ∈x s x s лог i Xϕ ϕ M а ( ) [ ]( ) ( )( )( ),,:'&'':' s XX Wa i лог i лог axsx Σ∈==∀ Mrr ϕϕ ( ) [ ]( ) ( )( )( );,:''':' s XX Wa i лог i лог axsx Σ∈=∨=∃ Mrr ϕϕ Теоретичні та методологічні основи програмування 9 для u ∈S* , функционального символа ω ∈Ωus , набора термов t u∈M i X ( )' 'ω t ∈M s i X и ( )( )( ) ( )( ) ( )( ) ( ) ( ) ( )( ).,,1 ,, 1 uu u u ttt tt XX XX i u i us i s i s Df r rr rM Kωα ωωαω = ===Σ Представленные построения основы- ваются на воззрениях, изложенных в [4]. Они дают возможность рассматривать знания о какой-либо предметной области, отражаемые в форме “логических” базисных термов с пе- ременными, не затрагивая их конкретизаций в определенных многоосновных алгебрах. Ес- ли, как в [4], обозначить представление таких знаний ( )Σ Φ, , где ( )Σ Ω= S , – сигнатура, а ( )( )Φ Σ⊆ M W Xлог лог , для некоторого S- индексированного семейства множеств пере- менных X , то ( )ΦΣ,MMMM можно обозначить множество всех моделей для представления ( )Σ Φ, : ( ) ( ){ Φ∈∀∈Σ=ΦΣ ϕ:,,, MBAM r Df MMMM ( )},,, rΣMϕ где MBA – класс всех многоосновных ал- гебр. ( )ΦΣ,MMMM обозначим замыкание пред- ставления ( )Σ Φ, : ( ) ( )( )( ){ :,, логлог Df XW Σ∈=ΦΣ MϕMMMM ( ) ( ) ( )}.,, r,M,M ΣΦΣ∈Σ∀ ϕ,,,,MMMMr Теорией в [4] называют представление, в котором множество формул совпадает с за- мыканием. Иначе говоря, если обозначить Ds совокупность всех представлений, то ( ) ( ){ }ΦΣ=Φ∈ΦΣ= ,:, MMMMTTTT Ds Df (12) обозначает совокупность всех теорий. На ос- новании изложенного выше можно предста- вить выражения для различных толкований семантического отношения выводимости ├ . Пусть для какой-либо сигнатуры ( )Σ Ω= S , , представления ( )Σ Φ, , S-индексированного семейства множеств переменных X и логиче- ского терма ( )( )ϕ ∈M W Xлог лог Σ , ( )Σ Φ, ├ ( ),, ΦΣ∈⇔ MMMMϕϕ а для какой-либо алгебры ( )M , ,Σ r ( )M , ,Σ r ├ ( )ϕ ϕ⇔ M , , .Σ r Для решения задач автоматизации программирования А.Я.Диковский и М.И.Канович в [5] предложили “теоретико- модельный подход”, заключающийся в учре- ждении “теоретико-модельной семантики”. Для теории вида (12), отражающей взаимо- связь свойств данных и операций, используе- мых в строящейся программе, эта семантика выражается моделью с носителем, представ- ляющим “логическую” связь данных, которые могут обрабатываться этой программой или возникать при её выполнении. В [6] эту связь данных выражают “предложения вычислимо- сти” вида P Q f  → ,соответствующие логи- ческим формулам вида ( ) ( )( )∀x P x Q f x: . В [5, с.51] о причинах использования таких моделей сказано следующее: “Одно из основных достоинств теоретико-модельной семантики состоит в том, что появляется воз- можность конструктивного понимания си- туации, когда решение отсутствует: если за- дача неразрешима, то можно построить её опровержение...”. Необходимо отметить: дальнейшее развитие воззрений, представ- ленных в [5-7], связано со сложностями, воз- никающими при автоматизации построения циклических предложений. На это в [7] ука- зывал С.С.Лавров. Источником сложностей является монотонность используемых логико- математических исчислений. Она вызывает необходимость привлечения дополнительных построений, таких, как “правила с забывани- ем” [5], “индексированные предикатные сим- волы” [6]. Но даже отказ от монотонности, использование неклассических логик и ис- числений “нелогического” типа не устраняют всех сложностей. Ведь сами исчисления воз- никли как формализация умозаключений. Объекты, возникающие в процессе вывода в каком-либо исчислении, не выделяются ка- Теоретичні та методологічні основи програмування 10 ким-либо особым образом. Само исчисление часто представляют как способ перечисления элементов множества. Признанным средством формализо- ванного описания организации каких-либо взаимосвязанных действий являются транзи- ционные системы. Они используются для ис- следования вопросов безопасного поведения сложных технических систем. Под транзици- онной системой [8] понимают пятерку ( )S S S Sacc rec, , , , ,∆ 0 где S – множество со- стояний; ∆ Σ⊆ × ×S S – отношение перехо- да; S S S Sacc rec0 , , ⊆ – множества соответст- венно начальных, допустимых и повторяю- щихся состояний. Для формализованного представления взаимосвязи вычислений и данных, исполь- зуемых при их выполнении, можно приме- нять сети Петри [9]. Под сетью Петри пони- мают четверку ( )c = P T I O, , , , где P,T – соот- ветственно конечные множества позиций и переходов; ( )I T P: → k , ( )O T P: → k – функ- ции, устанавливающие для каждого перехода соответственно его входные и выходные по- зиции, а также определяющие их кратность. Для какого-либо множества A ( ) { }+Z→= ABA B Df ::tk представляет множество его комплектов, а каждый комплект B представляет его функ- ция количества экземпляров tB . Эта функция определяет кратность принадлежности эле- ментов A комплекту B. Комплект можно ис- толковывать как множество, элементы кото- рого не задаются “абсолютно однозначно” их именами, иначе говоря, когда имеется не- сколько экземпляров элементов с одним име- нем. В таком случае A представляет множест- во используемых имен. Состояние системы в его представле- нии сетью Петри, меру наличия условий воз- можного выполнения переходов в этой сети представляет её текущая маркировка – функ- ция вида +Z→Μ P: . Значение функции маркировки для каждой позиции называют “количеством фишек” в ней. Переход в сети Петри может запускать- ся, если кратность каждой входной позиции этого перехода не превышает количества фи- шек, находящихся в этой позиции в текущий момент. В результате запуска перехода для каждой позиции из числа её фишек вычитает- ся её кратность как входной позиции выпол- няемого перехода и добавляется её кратность как выходной позиции этого перехода. Таким образом сеть Петри переходит в свое сле- дующее состояние. Сети Петри довольно давно и широко используются для анализа и поддержки вы- полнения программ (см., например, [10]). Од- нако очевидна и ограниченность их вырази- тельных возможностей. Она, в частности, проявляется в “ разрешительном характере ” выполнения переходов. В таких случаях при выборе перехода к выполнению приходится использовать дополнительную информацию, изначально соотнеся её с именами позиций и переходов. 3. Сети Петри для сред поддержки программ Сети Петри – отработанное, удобное средство для формализованного представле- ния какой-либо системы взаимообусловлен- ных действий. Представив такую систему с помощью этого средства, можно установить для нее свойства, вытекающие из общих со- ображений, установленных для сетей Петри как формальной системы. Если для среды поддержки программ, определение которой приводится в разд. 1, установить соответст- вующую сеть Петри, то задачи автоматизации программирования можно будет соотнести с задачами достижимости для такой сети. Пусть ( )X Wвозм, , , ,ε µX – среда поддержки программ. Очевидно, функции из µ следует соотнести с переходами, а с пози- циями – программные объекты-элементы X . Однако необходимо учитывать особенности представления состояний выполнения взаи- мообусловленных действий маркировками сети. Ведь если какие-либо две функции из µ имеют общий входной объект, то при их не- посредственном соотнесении с переходами и Теоретичні та методологічні основи програмування 11 позициями сети Петри это приводит к кон- фликтной ситуации, когда запуск одного пе- рехода исключает запуск другого. Избежать конфликта можно, установив в требуемой се- ти Петри отдельную позицию для каждой из функций, имеющих этот общий входной объ- ект, а также общий для них переход от ис- ходного общего входного объекта к вновь уч- реждаемым позициям. Таким образом, каж- дый переход, соответствующий одной из этих функций, имеет возможность независимого запуска. Определенные сложности возникают и при учете “дописываемых” значений входных объектов. Количество фишек для позиции, соответствующей такому программному объ- екту, истолковывается как количество “допи- санных” элементов данных. Но кратность та- кой позиции как входной для какого-либо пе- рехода, соответствующего функции из µ , должна совпадать с этим количеством фишек. Представленную проблему можно решить следующим образом: ограничить максималь- ное количество “ дописываний ” для каждого такого объекта; учредить в требуемой сети Петри новую позицию, соответствующую значению этого объекта, используемому при обращении к функции из µ ; учредить для ка- ждого такого объекта в требуемой сети Петри переходы, количество которых совпадает с максимальными “дописываниями”, причем все эти переходы имеют общие входную и выходную позиции: входная соответствует рассматриваемому объекту, а выходной явля- ется упомянутая вновь учрежденная, крат- ность входной позиции учреждаемых перехо- дов будет различной у разных переходов и охватывать все возможные “ дописывания ”; для всех переходов, соответствующих тем функциям из µ, для которых рассматривае- мый объект с “дописываемым” значением – входной в сети, вместо него входной устанав- ливается вновь учрежденная позиция. Таким образом в требуемой сети Петри представля- ется возможность отработки значений струк- турированных данных. Рассмотренные построения сетей Пет- ри отражены в следующих трех утверждени- ях, проверяемых непосредственно. Лемма 1. Для какой-либо СПП ( )X Wвозм, , , ,ε µX можно построить един- ственную сеть Петри ( )c1 = ′ ′ ′ ′ df P T I O, , , , для которой ′ =P X , ′ =T µ , а для какой-либо функции f ∈µ её входные и выходные объ- екты представляют входные и выходные по- зиции соответствующего перехода сети c1 : ( ) ( )A x xf I f= =     ′: ,t 1 ( ) ( )B x xf O f= =     ′: ,t 1 соответственно ( )t ′ ≡I f A f 0, ( )t ′ ≡O f B f 0. Лемма 2. Для какой-либо СПП ( )X Wвозм, , , ,ε µX и любого натурального числа K можно построить единственную сеть Петри ( )c2 = ′′ ′′ ′′ ′′ df P T I O, , , , для которой ′′ = ′ ∪P P P1, ′′ = ′ ∪T T T1 и ( ){ }P x x Q1 11= ∈, : , ( )( ){ },&&1,:1,, 11 KnnPxxnT ≤∈∈= N а { }Q x X x B ff1 = ∈ ∈ ∈: & ,' µ причем для какого-либо t T∈ ′ ( ) ( )t t′′ ′ ′ ′ ≡I t P Q I t P Q\ \ , 1 1 ( )t ′′ ≡I t Q1 0, ( ) ( )t t′′ ′ ′≡O t P O t 1 , ( )t ′′ ≡O t P1 0 и для каждого натурального n K≤ и всякого x Q∈ 1 если ( ) ( )t ′ =I t x 1, то ( )( ) ( )t ′′ = I n x x n, , ,1 Теоретичні та методологічні основи програмування 12 ( )( ) { } t ′′ ≡ I n x x , , ,1 0 ( )( ) ( )( )t ′′ = O n x x, , , ,1 1 1 ( )( ) ( ){ } t ′′ =O n x x , , , ;1 1 0 при этом ( ) ( ) ( ) ( ){ }t t′ = ∈′ ≡I t x x x QI t, : & , 1 1 1 1 и ( ) ( ) ( ) ( ){ }t t′′ = ∈′ ≡I t P x x x QI t1 11 1 0 \ , : & , а ( )′ ′ ′ ′P T I O, , , – сеть Петри из формулиров- ки леммы 1. Лемма 3. Для какой-либо СПП ( )X Wвозм, , , ,ε µX и какой-либо сети Петри ( )c2 = ′′ ′′ ′′ ′′ df P T I O, , , можно построить единственную сеть Петри c3 = df ( )= ′′′ ′′′ ′′′ ′′′P T I O, , , , для которой ′′′ = ′′ ∪P P P2 , ′′′ = ′′ ∪T T T2 и ( ) ( ) ( ){ }P p t p Q t T pI t2 2 1= ∈ ∈ ′′ =′′, : & & ,t ( ){ }T p p Q2 20= ∈, : , а ( )( ) ( )( ) },&& &1:{ 212 12 21 TtTtt tppPpQ tItI ′′∈′′∈≠ ≠==′′∈= ′′′′ tt причем для какого-либо t T∈ ′ ( )t ′′′ ≡I t Q2 0, ( ) ( )t t′′′ ′′ ′′ ′′ ≡I t P Q I t P Q\ \ , 2 2 ( ) ( )t t′′′ ′′ ′′≡O t P O t , а если же t T∈ 1 , то ( ) ( )t t′′′ ′′ ′′≡I t P I t , ( ) ( )t t′′′ ′′ ′′≡O t P O t , ( )t ′′′ ≡I t P2 0, ( )t ′′′ ≡O t P2 0 ; при этом для какого-либо p Q∈ 2 ( )( ) ( )t ′′′ = I p p 0, 1, ( )( ) { } t ′′′ ≡ I p p 0, 0, ( )( ) ( ) ( ) ( ){ } t t ′′′ ∈ ′′ =′′ ≡ O p p t t T pI t 0, 1 1 , : & , ( )( ) ( ) ( ) ( ){ } t t ′′′ ∈ ′′ =′′ ≡ O p p t t T pI t 0, 1 0 , : & . Адекватность полученной сети Петри c3 рассматриваемым задачам представляет следующее утверждение. Теорема 1. Пусть ( )X Wвозм, , , ,ε µX – СПП, а A B, ∈X и для любого ( )w W Aвозм∈ * найдется цепочка f ∈µ* такая, что сущест- вует ( ) ( )F w G ,w W B B возмµ ≡ ∈′′f f . Тогда для какой-либо сети Петри ( )c =3 ′′′ ′′′ ′′′ ′′′P T I O, , , в формулировке лем- мы 3 подмаркировка Λ p B∈ ′′′.1, где ( ) ( ) { }( )′′′ = ∪ ∩ ×B B Q B Q df \ ,1 1 1 а Λ – мета- ламбдаабстракция [11], достижима с началь- ной маркировки Λ p A∈ .1, причем для каж- дого ( )g ∈Z1 A B, в обобщенном дереве дос- тижимости 9 с. 90-106] для сети ( )c3 1, .Λ p A∈ существует путь от начальной вершины к вершине, соответствующей под- маркировке Λ p B∈ ′′′.1, в котором переходы, соответствующие элементам µ, размещаются в той же последовательности, что и в g. Справедливость представленного ут- верждения вытекает из следствия 3 в [3 с.15]. Теоретичні та методологічні основи програмування 13 4. Синтез программ на сетях Петри Представленные в предыдущем разде- ле утверждения обосновывают подход к ис- пользованию сетей Петри для автоматизации программирования с переприсваиваниями. Из теоремы 1 следует, что необходимым услови- ем положительного решения задачи анализа [5, с. 36] является положительное решение соответствующей задачи достижимости под- маркировки, а очередность расположения ис- полнимых программных предложений в тек- сте синтезируемой программы связана с соот- ветствующим деревом достижимости. Отраниченность выразительных воз- можностей сетей Петри проявляется, кроме прочего, и в “разрешительном характере” теоремы 1. Однако наличие определенного конечного дерева достижимости представляет механизм, используя который в любом со- стоянии выполнения какой-либо системы взаимообусловленных действий, представ- ляемых СПП ( )X Wвозм, , , ,ε µX , можно од- нозначно определить действие или несколько равноценных действий, которые следует по- пытаться выполнить для достижения постав- ленных целей. Кроме того, исполнимые про- граммные предложения, представляемые в сети элементами µ, реализуют термы вполне определенной простой структуры. Корректно поставленная задача авто- матизации программирования [5, с. 36] пред- полагает наличие “вычислительной модели” или “модели предметной области”, в которой полностью представляются все знания, доста- точные для построения требуемых программ. Исходя из этого уточним мнения функцио- нальных зависимостей, задаваемых в СПП ( )X Wвозм, , , ,ε µX элементами µ . Исследуя исторически сложившиеся представления о вычислительных моделях, А. Я. Диковский и М. И. Канович пришли к выводу [5, с. 37], что в вычислительных моделях представля- ются функциональные, условно функцио- нальные, операторные и условно оператор- ные зависимости. При этом под функцио- нальной зависимостью понимают зависи- мость вида ( ) ( )f W A W Bвозм f возм f: ,* → иначе говоря, зависимость, реализуемую соб- ственно исполнимым программным предло- жением (безусловным оператором). Под ус- ловной зависимостью понимают какую-либо зависимость ϕ , реализуемую с использовани- ем условного оператора, т.е. зависимостью вида если P то ϕ . Операторные зависимости – зависимости, реализуемые процедурами с парамерами- процедурами. Такие процедуры могут потре- боваться, например, для вычисления значе- ний определенных интегралов. Очевидно, действие всякой функцио- нальной зависимости, определенной в СПП ( )X Wвозм, , , ,ε µX элементом f ∈µ , можно реализовать мультиветвлением вида ВЫБОР f СЛУЧАЙ ( )X B Cf w f∩ = ′ Реализация w f wB A C f f '' ∪             ′ СЛУЧАЙ ( )X B Cf w f∩ = ′′ Реализация w f wB A C f f '' ∪             ′′ . . . . . . . . . СЛУЧАЙ ( )X B Cf w f∩ = ′′′ Реализация w f wB A C f f '' ∪             ′′′ ВСЁ-ВЫБОР где { } { }′ ′′ ′′′ = ∩ ∈C C C B C Cf, , , :K X . При этом следует учитывать, что при практиче- ском программировании “затирание” неопре- деленных значений B f '' требует привлечения специальных средств. Зависимости, функциональные по Ди- ковскому - Кановичу, – простейший случай для представления программных предложе- ний в сети Петри. Если все переходы в такой сети соответствуют этим зависимостям, то программа получается непосредственно из Теоретичні та методологічні основи програмування 14 пути в дереве достижимости отбрасыванием переходов из T1 и T2 . Сложности возникают при соотнесении переходов сети Петри с ус- ловно функциональными зависимостями. Сеть Петри позволяет определить возможную последовательность действий для достижения требуемой цели, но она не представляет средств для учета условий выполнения таких действий. Поэтому обращение к условному оператору в виде одного перехода предста- вить невозможно. Оно задается совокупно- стью переходов, в которой каждый из них со- ответствует отдельной альтернативе. Но то- гда и все последующие переходы в каждом из отдельных путей в дереве достижимости вплоть до узла, соответствующего требуемой маркировке, представляет тело условного оператора, соответствующего условию вы- полнения упомянутого начального перехода. Положение может спасти совпадение всех альтернативных путей начиная с какого-либо общего для них узла в дереве достижомости. В этом случае такому узлу соответствует ко- нец условного оператора, а упомянутые не- совпадающие альтернативные пути представ- ляют тела альтернатив в этом операторе. Итак, наличие условнофункциональ- ных зависимостей, соответствующих перехо- дам, имеющим в дереве достижимости общий начальный узел, может истолковываться как мультиветвление. Однако, чтобы программа, включающая такое мультиветвление, не была частичной, необходимо, чтобы указанные альтернативы образовывали полный набор. Иначе говоря, необходимо, чтобы конъюнк- ция соответствующих условий всегда была истинной. В [9, c. 90-98] показано, что логиче- скую взаимосвязь всех возможных состояний какой-либо системы взаимообусловленных действий представляет конечное дерево дос- тижимости соответствующей сети Петри. Для представления узлов такого конечного дерева используются маркировки, в которых пози- ции с неограниченно большой достижимой кратностью получают новое, обобщенное значение “ ∞”. В соответствии с теоремой 1 такое дерево можно использовать для опре- деления очередности следования исполнимых программных предложений. Но, кроме того, используя такое дерево достижимости, для требуемой программы можно построить цик- лические предложения. Если какой-либо из путей от началь- ной маркировки до какой-либо маркировки, включающей требуемую подмаркировку, со- держит позицию, для которой в дереве дос- тижимости есть замкнутый путь, то этому пу- ти соответствует тело цикла-рекурсии. Ите- рации соответствует участок упомянутого пу- ти до маркировки, в которой каждая из пози- ций по количеству фишек меньше, чем в ко- нечной. Как указано в [5, с.37]: “Из известных фактов теории алгоритмов следует, что если вид зависимостей не ограничить разумным образом, то алгоритмы анализа и синтеза ли- бо невозможны, либо неизбежно крайне не- эффективны. Поэтому в практически реали- зуемых системах синтеза программ ограни- чиваются зависимостями сравнительно про- стого вида.” Исходя из представленных выше соображений рассмотрим возможности син- теза программ из модулей, реализующих за- висимости, функциональные и условно функ- циональные по Диковскому - Кановичу. Для этого расширим язык цепочек функциональ- ных символов, представленный в [1] и уже использованный подобным образом в [3]. Се- мантику учреждаемых конструкций будет от- ражать функция, представляющая значения для образуемых функциональных термов. Пусть ( )X Wвозм, , , ,ε µX – СПП. Рассмотрим выразительные возможности та- кой среды, когда в µ представлены зависимо- сти, функциональные и условно функцио- нальные по Диковскому - Кановичу. Иначе говоря, пусть µ включает непустые множест- ва µF " и µCF " такие, что ( ) ( )∀ ∈ →f f W A W BF возм f возм fµ" * ": , ( ) ( ) ( )( ).&" " ∅== ∈∀∈∀ wffwf fвозм XBX AWwf CF µ Таким образом, для f CF∈µ" существует пре- дикат Теоретичні та методологічні основи програмування 15 { } ( )P iстина фальшf W Aвозм f∈ , , ( ) ( )( ( ) ( ) ),& &''* ∅=⇔¬ ⇔∈∀ wff fffвозм XwP BwPAWw и функция ( ) ( )ϕ f возм f f возм fW A P W B: , ,* * → где ( ) ( ) ( ){ }W A P w w W A P wвозм f f df возм f f , : & .= ∈ Представим условно функциональные зави- симости из µCF " парами вида ( )P, .ϕ Семан- тику языка цепочек функциональных симво- лов-элементов µ представляет функция ( )G wf , вида (3)-(6). Дополним этот язык предложениями вида ( )P, ,f где P – преди- кат, f – предложение языка ( его императивно интерпретируемый нетерминальный символ). Пусть ( )( ) ( ) ( )    ⊆ = = , ,&,, ,, случаяхостальныхвсехвоw XAwPеслиwG wPG wff f где ( )w W X∈ , ,ε X . Несложно ввести пред- ложения более общего вида, представляющие мультиветвление. Пусть для предикатов ′ ′′ ′′′P P P, , ,K и предложений ′f , ′′ ′′′f f, ,K ( )( ) ( ) ( ) ( ) ( ) ( ) ( )          ⊆′′′′′′ ⊆′′′′ ⊆′′ = =′′′′′′′′′′′′ ′′′ ′′ ′ . ,&,, ,&,, ,&,, ,,;,;, случаяхостальныхвсехвоw XAwPеслиwG XAwPеслиwG XAwPеслиwG wPPPG w w w Df Df f f f f f f ,fff M K Очевидна справедливость следующего утверждения. Лемма 4. Пусть ( )X Wвозм, , , ,ε µX – СПП и для некоторой цепочки функциональ- ных символов f ∈µ известно, что для w W Aвозм∈      * f ( ) ( ) ( )′ ⇒ ≡ ′P w G w G wf f, , , ( ) ( ) ( )′′ ⇒ ≡ ′′P w G w G wf f, , , K ( ) ( ) ( )′′′ ⇒ ≡ ′′′P w G w G wf f, , для определенных предикатов { } ( )′ ′′ ′′′ ∈P P P iстина фальш W Aвозм, , , , * K f и цепочек функциональных символов ′ ′′ ′′′ ∈f , , , f fK µ при A A A A′ ′′ ′′′ ⊆f f f f, , , .K Тогда ( ) ( )( )G w G P P P wf f f f, , ; , ; ; , ,≡ ′ ′ ′′ ′′ ′′′ ′′′K для w W Aвозм∈       f , если ( ) ( ) ( ) ( ).&&&* wPwPwPAWw возм ′′′′′′∈∀ Kf Также нетрудно убедиться в справед- ливости следующего утверждения. Теорема 2. Пусть ( )X Wвозм, , , ,ε µX – СПП. Для каких-либо ′ ′′f , ,f K ( )K, , " " * ′′′ ∈ ∪f h µ µF CF и предикатов { } ‰”Ќ” WложьистинаPPP ,,,, ∈′′′′′′ K ( )( ) ( )( )( )w,,P;;,P;,PG,G w,,P;;,P;,PG fffh hfhfhf ′′′′′′′′′′′′≡ ≡′′′′′′′′′′′′ K K для w Wвозм∈ , если ( ) ( ) ( )∀ ∈ ′ ′′ ′′′w W P w P w P wвозм & & & .K В [3] рассмотрен синтез циклических предложений, причины и условия их по- строения в синтезируемой программе. Глав- ные условия применения циклических пред- ложений – наличие набора программных объ- ектов, состояние которого определяется и из- меняется (возможно, многократно) в процессе выполнения требуемых действий, а также на- личие набора программных объектов, в со- стоянии которого фиксируется конечный ре- зультат выполнения действий, связанных с циклическим изменением состояния упомя- нутого выше набора. Дополним рассматриваемый язык це- почек функциональных символов предложе- ниями вида ( )f , ,A где f – предложение язы- ка, A – описанный выше набор программных объектов с циклически изменяемым состоя- Теоретичні та методологічні основи програмування 16 нием. Пусть для ( )w W X∈ , ,ε X ( )( ) ( ) ( )( ) ( ) ( ) ( )    ≡ ≠ = = .,,, ,,,,,, ,, AA AA wGwеслиwG wGwеслиwGAG wAG ff fff f Из следствия 1 в [3 с.13] вытекает справедливость следующего утверждения. Теорема 3. Пусть ( )X Wвозм, , , ,ε µX – СПП. Для каких-либо A B, ∈X и какой-либо цепочки функциональных символов ( )f ∈ ∪µ µF CF " " * такой, что ( )f ∈Z1 A B, , для h CF∈µ" , если A A Bh ⊆ ∪f f и ′ = ∩ ≠ ∅A A B df hf1 " , то ( )( )( )F G h A w F wµ µf , , .′ ⊆ Лемма 4 и теорема 2 обосновывают приведенные выше соображения о синтезе условных операторов на дереве достижимо- сти, а теорема 3 – подход к построению цик- лических предложений на дереве достижимо- сти. Таким образом, если для СПП ( )X Wвозм, , , ,ε µX функции, представляе- мые элементами µ, выражают функциональ- ные или условно функциональные зависимо- сти, то для каких-либо входного A и выходно- го B наборов, A B, ∈X , можно решить задачу анализа, используя дерево достижимости со- ответствующей сети Петри. Положительное решение этой задачи представляется наличи- ем в таком дереве достижимости пути от мар- кировки Λ p A∈ .1 до подмаркировки Λ p B∈ .1, в котором нет переходов f ∈µ , приводящих к маркировкам, где для некото- рого p B f∈ ' ' ( )Μ p > 1. Выводы Термальный аспект автоматизации программирования с переприсваиваниями рассмотрен с теоретико-модельных позиций. Такой подход позволил учесть и программи- стскую, и декларативную семантику синтези- руемых термов, используя модели, основан- ные на семантике как маркировок, так и со- стояний. На этой концептуальной основе предложен уточненный подход к практиче- скому автоматическому синтезу реальных программ. 1. Приходько П.П. Функциональный подход к концеп- туальному программированию // Дис. ... канд.физ.-мат. наук.– Киев,1991. – 177 с. 2. Успенский В.А., Семенов А.Л. Теория алгоритмов: основные открытия и приложения. – М.: Наука,1987.– 288 с. 3. Приходько П.П. О возможных основаниях немоно- тонного дедуктивного синтеза программ // Пробл. про- граммирования. – 2003. – №4. – С. 5-23. 4. Замулин А.В. Категории типов данных / Новоси- бирск: ВЦСО АН СССР . - Препр. № 667. 1986. – 24 с. 5. Диковский А.Я., Канович М.И. Вычислительные модели с разделяемыми подзадачами // Изв. АН СССР. Техн. Кибернетика. – 1985. – №5. – С. 36-59. 6. Тыугу Э.Х. Концептуальное программирование. – М.: Наука, 1984. – 256 с. 7. Лавров С.С. Синтез программ // Кибернетика. – 1982.– №6 . – С.11-16. 8. Model checking / Edmund M. Clarke, Bernd-Holger Schlingloff // HANDBOOK OF AUTOMATED REASONING Edited by Alan Robinson and Andrei Vo- ronkov  Elsevier Science Publishers B.V., 2001. – Р. 1369-1522. 9. Питерсон Дж. Теория сетей Петри и моделирова- ние систем: Пер. с англ. – М.: Мир, 1984. – 264 с. 10. Shapiro R., Saint H., A New Approach to Optimization of Sequencing Decisions, Annual Review in Automatic Programming, 6, Part 5, 1970, p. 257-288. 11. Барендрегт Х. Ламбда-исчисление. Его синтаксис и семантика. – М. : Мир, 1985. – 606 с. Получено 04.10.05 Об авторе Приходько Павел Петрович канд. физ.- мат. наук тел (044) 5324690 Место работы автора: Институт программных систем НАН Украины просп. Академика Глушкова, 40, Киев-187,03680 тел (044) 5324690
id	nasplib_isofts_kiev_ua-123456789-2325
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn	1727-4907
language	Russian
last_indexed	2025-12-07T18:37:04Z
publishDate	2006
publisher	Інститут програмних систем НАН України
record_format	dspace
spelling	Приходько, П.П. 2008-09-17T14:20:47Z 2008-09-17T14:20:47Z 2006 О термальном аспекте автоматизации программирования / П.П. Приходько // Проблеми програмування. — 2006. — N 1. — С. 3-16. — Бібліогр.: 11 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2325 681.3.06 Уточняются основные положения немонотонного синтеза программ с переприсваиваниями. Такой синтез рассматривается с использованием теоретико-модельного подхода. Для изучения программистской и декларативной семантики предлагается использовать многоосновные алгебры термов при представлении операций над данными в синтезируемых программах. Для изучения путей эффективного автоматического синтеза программ применяются сети Петри. Уточнюються основні положення немонотонного синтезу програм з переприсвоюваннями. Такий синтез розглядається з використанням теоретико-модельного підходу. Для дослідження прорамістської та декларативної семантики запропоновано використовуати многоосновні алгебри термів при представленні операцій над даними в програмах, що синтезуються. Для дослідження шляхів ефективного автоматичного синтезу програм використовуються мережі Петрі. Substantive provisions of nonmonotonic synthesis of programs with reassignments are specified. Such synthesis is considered with use of the approach with models theory. For studying programmer and declarative semantics it is offered to use the multibasic algebras of terms at representation of operations above the data in synthesized programs. Petri nets are applied to studying ways of effective automatic synthesis of programs. ru Інститут програмних систем НАН України Теоретичні та методологічні основи програмування О термальном аспекте автоматизации программирования Про термальний аспект автоматизації програмування About thermal aspect of automation of programming Article published earlier
spellingShingle	О термальном аспекте автоматизации программирования Приходько, П.П. Теоретичні та методологічні основи програмування
title	О термальном аспекте автоматизации программирования
title_alt	Про термальний аспект автоматизації програмування About thermal aspect of automation of programming
title_full	О термальном аспекте автоматизации программирования
title_fullStr	О термальном аспекте автоматизации программирования
title_full_unstemmed	О термальном аспекте автоматизации программирования
title_short	О термальном аспекте автоматизации программирования
title_sort	о термальном аспекте автоматизации программирования
topic	Теоретичні та методологічні основи програмування
topic_facet	Теоретичні та методологічні основи програмування
url	https://nasplib.isofts.kiev.ua/handle/123456789/2325
work_keys_str_mv	AT prihodʹkopp otermalʹnomaspekteavtomatizaciiprogrammirovaniâ AT prihodʹkopp protermalʹniiaspektavtomatizacííprogramuvannâ AT prihodʹkopp aboutthermalaspectofautomationofprogramming

О термальном аспекте автоматизации программирования

Institution

Ähnliche Einträge