Построение программ
Построение программ.
Основные принципы:
1. программа и доказательства ее правильности должны строиться одновременно
2. строя программу надо пользоваться и теорией и здравым смыслом
3. изучите свойства объектов, с которыми должна работать программа
4. никогда не отвергайте как очевидный никакой фундаментальный принцип
5. программирование – это целенаправленная деятельность
Целенаправленная деятельность значит –
{?} S {R: z=max(x,y)} и {T} S {?}
Рекомендуемые материалы
6. уточните и разъясните себе предусловие и постусловие
Пусть есть задача
Определено предусловие {T} S {?}
Нужно найти максимальное из 2-х чисел.
{T} S { R: z=max(x,y)}
напишем программу исходя из предусловий и постусловий.
R: z:=x Ù x³y Ú z=y Ù y³x расписали что значит максимум
S - ?
Выскажем две гипотезы
S
z:=x
z:=x+1
Возьмем первую гипотезу, т.к. она проще и следует из R.
Найдем условие, такое что из z:=x получаем R.
Wp(“z:=x”,R) = x Ù x³y Ú z=y Ù y³x = x³y Ú x=y = x³y
Программа z:=x при условии х³у приведет к R.
if
x³y ® z:=x
fi
Какие еще охраны можно написать?
Можно еще написать команду z:=у, подставив получим х£у.
Теперь можно написать программу S.
z:=y
wp(“z:=y”,R)=y³x
S:
if
x³y ® z:=x
y³x ® z:=y
fi
Теперь можно доказать, что это правильно (по теореме о команде выбора)
- Q Þ BB
Люди также интересуются этой лекцией: Методология проектирования программных продуктов.
T Þ (x³y)Ú(y³x)=(FÚT)=T
1.1 Q Ù B1 Þ wp(S1, R)
T Ù x³yÞwp(“z:=x”, z=max(x,y))=(x³yÞx=max(x,y))=T
1.2 Q Ù B2 Þ wp(S2, R)
T Ù y³xÞwp(“z:=y”, z=max(x,y))=(y³xÞy=max(x,y))=T
При прочих равных условиях делайте охраны в командах выбора настолько, сильными насколько возможно, с тем, чтобы некоторые ошибки приводили к аварийному останову.