Флойд әдісі бойынша программаның дұрыстығын дәлелдеу

1. Флойд әдісі бойынша программаның дұрыстығын дәлелдеу дегенміз соңғышарттың ақиқаттығы алғышарт ақиқаттылығынан және барлық аралықшарттар ақиқаттылығынан шығатындығын дәлелдеу.

Сонымен талданатын Р программасы р₁,р₂,…,р_и программалық бірліктерінен тұрғызылған болсын, яғни, әрбір программалық бірлік р₁(t=1,n) меншіктеу операторы, тармақталу операторы, тармақталу операторы, қайталану операторы немесе, топталу операторы болады. Р программасының верификациялау шарты cν (Р,і_р,о_р) арқылы белгіленсін, яғни,

cν (Р,і_р,о_р)→(і_р(Х,)∩r_р1(х,у)|_р2 )&( r_р1(х,у) ∩ r_р2(х,у)_р2) &…&( r_рn-1(х,у) ∩о_р(X,y)

2. Берілген программаның дербес дұрыстығын дәлелдеу, осы программадағы барлық жолдарға арнап құрылған(1), (2) және (3)верификациялаушарттарының ақиқаттығын орнатуға келіп тіреледі.

(1)- формуладан арифметикалық амалдардф орындап біткен соңмынадай x₁ ³ & x₂ > o É x₁=x₁& x₁³ o логикалық өрнек шығады,мұндағыx₁=x₁— 2h әр қашанда ақиқат(тавтология), сондықтаноны қысқартыптастапөрнектенмынадай X₁³O&x₂>OÉx₁³ Oформула алуға болады.

(2)- формуладан арифметикалық амалдардыорындап біткен соңжәнеAÉ(BÉС) және A&BÉС түріндегіформулалардыңлогикалық теңмәнділігін,сондай-ақ,конъюнкцияның коммутативтілігінескереотырып, A&BÉA түріндегі аксиоманы (мәні әрқашан ақиқат формуланы) алуға болады, яғни,

x₁=y₁* x₂+y₂& y₂³x₂ &y₂³ O Éx₁=y₁ * x₂+y₂³x₂

AB A

(3)- формуланытүрлендіре отырып DÉ Dтүріндегі аксиоманыалуға болады, мұнда D арқылы мына х₁=y₁ *x₂+y₂ & y₂& x₂> y₂ әрнегі белгіленеді.

Енді алынған (1), (2) және (3) верификациялаушарттарыныңақиқаттығынтексеру үшін мән орнату функциясы VAL-ңкөмегімен х₁  және х₂енгізу айнымалылары үшін нақты тестілікдеректералайық, мысалы, VAL (х_1, х₂) = (7,3) болсын.Сонда верификациялау шарттарыбойынша айнымалылар үшін келесі мәндерді аламыз:

7³О& 3>ОÉ 7=О*7+7 & 7³О;(1)

7=1*3+4 & 4³O É(43 Й 7=(1+1)* 3+4-3 & 4³3; (2)

7=2*3+1& 1³ O É (3>1É7=2*3+1& 3>1) (3)

(1’’). (2’’)және (3’’)өрнектердіңақиқаттығы көрініп тұр, яғни, P программасын верификациялау шарты _сv (Р, і, о )ақиқат болады, ол жоғарыдағы теорема V. 1 бойынша і_р {p}o_p-ңақиқаттығын көрсетеді. Ендеше, біз қарастырған бүтін санды бүтін санға бөлуді орындайтын З программасыдербесдұрыс.