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

=((x ³ y) Þ( z: =x, z =max(x,y))) Ù ((x<y) Þ ( z: =y, z =max(x,y)))=

=(x ³ y) Þ (x=max(x,y)) Ù ((x<y) Þ (y= max(x,y))= TÙT = T.

Пример 10.6. Покажем, что

wp(if x=>y then z: =x else z: = y , z =y)= (x £ y).

wp(if x=>y then z: =x else z: = y , z =y)=

(x ³ y) Þ ( z: =x, z =y) Ù (x<y) Þ ( z: =y, z =y)=

(x ³ y) Þ (x=y) Ù (x<y) Þ (y=y)=(x £ y).

У читателя может сложиться мнение, что для доказательства того, что было сделано в этих примерах, потрачено слишком много усилий. В конце концов, это можно было получить, руководствуясь интуитивными соображениями. Однако, важно уже сейчас научиться проделывать подобные формальные преобразования. Это приведет к лучшему пониманию условного оператора. При построении и анализе некоторых программ, эта техника будет совершенно необходима. Даже выполнение небольшого числа упражнений будет способствовать изменению привычных для нас способов обдумывания программ и того, что называется интуицией программиста.