Евгений Корныхин - Формальная спецификация программ (Евгений Корныхин - Формальная спецификация программ.pdf), страница 7

Что это означает?1.6. Эксплицитное и имплицитное описание функций551.17.2 Когда Ясон кинул в середину войска, выросшего из зубов дракона, камень, все воины передрались и перебили друг друга. Переведитеэто утверждение на формальный язык.1.17.3на нем.1.17.4Ограниченная сверху и снизу на [a, b] функция непрерывнаФункция имеет разрыв 2-го рода в точке 0.1.17.5 Функция, имеющая точку разрыва, не может быть непрерывной.1.17.6Монотонная на [a, b] функция ограничена снизу на [a, b].1.17.7 Если последовательность ограничена, то она имеет предельную точку.1.17.8 Чтобы установить рекорд, необходимо иметь способности, иприлежно тренироваться, и найти хорошего тренера.1.17.9 Чтобы победить, нам необходимы и хорошие нападающие, ихорошие защитники, и хорошие вратари.1.17.10 Если вчера Петров прогулял два занятия, то сегодня толькоодно.1.17.11 Все члены Политбюро, избранного на XIV съезде ВКП(б),ненавидели друг друга.1.17.12Все философы критиковали друг друга.1.17.13Все рыцари сражались друг с другом на поединках.1.17.14Все начальники подсиживают друг друга.1.17.15Все мужчины — подонки, а мой муж — хороший человек.1.17.16Сдай экзамен на «отлично», и поступишь в аспирантуру.56Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)Для данной явной спецификации построить эквивалентную неявную спецификацию1.18.1123variable x : Intvalue f : Int → write any Intf ( t ) ≡ ( x := t ; x )1.18.2123variable x : Intvalue f : Int → write any Intf ( t ) ≡ ( i f x = t then x e l s e t end )1.18.3123variable x : Intvalue f : Int × Int → write any Unitf ( u , v ) ≡ ( i f u>v then x :=u e l s e x :=v end)1.18.4123variable x : Intvalue f : Int → write any Intf ( t ) ≡ ( x := t ; x := abs x ; x )1.18.5123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( x := y ; x+t )1.18.6123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( i f x = y then x e l s e t end )1.18.71.6.

Эксплицитное и имплицитное описание функций123variable x , y : Intvalue f : Int → write x Intf ( y ) ≡ ( x := y ; x )1.18.8123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y := x ; x := t ; y−x )1.18.9123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( x := t ; x+y )1.18.10123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y := x ; x − 2* t )1.18.11123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( x := t−x ; y−x )1.18.12123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y := x−y ; x := x−y ; y−x )1.18.13123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y :=t ; y :=x+y ; x )1.18.145758123Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y :=x ; y :=y ; x−2*t )1.18.15123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( x :=t−x ; x :=t−x ; y−x )1.18.16123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( y := x−y ; y := x−y ; x−y )1.18.17123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( i f x > 0 then y := x e l s e x := y end ; t )1.18.18123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( i f y < x then y := t e l s e x := t end ; x )1.18.19123variable x , y : Intvalue f : Int → write any Intf ( t ) ≡ ( i f x = t then x := y−1 e l s e x := y+1 end ; t )1.18.2012345value f : Int × Int × Int → write x , y read z Int × Intf ( a , b , c ) ≡ i f x ≡ 0−y then( i f c > b+1 then x :=y+1;0−c e l s e x :=y ; c end ,( i f a+x < z then 0−c e l s e x :=y+2; b*a end)−x )e l s e ( y , x :=b ; a+b ) end1.6.

Эксплицитное и имплицитное описание функций591.18.211234value f : Int × Int → write x , y , c Int × Int × Intf ( a , b ) ≡ l o c a l variable v : Int := x infor i in ⟨ a+ 1 . . x ⟩ do v := v+2*(x :=i ; y :=x*y ; x+i )end ; ( c *b , x :=x−v ; a*b , v*v−b* c ) end1.18.2212345value f : Int × Int × Int → write x , y write z Int × Intf ( a , b , c ) ≡ i f b ̸= 0 ∧ a \ b = z then( i f a+b > c+b then y :=( z :=z +1; z ) ; a e l s e a/b end , x :=a*y ;( i f c>y then y :=x+c ; x e l s e y :=x−c ;0− c end)\ b )e l s e ( z :=x ; x , x :=a+b ; z ) end1.18.23123456value f : Int × Int → write x , y , z Int × Int × Intf ( a , b ) ≡ x := 2 ; l o c a l variable v : Int := 1 infor i in ⟨ a . .

a−1 +b ⟩ doi f x > 0 then v := v+1 end ;l e t u = v*v in v := i *( x :=x+u ; i )*2 endend ; ( y := z ; a , v :=v+1;x , b+v ) end1.18.241234567value f : Int × Int × Int → write x , y , z Int × Intf ( a , b , c ) ≡ i f x ̸= y then( i f a−b < c then y :=b*x ; int real be l s i f a−y>c then x :=a*y ; a+ye l s e x−y end ,( a+b ) * ( i f x>0 then c e l s e y :=c +1; 0−c end ) )e l s e ( y , x :=a−b ; y :=abs x+b ; x ) end1.18.2512345value f : Nat × Nat × Int → write x , y read z , u Int × Intf ( a , b , c ) ≡ i f a+b = z+u ⇒ x + y = z+u then( i f a*y < a* c then y :=z+u ; y e l s e x :=y−x+1; c end ,y *( i f x>a then x :=b+y ; 0−y e l s e y :=a+b ; c end ) )e l s e ( y+1, a−z+(x :=x + 1 ; 1 ) ) end60Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)Для следующих эксплицитных заданий функции запишите эквивалентное имплицитное задание без использования рекурсиии цикловГлава 2КонтрактныеспецификацииИтак, перед нами либо уже существующая программная система, длякоторой надо понять, правильная ли она, либо только еще проектируемая. В любом случае мы хотим оценить качество программной системыобоснованным образом, для чего применяем формальные техники. Мывыбрали некоторый уровень абстракции для нашей программной системы, выбрали формализм для составления модели. Теперь мы определяемся с синтаксисом модели (набором идентификаторов: имен констант,имен типов, имен функций — и их типов и сигнатур).

Т.е. сейчас естьнекая «картинка» (см. рис......), известно, на каких принципах она работает (в данном случае, работает «как черный ящик», принимая на входоперацию с аргументами, тут же выдавая на выход результат и ожидаяследующей операции), но не заданы сами операции.Поэтому теперь «на этом скелете» можно формулировать ожидаемые функциональные свойства операций: в каких ситуациях каким образом «ведут себя» операции (т.е.

какой возвращают результат, какойосуществляют побочный эффект). Сейчас мы ограничимся только свойствами корректности операций, т.е. это такие свойства, при выполнении которых программную систему можно назвать правильной, а приневыполнении — нельзя.

Поскольку нами выбран формализм, то и свойства корректности мы будет формулировать в рамках этого формализма.А именно, у нас есть входные данные с операциями, выходные данныес операциями, есть внутреннее состояние, есть представление о том, чтовозможны цепочки операций. Значит, у нас есть следующие возможностидля выражения того, является ли система правильной:6162Глава 2. Контрактные спецификации∙ если на допустимые входные данные она возвращает правильносоответствующие им выходные данные;∙ если система никаким воздействием не приводится к недопустимому, несогласованному, разрушающему, внутреннему состоянию(safety).Для выражения свойств первого вида применяются программные контракты, для выражений свойств второго вида — инварианты состояния.В заключении хочется ещё раз подчеркнуть, что рассматриваемые вданном курсе формализмы достаточно простые и далеко не единственные в software engineering.

Если эти формализмы читателю покажутся недостаточно полезными, имеет смысл посмотреть в сторону другихформализмов, но ни в кое случае не «ставить крест» сразу на всех формальных методах.2.1Программные контракты1Программный контракт операции состоит из предусловия и постусловия. Первое фиксирует требования к корректному использованию этойоперации со стороны окружения системы — при каких ограничениях нааргументы обращение к этой операции корректно.

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

Эти группы почти всегда1Текст раздела взят из статьи В.В.Кулямина «Критерии тестового покрытия, основанные наструктуре контрактных спецификаций», опубликованная в томе 14 «Трудов Института системногопрограммирования»2.2. Ситуации и ветви функциональности63соответствуют компонентам или модулям системы, ответственным за реализацию этих функций.

Часто такие компоненты имеют внутреннее состояние, недоступное для непосредственного наблюдения извне системы,но влияющее на поведение вызываемых операций компонента и изменяемое ими.Поэтому для описания ограничений в пред- и постусловиях необходимо как-то учитывать внутреннее состояние компонента, операции которого описываются.

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