Учебное пособие по методам Флойда, страница 9
Описание файла
PDF-файл из архива "Учебное пособие по методам Флойда", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 9 страницы из PDF
Доменом всех переменных является множество целых чисел.START:( y1, y2 ) ( 2x, 1 )TFy1 ≠ 0Ty1 > 0( y1, y2 ) ( -y1- 1, y1⋅y2 )FHALT:z y2( y1, y2 ) ( -y1 + 1, -y1⋅y2 )782.5.4 Доказать полную корректность программы относительно спецификации (x 0) ∧ (x ⋮ 2) и ( z x2 + 2x + 3). Доменом всех переменных является множество целых чисел.START:( y1, y2, y3 ) ( 1, 3, -2 )TFy1 ≤ хTy2 > y3 + 6HALT:z y2 + y3 + 2y1 0( y1, y2 ) ( y1 + 1, y2 - y1 + 3)y3 3y1 + y3 - 579F2.5.5 Доказать полную корректность программы относительно спецификации (x 1) ∧ (x ⋮ 3) и ( z (2x + 1)2). Доменом всех переменных является множество целых чисел.START:( y1, y2, y3 ) ( 1, 2, -2 )TFy1 ≤ хTFHALT:z y2 + y3 + 1y2 > y3 + 4( y1, y2 ) ( y1 + 1, y2 - y1 + 2)y1 0y3 9y1 + y3 - 11802.5.6 Доказать полную корректность программы относительно входного предиката (x1 0) ∧ (x2 0) ивыходного предиката (0 z2 x2) ∧ (x1 z1x2 + z2).
Доменом всех переменных является множество целыхчисел.START:( y1, y2, y3 ) ( 0, 0, x1 )FTy3 0y1 if (y2+1 x2) then (y1 + 1) else y1y2 if (y2+1 x2) then 0 else (y2 + 1)HALT:( z1, z2 ) ( y1, y2 )y3 y3 1812.5.7 Доказатьполнуюкорректностьпрограммыотносительноспецификации ( z (x + 2)2 ). Доменом всех переменных является множество целых чисел.START:( y1, y2, y3 ) ( 1, 1, 1 )TFy1 ≤ хTFHALT:z y2 + 2 y3 + 1y2 > y3( y1, y2 ) ( y1+1, y2 - 2y1 + 1)y1 0y3 2y1 + y3 - 182 (x 3)и2.5.8 Доказать полную корректность программы относительно входного предиката (x 0) и выходногопредиката ( z x2 ). Доменом всех переменных является множество целых чисел.
Оператор odd(y)принимает истинное значение, при нечетном значении аргумента y.START:( y1, y2, y3 ) ( 0, 1, 1-x )FTy3 ≥ xFTHALT:z y1odd(y2)( y2, y3 ) ( y2+1, y3 +1 )( y1, y2, y3 ) ( y1 + y2, y2+1, y3+1 )832.5.9 Доказать полную корректностьSTART:(y1, y2, y3, y4 ) (1, 1, 0, 1)программы относительно входного предиката (x > 0) и выходного предиката ( |z| |x| ) при помощи методовTФлойда.
Доменом всех переменных является множество целых чисел.T y1 y1 1Ty2 > 0 y4 y4- y1Fy1 хy3 ≥ 0y3 y4F y4 y4+y1HALT:z y3 + y4( y2 , y3 ) (y1 y4 , y3 + y4)84F2.5.10 Доказать полную корректность программы относительно входного предикатавыходного предиката ( z x3). Доменом всех переменных является множество целых чисел.START:( y1, y2, y3 ) ( x, 1, x )TFy2 y3TFy3 x( y1, y2 ) ( y1 x, y2 1 )HALT:z y1y3 y185 (x 1) и2.5.11 ДоказатьполнуюSTART:( y1, y2, y3, y4 ) (0, 0, 0, 0 )корректность программы относительно входного предиката (x 0) ∧ (x ⋮ 2) и выход-Fного предиката ( z x2 )при помощи методов Флойда.Fy1 = xДоменом всех переменных является множество целых чисел.FTy3 = 1( y1, y2 ) ( y1 + 1,y2 y1 )( y1, y2 ) ( y1 + 2, y2 1 )86y4 = 4TTHALT:z y2 + y3y1 0y4 1 + y4y3 1 – y32.5.12 Доказать полную корректность программы относительно входного предиката (x 0) ивыходного предиката ( z x2) при помощи методов Флойда.
Доменом всех переменных являетсямножество целых чисел.START:( y1, y2 ) ( x, 1 )TFy2 xT( y1, y2 ) (2y1, 2y2 )2y2 xFHALT:z y1( y1, y2 ) ( y1 x, y2 1 )872.5.13 Доказать полную корректность программы относительно спецификации (x 0) и ( if x = 1then z = 3 else z = x2 ). Доменом всех переменных является множество целых чисел.START:( y1, y2 ) ( 0, 0 )y2 y2 + 1FTy1 = xy2 y1 + y2 - 1y2 2 ∙ y2y1 1 + y1Fy2 ≥ y188THALT:z y1 + y22.5.14 Доказать полную корректность программы относительно входного предиката (x2 0) иxвыходного предиката (z = x 1 2 ) при помощи методов Флойда. 0 0 считается равным 1.
Доменом всехпеременных является множество целых чисел. Оператор odd(y) принимает истинное значение, при нечетномзначении аргумента y.START:( y1, y2, y3 ) (x1, x2, 1)FFy2 0THALT:z y3odd(y2)( y1, y2 ) ( y1 y1, y2 /2 )T( y2, y3 ) ( y2 1, y1 y3 )892.5.15 Доказать полную корректностьпрограммы относительно входного преди-START:( y1, y2 ) ( 0, 0 )ката (x 0) и выходного предиката ( z x2 ) при помощи методов Флойда.Доменом всех переменных является мно-y2 = xжество целых чисел. A div B обозначаетлена только для неотрицательных А и по-HALT:z y1Fоперацию получения частного от деленияцелого А на целое В. Эта операция опреде-TTFy2 y2 + 1y2 = xложительных В.y1 2y2 + y1F90y1 y1 - 1(y1 - 1) div y2 = y2T2.5.16 Доказать полную корректность програ-м-START:( y1, y2, y3 ) ( 0, 0, 1 )мы относительно следующего входного предиката (x 0)ивыходногопредиката ( z3 x (z + 1)3 ).
Доменом всех переменныхявляется множество целых чисел.y2 y2 + y3Fy1 y1 + 1y3 y3 + 6 y191y2 xTHALT:z y12.5.17 Доказать полную корректность программы относительно входного предиката (x > 0) (x ⋮ 2) ивыходного предиката ( z x2 ) при помощи методов Флойда. Доменом всех переменных являетсямножество целых чисел.START:( y1, y2, y3) ( 0, 0, 0 )FTy3 ⋮ 2( y2, y3 ) ( y2 + y3, y3 + 1 )HALT:z 2⋅(y1+ y2 ) - y3 + 1( y1, y3 ) ( y1 + y3, y3 + 1 )FTy3 < x922.5.18 Доказать полную корректность программы относительно входного предиката (x 0) (x ⋮ 2) ивыходного предиката ( z x2 ) при помощи методов Флойда. Доменом всех переменных являетсямножество целых чисел.START:( y1, y2, y3 ) ( x, -x, 0 )FTy1 = 0Fy2 0( y1, y3 ) ( y1 - 1, y3 x )( y1, y2, y3) (x, y2+1, -y3)ac93THALT:z y32.5.19 Доказать полную корректность программы относительно входного предиката (x > 0) (x ⋮ 2) ивыходного предиката ( z x2 ) при помощи методов Флойда.
Доменом всех переменных являетсямножество целых чисел. rem(x,y) — оператор взятия остатка от целочисленного деления, который не определенпри y=0.START:(y1, y2, y3, y4) (0,x,2,0)TFrem(y2 , y3) = 0( y1, y2, y3 ) ( y1 + x, y2 - 1, 2)( y2, y3, y4 ) (y2 -1, y3-1, y3+y4)TFy2 >0HALT:z 2⋅y1 - y4 + 3942.5.20 Доказать полную корректность программы относительно входного предиката (x > 0) ивыходного предиката ( z x3 ) при помощи методов Флойда.
Доменом всех переменных являетсямножество целых чисел. div(x,y) — оператор целочисленного деления, который не определен при y=0.START:( y1, y2, y3, y4 ) ( 1, x, 0, 0 )FTy2 >0( y1, y2, y3, y4) ( y3, x, 0, y3 + y4)( y2, y3 ) ( y2 - 1, y3 + x )FTdiv(y4 , y1) ≥ x95HALT:z y42.5.21 Доказать полную корректность программы относительно входного предиката (x 0) ивыходного предиката ( z2 x (z + 1)2 ) при помощи методов Флойда. Доменом всех переменныхявляется множество целых чисел.START:( y1, y2 ) ( x, (x+1)/2 )FTy1 = 0FTy1 ≤ 3FTHALT:z1y2 ≥ y1( y1, y2 ) ( y2, (x/y2 + y2)/2HALT:z y196HALT:z02.5.22 Доказать полную корректность программы относительно входного предиката (x 0) (x ⋮ 2) ивыходного предиката (z x2) при помощи методов Флойда.
Доменом всех переменных является множествоцелых чисел. rem(x,y) — оператор целочисленного деления, который не определен при y=0.START:( y1, y2, y3 ) ( 1, -x, -x )F( y1, y2, y3 ) ( y1+1, y2+1, y3x )Ty2 ⋮ 2Ty1 < x( y1, y2) ( rem(y1+1,x), y21 )97FHALT:z y2 + y3 +1Литература1. R. W. Floyd, "Assigning meanings to programs", Proc. Symp.Appl. Math., 19; in: J.T.Schwartz (ed.), Mathematical Aspectsof Computer Science, pp. 19-32, American MathematicalSociety, Providence, R.I., 1967.2.
N.Francez,"Verificationofprograms",Addison-WesleyPublishers Ltd., 1992.3. Z. Manna, "Mathematical theory of computation", McGraw-Hill,1974.4. Z. Manna, A. Pnueli, "The Temporal Logic of Reactive andConcurrent Systems", Springer-Verlag, 1991.5. Р.Андерсон,"Доказательствоправильностипрограмм",Москва, Мир, 1982.6. Д. Жуков, "Методы верификации программ", ПереславльЗалесский, 2002.98.
