ПРОГРА́ММ ВЕРИФИКА́ЦИЯ

ПРОГРА́ММ ВЕРИФИКА́ЦИЯ, на­прав­ле­ние тео­ре­тич. про­грам­ми­ро­ва­ния, свя­зан­ное с раз­ра­бот­кой и изу­че­ни­ем ме­то­дов до­ка­за­тель­ст­ва пра­виль­но­сти про­грамм, ори­ен­ти­ро­ван­ных на прак­тич. при­ме­нение.

Про­грам­ма A час­тич­но пра­виль­на от­но­си­тель­но пре­ду­сло­вия P и по­сту­сло­вия Q (обо­зна­че­ние P{A}Q), ес­ли, в слу­чае ко­гда P ис­тин­но для вход­ных зна­че­ний пе­ре­мен­ных и A за­вер­ша­ет ра­бо­ту, Q ис­тин­но для вы­ход­ных зна­че­ний пе­ре­мен­ных. Про­грам­ма A то­таль­но пра­виль­на от­но­си­тель­но P и Q, ес­ли вы­пол­ня­ет­ся P{A}Q и A за­вер­ша­ет ра­бо­ту для вход­ных зна­че­ний пе­ре­мен­ных, удов­ле­тво­ряю­щих ус­ло­вию P. Для до­ка­за­тель­ст­ва час­тич­ной пра­виль­но­сти опе­ра­тор­ных про­грамм обыч­но ис­поль­зу­ют­ся мо­ди­фи­ка­ции ме­то­да Флой­да, ко­то­рый со­сто­ит в сле­дую­щем. На про­грам­мы схе­ме вы­би­ра­ют­ся кон­троль­ные точ­ки так, что­бы лю­бой цик­лич. путь про­хо­дил по край­ней ме­ре че­рез од­ну точ­ку. С ка­ж­дой кон­троль­ной точ­кой ас­со­ции­ру­ет­ся спец. ус­ло­вие (ин­дук­тив­ное ут­вер­жде­ние или ин­ва­ри­ант цик­ла), ко­то­рое ис­тин­но при ка­ж­дом пе­ре­хо­де че­рез эту точ­ку. С вхо­дом и вы­хо­дом схе­мы так­же ас­со­ции­ру­ют­ся пред- и по­сту­сло­вия. За­тем ка­ж­до­му пу­ти про­грам­мы ме­ж­ду дву­мя со­сед­ни­ми кон­троль­ны­ми точ­ка­ми со­пос­тав­ля­ет­ся т. н. ус­ло­вие пра­виль­но­сти. Вы­пол­не­ние всех ус­ло­вий пра­виль­но­сти га­ран­ти­ру­ет час­тич­ную пра­виль­ность про­грам­мы.

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

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