Теормин - шпоры (1158131), страница 6
Текст из файла (страница 6)
(ɫ) 2006 GrGr (grgr@later.ru)Ɂɚɦɟɱɚɧɢɟ. ɇɟ ɫɭɳɟɫɬɜɭɟɬ ɧɢ ɨɞɧɨɝɨ ɫɨɞɟɪɠɚɬɟɥɶɧɨɝɨ ɦɚɬɟɦɚɬɢɱɟɫɤɨɝɨ ɭɬɜɟɪɠɞɟɧɢɹ, ɞɥɹɤɨɬɨɪɨɝɨ ɧɟɥɶɡɹ ɛɵɥɨ ɛɵ ɩɨɫɬɪɨɢɬɶ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɝɨ ɞɨɤɚɡɚɬɟɥɶɫɬɜɚ, ɨɞɧɚɤɨ ɜɫɟɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɞɨɥɠɧɵ ɩɨɤɚɡɵɜɚɬɶ ɩɪɚɜɢɥɶɧɨɫɬɶ ɭɬɜɟɪɠɞɟɧɢɹ ɹɜɧɨ (ɤɨɧɫɬɪɭɤɬɢɜɧɨ),ɩɨɷɬɨɦɭ ɜɫɟ ɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɩɨɥɭɱɚɸɬɫɹ ɛɨɥɟɟ ɫɥɨɠɧɵɦɢ, ɚ ɪɟɡɭɥɶɬɚɬɨɦ ɥɸɛɨɝɨ ɬɚɤɨɝɨɞɨɤɚɡɚɬɟɥɶɫɬɜɚ ɛɭɞɟɬ ɩɨɫɬɪɨɟɧɢɟ ɚɥɝɨɪɢɬɦɚ.ɍɬɜɟɪɠɞɟɧɢɟ (ɞɢɡɴɸɧɤɬɢɜɧɨɟ ɫɜɨɣɫɬɜɨ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣ ɥɨɝɢɤɢ). ɂɧɬɭɢɰɢɨɧɢɫɬɫɤɚɹɨɛɳɟɡɧɚɱɢɦɨɫɬɶ ɮɨɪɦɭɥɵ M \ ɷɤɜɢɜɚɥɟɧɬɧɚ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɨɣ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɥɢɛɨ M ,ɥɢɛɨ \ .(x = t)ɉ1, ɉ2if A then ɉ1 else ɉ2 fiwhile A do ɉ1 odeps,Ƚɞɟ ɯ – ɩɟɪɟɦɟɧɧɚɹ, t – ɬɟɪɦ ɉi – ɩɪɨɝɪɚɦɦɵ, Ⱥ – ɚɬɨɦ, eps – ɩɭɫɬɨɬɚ.F1 , F2 ,..., Fn, ɩɪɢɱɟɦF0ɜɵɪɚɠɟɧɢɹ ɜ ɜɟɪɯɧɟɣ ɱɚɫɬɢ ɩɪɚɜɢɥɚ ɧɚɡɵɜɚɸɬɫɹ ɩɪɟɞɩɨɫɵɥɤɚɦɢ, ɜɵɪɚɠɟɧɢɟ ɜ ɧɢɠɧɟɣ ɱɚɫɬɢɩɪɚɜɢɥɚ ɧɚɡɵɜɚɟɬɫɹ ɡɚɤɥɸɱɟɧɢɟɦ.
ɋɟɦɚɧɬɢɤɚ ɩɪɚɜɢɥɚ ɜɵɜɨɞɚ ɬɚɤɨɜɚ: ɟɫɥɢ ɢɫɬɢɧɧɵɦɩɪɟɞɩɨɫɵɥɤɢ, ɬɨ ɢɫɬɢɧɧɨ ɢ ɡɚɤɥɸɱɟɧɢɹ.Ɉɩɪɟɞɟɥɟɧɢɟ. ɉɪɚɜɢɥɨɦ ɜɵɜɨɞɚ ɧɚɡɵɜɚɟɬɫɹ ɮɢɝɭɪɚ ɫɥɟɞɭɸɳɟɝɨ ɜɢɞɚ:Ɋɚɫɫɦɨɬɪɢɦ ɫɥɟɞɭɸɳɭɸ ɫɢɫɬɟɦɭ ɩɪɚɜɢɥ:M o M '1 ,{M '1} 3 ! {M '2 }, M 2 o M '2(ɨɫɥɚɛɥɟɧɢɹ)1. 1{M } 3 ! {M }12^ `M o\ x t(ɩɪɢɫɜɚɢɜɚɧɢɹ){M} x:= t ! {\ }{M} 31 ! {F },{F } 3 2 ! {\ }3.(ɩɨɫɥɟɞɨɜɚɬɟɥɶɧɨɝɨ ɫɨɟɞɢɧɟɧɢɹ){M} 3 ; 3 ! {\ }2.1ɍɬɜɟɪɠɞɟɧɢɟ. Ɏɨɪɦɭɥɚ xM ( x) ɨɛɳɟɡɧɚɱɢɦɚ ɬɨɝɞɚ ɢ ɬɨɥɶɤɨ ɬɨɝɞɚ, ɤɨɝɞɚ ɫɭɳɟɫɬɜɭɟɬ ɬɚɤɨɣɬɟɪɦ t, ɱɬɨ ɮɨɪɦɭɥɚ M (t ) ɛɭɞɟɬ ɢɧɬɭɢɰɢɨɧɢɫɬɫɤɢ ɨɛɳɟɡɧɚɱɢɦɨɣ.21Ɇɚɬɟɦɚɬɢɱɟɫɤɚɹ ɥɨɝɢɤɚ, ɫɜɨɞɤɚ ɨɩɪɟɞɟɥɟɧɢɣ. (ɫ) 2006 GrGr (grgr@later.ru){F inv & A} 3 !, F inv & A o \ , M o F inv(ɢɬɟɪɚɰɢɢ; F inv ɧɚɡɵɜɚɟɬɫɹ ɢɧɜɚɪɢɚɧɬɨɦ{M} while_A_do_3 ! {\ }ɨɩɟɪɚɬɨɪɚ ɢɬɟɪɚɰɢɢ, ɞɥɹ ɩɪɨɜɟɪɤɢ ɩɪɚɜɢɥɶɧɨɫɬɢ ɪɚɛɨɬɵ ɰɢɤɥɚ ɬɪɟɛɭɟɬɫɹ ɟɝɨ ɧɚɣɬɢ)6. {M} eps ! {M } (ɚɤɫɢɨɦɚ)5.ɋɢɫɬɟɦɚ ɬɚɤɢɯ ɩɪɚɜɢɥ ɧɚɡɵɜɚɟɬɫɹ PVS (Prototype Verification System) ɢ ɩɨɡɜɨɥɹɟɬ ɭɩɪɨɳɚɬɶɩɪɨɜɟɪɤɭ ɩɪɚɜɢɥɶɧɨɫɬɢ ɩɪɨɝɪɚɦɦ.4.4.
Ʌɨɝɢɤɢ ɡɧɚɧɢɣɊɚɫɫɦɨɬɪɢɦ ɦɭɥɶɬɢɚɝɟɧɬɧɭɸ ɫɢɫɬɟɦɭ (ɫɥɨɠɧɭɸ ɫɢɫɬɟɦɭ, ɩɪɢɧɢɦɚɸɳɭɸ ɪɟɲɟɧɢɹ)A1 , A2 ,..., An ɩɪɨɝɪɚɦɦ-ɚɝɟɧɬɨɜ. ɉɪɢ ɷɬɨɦ ɩɪɢɧɹɬɢɟ ɪɟɲɟɧɢɹ ɦɨɠɟɬ ɨɩɢɪɚɬɶɫɹ ɧɚ ɬɨ, ɱɬɨɡɧɚɸɬ ɢɥɢ ɧɟ ɡɧɚɸɬ ɞɪɭɝɢɟ ɭɱɚɫɬɧɢɤɢ ɩɪɨɰɟɫɫɚ ɩɪɢɧɹɬɢɹ ɪɟɲɟɧɢɣ.Ɉɩɪɟɞɟɥɟɧɢɟ. Ɇɨɞɚɥɶɧɵɦ ɨɩɟɪɚɬɨɪɨɦ ɧɚɡɵɜɚɟɬɫɹ ɨɩɟɪɚɬɨɪ , ɤɨɬɨɪɵɣ ɜɵɪɚɠɚɟɬɨɬɧɨɲɟɧɢɟ ɭɜɟɪɟɧɧɨɫɬɢ (ɧɟɨɛɯɨɞɢɦɨɫɬɢ).
ȿɝɨ ɫɟɦɚɧɬɢɤɚ ɬɚɤɨɜɚ:ɹM ɨɡɧɚɱɚɟɬ «ɹ ɡɧɚɸ, ɱɬɨ ɮɨɪɦɭɥɚ M ɢɫɬɢɧɧɚ».ȼɨɩɪɨɫ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɮɨɪɦɭɥɵM o M - ɜɨɩɪɨɫ ɧɟɩɪɨɬɢɜɨɪɟɱɢɜɨɫɬɢ ɛɚɡɵ ɡɧɚɧɢɣ.ɹȼɨɩɪɨɫ ɨɛɳɟɡɧɚɱɢɦɨɫɬɢ ɮɨɪɦɭɥɵ M oM - ɜɨɩɪɨɫ ɩɨɥɧɨɬɵ ɛɚɡɵ ɡɧɚɧɢɣ.ɹ4.5. Ⱦɢɧɚɦɢɱɟɫɤɚɹ ɥɨɝɢɤɚ (ɥɨɝɢɤɚ ɩɪɨɝɪɚɦɦ)ɋɢɧɬɚɤɫɢɫ ɞɢɧɚɦɢɱɟɫɤɨɣ ɥɨɝɢɤɢ ɫɨɫɬɨɢɬ ɢɡ ɞɜɭɯ ɱɚɫɬɟɣ:ɉɪɨɝɪɚɦɦɵɎɨɪɦɭɥɵA {a1 , a2 ,..., an } - ɧɚɛɨɪ ɛɚɡɨɜɵɯ ɞɟɣɫɬɜɢɣP {M1 , M2 ,..., Mn } - ɧɚɛɨɪ ɛɚɡɨɜɵɯ ɭɫɥɨɜɢɣ(ɨɩɟɪɚɬɨɪɨɜ)(ɩɪɨɩɨɡɢɰɢɨɧɧɵɯ ɩɟɪɟɦɟɧɧɵɯ)1) a A - ɩɪɨɝɪɚɦɦɚ;1) M P - ɮɨɪɦɭɥɚ;2) 31 , 3 2 - ɩɪɨɝɪɚɦɦɚ;2) M1 & M2 , M1 M2 , M1 o M2 , M - ɮɨɪɦɭɥɵ;3) 31 || 3 2 - ɩɪɨɝɪɚɦɦɚ (|| 3) ɟɫɥɢ ɉ – ɩɪɨɝɪɚɦɦɚ, ɬɨ [3 ]M - ɮɨɪɦɭɥɚ.ɧɟɞɟɬɟɪɦɢɪɨɜɚɧɧɵɣ ɜɵɛɨɪ);4) (3 i ) * - ɩɪɨɝɪɚɦɦɚ;5) M ? - ɩɪɨɝɪɚɦɦɚ (ɬɟɫɬ; M - ɮɨɪɦɭɥɚ).ɉɪɢɦɟɪ: ɜɵɪɚɠɟɧɢɟ {M } <if A then ɉ1 else ɉ2 fi > {\ } , ɡɚɩɢɫɚɧɧɨɟ ɜ ɬɟɪɦɢɧɚɯ ɥɨɝɢɤɢɏɨɚɪɚ, ɜ ɬɟɪɦɢɧɚɯ ɞɢɧɚɦɢɱɟɫɤɨɣ ɥɨɝɢɤɢ ɛɭɞɟɬ ɜɵɝɥɹɞɟɬɶ ɤɚɤ M o [( A ?, 31 ) (A ?, 3 2 )]\ .24224.2{M & A} 31 ! {\ },{M & A} 3 2 ! {\ }(ɜɟɬɜɥɟɧɢɹ){M & A} if_A_then_31_else_3 2 _fi ! {\ }23.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
