Контрольная работа по "Программированию и компьютерам"

Министерство образования  и науки Российской Федерации

федеральное государственное бюджетное  образовательное учреждение

высшего  профессионального образования

 

«ПЕРМСКИЙ НАЦИОНАЛЬНЫЙ ИССЛЕДОВАТЕЛЬСКИЙ 

ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ»

 

 

 

 

 

Контрольная работа

по дисциплине “Теория программирования”

 

 

 

 

 

 

Выполнил студент

Группы: АСУзу-10-2

                                                                        Жаровин Н.С.

Проверил преподаватель:

                                   Кузнецов Д.Б.

 

 

 

 

 

 

 

 

 

 

 

Пермь – 2011

Контрольная работа №1

 

1. Вычислить wp и упростить.

 

a. wp("x:=x*(y-1)", x*y=c) = (x*(y-1)*y=c) = (xyy-xy=c)

 

b. wp("x:=x-2*y; skip", x>y) = wp("x:=x-2*y", wp("skip", x>y)) = wp("x:=x-2*y", x>y) = (x-2*y>y) = (x>3y)   

 

c. wp("x:=2*y-x; abort", x>y) = False  

 

d. wp("x:=x+y; y:=y-x", x=y-c) = wp("x:=x+y", wp("y:=y-x", x=y-c)) = wp("x:=x+y", x=y-x-c) = (x+y=y-(x+y)-c) = (x+y=y-x-y)-c) = (y=-2x-c)

 

e. wp("b[n-1]:=5", Эk:0<=k<n : b[k]<5) = wp("b=(b; n-1:5)", Эk:0<=k<n : b[k]<5) = Эk:0<=k<n:(b; n-1:5)[k]<5 = (b; n-1:5)[n-1]<5 & Эk:0<=k<n-1 : (b; n-1:5)[k]<5 = 5<5 & Эk:0<=k<n-1 : b[k]<5 = F

 

2. Найти X

 

{a*b=c} a,b:=a*2,x {a*b=c}

где С - неизвесная константа

wp("a,b:=a*2,x", a*b=c) = (a*2*x=c)

a*2*x = a*b

x=(a*b)/(2*a) = b/2

a,b:=a*2, b/2

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Контрольная работа №2

 

Проверить соответствие программы спецификации

 

1.

{a=2 v b=a}

if                                    

   a=2 -> b:=a      

   b=2 -> a:=2

fi

   {a=2 & b=2}

 

Теорема о команде  выбора

 

1) Q => BB                     

a=2 v b=a => a=2 v b=2 ≡ T

 Доказательство

 

 2.1) Q&Bi => wp(Si, R)

        (a=2 v b=a) & a=2 => wp(“b:=a”, a=2 & b=2) ≡ T

 

2.2) (a=2 v b=a) & b=2 => wp(“a:=2”, a=2 & b=2)

          a=2 & b=2 => wp((“a:=2”, a=2 & b=2) ≡ T

 

 

 

2.

{n≥1}

i,b[0]:=1, 7

{P: (Vk: 0≤k<i : b[k]=7) & 0≤i≤n}  

{t:n-i} 

Do                       

    i≠n & b[i]=7 -> i:=i+1

    i≠n & b[i]=7 -> i,b[i]:=i+1, 7

od

{R: Vk: 0≤k<i : b[k]=7}            

 

Список условий для  проверки цикла

 

1) P истинно перед выполнением цикла

Wp(“i,b[0]:=1, 7”, P) = (Vk: 0≤0<1: b[0]=7) & 0≤1≤n ≡ T

 

2.1) {P&Bi} Si {P}  P является инвариантом цикла

        ((Vk:0≤k<i : b[k]=7) & 0≤i≤n) & (i≠n & b[i]=7) =>

        => wp(“i:=i+1”, ((Vk: 0≤k<i : b[k]=7) & 0≤i≤n))

       ((Vk:0≤k<i : b[k]=7) & 0≤i≤n) & (i≠n & b[i]=7) => (Vk: 0≤k<i+1: b[k]=7) & 0≤i+1≤n

…b[k]=7 & b[i]=7 … => …b[k]=7…≡ T

0≤i => 0≤i+1 ≡ T

i≤n & 1≠n => i+1≤n ≡ T

 

2.2) ((Vk:0≤k<i : b[k]=7) & 0≤i≤n) & (i≠n & b[i]≠7) =>

=> wp(“i,b[i]:=i+1, 7”, ((Vk: 0≤k<i : b[k]=7) & 0≤i≤n))

((Vk: 0≤k<i : b[k]=7) & 0≤i≤n) & (i≠n & b[i] ≠7) =>

=> (Vk: 0≤k<i+1 : b[k]=7) & 0≤i+1≤n

… b[k]=7… =>… b[k]=7… ≡ T

0≤I => 0≤i+1 ≡ T

i≤n & i≠n => i+1≤n ≡ T

 

 

3) Выполнение P и не выполнение BB должно дать R: P & ⌐BB =>R

BB =  i≠n & B[i]=7 v i≠n & b[i] ≠7 = i≠n(b[i]=7 v b[i] ≠7) = i≠n & 1 = i≠n

P & i = n => R

(Vk: 0≤k<i : b[k]=7) & 0≤n≤n = Vk: 0≤k<n : b[k]=7 ≡ T

 

 

4) Если цикл еще не закончен, то ограничивающая функция положительна: P & BB => t>0

P & i≠n => t>0

P & i≠n => n-i>0 [n>i]

0≤i≤n & i≠n => n>i

 

 

5) Каждый шаг цикла ведет к концу цикла

{P & Bi} t1:=t; Si {t<t1}

 

1. {P & i≠n  & b[i]=7} t1:=t; Si{t<t1}

       {P & i≠n  & b[i]=7} t1:=n-i; i:=i+1 {t<t1}

        wp(“t1:=n-i; i:=i+1”, n-i<t1) = wp(“t1:=n-i”, n-i-1<t1) =  n-i-1< n-I = -1<0 = 1>0 ≡ T

 

2. {P & i≠n  & b[i]=7} } t1:=n-i; i,b[i]:=i+1, 7

        wp(“t1:=n-i; i,b[i]:=i+1, 7”,  n-i<t1) = wp(“t1:=n-i”, n-i-1<t1) = n-i-1< n-i = 1>0 ≡ T

 

 

2. 2.2  ((Vk:0≤k<i : b[k]=7) & 0≤i≤n) & (i≠n & b[i]≠7) =>

=> wp(“i,b[i]:=i+1, 7”, ((Vk: 0≤k<i : b[k]=7) & 0≤i≤n))

            Wp(“b:=(b; i:7), i:=i+1”, ((Vk: 0≤k<i : b[k]=7) & 0≤i≤n)) =

            = (Vk: 0≤k<i+1 : (b; i:7)[k]=7) & 0≤i+1≤n =

            = 7 = 7 & (Vk: 0≤k<i: (b; i:7)[k]=7) & 0≤i+1≤n

    

7 = 7 & (Vk: 0≤k<i: (b; i:7)[k]=7) & 0≤i+1≤n

7 = 7 & (Vk: 0≤k<i: b[k]=7) & 0≤i+1≤n

… b[k]=7… =>… b[k]=7… ≡ T

0≤i => 0≤i+1 ≡ T

i≤n & i≠n => i+1≤n ≡ T

 

 

 

 

 

 

 

 

 

 

 

Контрольная работа №3

 

Найти ближайшее к n число  кратное 3 снизу.

 

{n≥0} S {x≤n<x+3 & x mod 3 = 0}         

{n≥0}

x:=0

{P: x≤n & x mod 3 = 0} 

{t: n-x}

do

     n>x+3 -> x:=x+3

od

{R: x≤n<x+3 & x mod 3 = 0}

 

 

 

Список условий для  проверки цикла

 

Проверка:

1. P истинно перед выполнением цикла

Wp(“x:=0”, P) = 0≤n & 0 mod 3=0 ≡ T

 

2. {P&Bi} Si {P} P является инвариантом цикла.

(x≤n & x mod 3=0) & (n> x+3) = > wp(“x:=x+3”, x≤n & x mod3=0)

(x≤n & x mod 3=0) & (n> x+3) => x+3≤n & (x+3) mod3 = 0

…x mod3=0… => …(x+3)mod3=0… ≡ T

 

3. P & ⌐BB => R

(x≤n & x mod 3=0) & n< x+3 = x≤n< x+3 & x mod 3=0

 

4. P & BB => t>0

P & n>x+3 => t>0

P & n>x+3 => n-x>0 [x≤n]

x≤n &n>x+3 => n>x

 

5. Каждый шаг цикла ведет его к концу: {P & Bi} ti:=t; Si {t1>t}

{P & n>x+3} t1:=n-x; x:=x+3 {t<t1}

wp(“t1:=n-x; x:=x+3”, n-x<t1) = wp(“t1:=n-x”, n-x-3<t1) = n-x-3<n-x = -3<0 ≡ T

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Преобразователь предикатов wp определяет множество всех состояний, для выполнение команды S, начавшейся в таком сотоянии, закончится, через конечное время, в состоянии, удовлетворяющем R

 

Спецификация программы на языке предикатов выглядит следующим образом:

{Q} S {R}

Q – предусловие

S – программа

R – постусловие

Если выполнение S началось в состоянии удовлетворяющем Q то имеется гарантия что оно завершиться в конечное время с состоянии удовлетворяющем R

 

Спецификация программ – это  выражение на определенном языке  возможно естественном, которое точно  описывает что должно быть в результате выполнения программ.

 

Красным выделены посылки из Теоремы о цикле его инварианте и ограничевающей функции.

 

Если зафиксируем S, то получим wps(R), т.е. из одного предиката получаем другой.

 

Композиция  команд

wp(“S1 ; S2 ”,R)=wp(S1 ,wp( S2,R))

 

Частичная и полная коррекция

Если выполнение команды S начинается в состоянии, удовлетворяющем Q, и если оно

заканчивается, то конечное состояние  будет удовлетворять R.b[i]:=e обозначим b:=(b;i:e) – функциональная запись массива (берем b и по индексу i

присваиваем е).

1. wp(“b[i]:=5”,b[i]=5)=wp(“b=(b;i:5)”,b[i]=5)=((b;i:5)[i]=5)

= (5=5)=TПример: x=abs(x)

if

x≥0 -> skip

. x≤0 -> x:=-x

fi

if x<0 then x:=-x

Явное появление в тексте всех охран помогает читателю. Кроме этого каждая

альтернатива представлена во всех деталях. И возможность упустить из вида какую-

нибудь ситуацию уменьшается.

Если Р истина перед циклом, перед каждым шагом цикла и после него, то Р

истинно после цикла.

 

 

Предикат Р истинный перед  и после выполнения каждого шага цикла, называется

инвариантом цикла.