Теормин - шпоры, страница 6

Описание файла

PDF-файл из архива "Теормин - шпоры", который расположен в категории "к экзамену/зачёту". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 6 страницы из PDF

(ɫ) 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.

Свежие статьи
Популярно сейчас