ПРОГРА́ММ СИ́НТЕЗ

ПРОГРА́ММ СИ́НТЕЗ, про­цесс так на­зы­вае­мо­го до­ка­за­тель­но­го про­грам­ми­ро­ва­ния, ко­гда со­став­ле­ние про­грам­мы со­про­во­ж­да­ет­ся до­ка­за­тель­ст­вом её со­от­вет­ст­вия фор­маль­ной по­ста­нов­ке ис­ход­ной за­да­чи. На прак­ти­ке П. с. объ­е­ди­ня­ет в се­бе три ти­па фор­маль­ных ма­ни­пу­ля­ций с про­грам­ма­ми: ло­гич. син­тез, сбор­ку и кон­кре­ти­за­цию.

Ло­ги­че­ский син­тез – один из спо­со­бов пе­ре­хо­да от про­грам­мы спе­ци­фи­ка­ции к реа­ли­зую­ще­му ал­го­рит­му, имею­щий фор­му точ­но­го рас­су­ж­де­ния в не­ко­то­рой ло­гич. сис­те­ме. Од­ной из ло­гич. сис­тем яв­ля­ет­ся кон­ст­рук­тив­ная ло­ги­ка, где син­те­зи­руе­мая про­грам­ма из­вле­ка­ет­ся из кон­ст­рук­тив­но­го до­ка­за­тель­ст­ва тео­ре­мы о су­ще­ст­во­ва­нии ре­ше­ния за­да­чи. Дру­гой тип ло­гич. сис­те­мы – ло­ги­ки Хоа­ра (см. в ст. Про­грамм ве­ри­фи­ка­ция).

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

При кон­кре­ти­за­ции ре­зуль­ти­рую­щая про­грам­ма по­лу­ча­ет­ся пу­тём су­же­ния уни­вер­саль­но­го ал­го­рит­ма на осо­бые ус­ло­вия его при­ме­не­ния, ха­рак­те­ри­зую­щие ча­ст­ную за­да­чу, под­ле­жа­щую ре­ше­нию.

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