Реферат: Написание программ вычисления факториалов

{x=Y Ù y=X Ù t=Y}

x : =y ;

{x=X Ù y=X Ù t=Y}

y : = t ;

{x=X Ù y=Y Ù t=Y}

или

{x=Y Ù y=X} t : =х ; x : =y ; y : = t ; {x=ХÙ y=Y}.

Что и требовалось доказать.

Условный оператор.

Условный оператор в большинстве языков программирования реализует операцию композиции “выбор”. Этот оператор позволяет выбрать ту или иную последовательность операторов в зависимости от текущего состояния вычислительного процесса.

Пример 10.4.

if x=>0 then z: =x else z: =-x.

В результате выполнения этого условного оператора, переменная z получит значение, равное абсолютной величине х .

Согласно синтаксису языка Pascal, между ключевыми словами if и then должно стоять логическое выражение. Если значение этого логического выражения Т, то выполняется оператор, стоящий после then, если - F, то оператор, стоящий после else.

Определение 10.3.

wp(if B then S₁ else S₂ , R) =

= domain (B)Ù(B ÚØB)Ù((B Þ wp(S₁ , R))Ù(ØBÞwp(S₂ , R))) ,

где domain (B) - предикат, определяющий область определения для логического выражения В.

Обычно, B - всюду определенный предикат, поэтому член domain (B) опускают, и остается

wp(if В then S₁ else S₂ , R)= B Þ wp(S₁ , R) ÙØBÞwp(S₂ , R)

Покажем, что при любых начальных условиях, выполнение оператора из примера 10.4. дает в результат в z абсолютную величину х.

wp( if x=>0 then z: =x else z: = -x , z =abs(x))=

= x ³ 0 Þ wp(z: =x , z =abs(x)) Ù x < 0 Þ wp(z: = -x , z = abs(x))=

= x ³ 0 Þ x = abs(x) Ù x < 0 Þ -x = abs(x) = TÙT = T ,

т.е., при любом предусловии этот оператор даст в качестве значения

z =abs(x).

Пример 10.5. Покажем, что при любом начальном состоянии оператор

if x=>y then z: =x else z: = y

дает z =max(x,y).