Информатика и выч. техника \ Информатика

Решение задачи по управлению самолетами и аэродромами, страница 2

№4

№	класс	расстояние
0	1	5
1	2	1
2	2	4
3	4	4
4	3	1
5	5	3
6	1	5

№	Принятые самолеты		Кол-во принятых	класс	Макс-е кол-во	Расстояния до самолетов
№	Принятые самолеты		Кол-во принятых	класс	Макс-е кол-во	0	1	2	3	4	5	6
0	0	6	2	3	2	5	3	9	2	15	2	4
1			2	2	2	4	7	5	9	9	1	7
2	5		1	5	1	2	2	5	8	7	2	11

P₁=do x,y: = x + y, y - 1 until y = 0 od

1)Преобразуем программу P₁ в эквивалентную программу P₂.

P₂ = x,y : = x + y, y - 1; while y ≠ 0 do x,y := x + y, y - 1 od

Докажем, что [P₁] = [P₂]. Регулярное выражение, соответствующее P_1, будет выражение (ab)⁺, если символом ‘a ‘ будем обозначать оператор x:= x + y, а символом ‘ b’ будем обозначать оператор y: = y - 1.

Регулярное выражение соответствующее P₂ – ( ab) (ab)^* = (ab)⁺.

Таким образом, программы P₁ и P₂ эквивалентны по выполнению и следовательно, эти программы эквивалентны функциональны. В этом случае достаточно доказать правильность программы P₂.

Программа P₂ не является элементарной программой. Следовательно, для доказательства её правильности необходимо выделить элементарные подпрограммы, из которых сконструирована программа P₂.

P₂ = x,y := x + y, y - 1; P^‘2;

P^‘2 = while y ≠ 0 do x,y := x + y, y - 1 od

Теперь рассмотрим подпрограмму P^‘2. Определить программную функцию и инвариант для этой программы: цикл не зацикливается при

y ³ 0, так как на каждом шаге ‘y’ уменьшается на единицу, а к ‘x’ прибавляется ‘y’, таким образом, начальное значение ‘x’ увеличится на .

Следовательно, предполагаемая функция f=( y³0®x, y: = , 0) Естественно, что с начала необходимо доказать правильность определённой функции, и только потом, используя эту функцию, строить инвариант для данной элементарной, циклической программы.

function (x,y - целые числа)

f=( y³0®x, y: = , 0)

program

while y ≠ 0 do x,y := x + y, y - 1 od

proof

term

Начальное значение y ≥ 0 при каждой итерации уменьшается на 1, так что в итоге

while _ тест примет значение ложно

pass

while_test true ( доказать (p ® f)=(p ® f ° g))

фрагмент	условие	x	y
y ≠ 0	y₀ ≠ 0	x₁=x₀	y₁=y₀
x,y := x + y, y - 1		x₂ = x₁ + y₁	y₂ = y₁- 1
f=( y³0®x, y: = , 0)	y₂³ 0	x₃=	y₃= 0

выводы:

а) условие: y ≠ 0

условие: y₀ ¹ 0L y₂ ³ 0 = y₀ ¹ 0L y₁ - 1³ 0

= y₀ ¹ 0L y₀ - 1³ 0

= y₀ ¹ 0L y₀ ³ 1

= y₀ > 0

б) присваивание: x₃ =

Функция программы:

f=(y > 0®x, y:=, 0), которая при значении while _теста истина совпадает с заданной функцией.

pass

while_test false (доказать ( Ø p ® f ) = (Øp ® I))

(y = 0 ®( y ³ 0®x, y := , 0))

= (y = 0 ® x, y := , 0)

= (x = 0 ® x, y := x, y)

т.е. получили тождественную функцию, что и требовалось доказать

pass

result

pass comp

3) определим инвариант:

X	f(X)	f(X₀)
x
y	0	0

Согласно теореме об инвариантах для построения инварианта необходимо приравнять компоненты, соответствующие f(X) и f(X₀):

1) =

2) 0 = 0

Первый инвариант представляет интерес, т.к. характеризует функцию. Учитывая второе соотношение у = у₀, предикат = перепишем (x - x₀) = - . 1) этот предикат верен перед выполнением цикла, т.к. x = x₀, аy = y₀; 2) этот предикат выполняется во время выполнения цикла (x - x₀) = - ; 3) после выполнения цикла у = 0. Следовательно, получаем (x - x₀) =, а это есть предикат x =х₀+L у = 0, что соответствует функции программы.