Π§ΠΈΡ‚Π°ΠΉΡ‚Π΅ ΠΊΠ½ΠΈΠ³ΠΈ ΠΎΠ½Π»Π°ΠΉΠ½ Π½Π° Bookidrom.ru! БСсплатныС ΠΊΠ½ΠΈΠ³ΠΈ Π² ΠΎΠ΄Π½ΠΎΠΌ ΠΊΠ»ΠΈΠΊΠ΅

Π§ΠΈΡ‚Π°Ρ‚ΡŒ ΠΎΠ½Π»Π°ΠΉΠ½ Β«ΠžΡΠ½ΠΎΠ²Ρ‹ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π½ΠΎ-ΠΎΡ€ΠΈΠ΅Π½Ρ‚ΠΈΡ€ΠΎΠ²Π°Π½Π½ΠΎΠ³ΠΎ программирования». Π‘Ρ‚Ρ€Π°Π½ΠΈΡ†Π° 161

Автор Π‘Π΅Ρ€Ρ‚Ρ€Π°Π½ ΠœΠ΅ΠΉΠ΅Ρ€

ΠŸΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ восстановлСнный ΠΈΠ½Π²Π°Ρ€ΠΈΠ°Π½Ρ‚ класса ΠΌΠΎΠΆΠ½ΠΎ Π½Π°ΠΉΡ‚ΠΈ Π² плоской ΠΈ ΠΊΡ€Π°Ρ‚ΠΊΠΎΠΉ плоской Ρ„ΠΎΡ€ΠΌΠ΅ послСднСго (см. Π»Π΅ΠΊΡ†ΠΈΡŽ 15).

ΠŸΡ€Π΅Π΄ΡƒΡΠ»ΠΎΠ²ΠΈΡ ΠΈ постусловия ΠΏΡ€ΠΈ Π½Π°Π»ΠΈΡ‡ΠΈΠΈ динамичСского связывания

Π’ случаС с прСдусловиями ΠΈ постусловиями ситуация Ρ‡ΡƒΡ‚ΡŒ слоТнСС. ΠžΠ±Ρ‰Π°Ρ идСя, ΠΊΠ°ΠΊ ΠΎΡ‚ΠΌΠ΅Ρ‡Π°Π»ΠΎΡΡŒ, состоит Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ любоС ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠ΅ объявлСниС Π΄ΠΎΠ»ΠΆΠ½ΠΎ ΡƒΠ΄ΠΎΠ²Π»Π΅Ρ‚Π²ΠΎΡ€ΡΡ‚ΡŒ утвСрТдСниям ΠΎΡ€ΠΈΠ³ΠΈΠ½Π°Π»ΡŒΠ½ΠΎΠΉ ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹. Π­Ρ‚ΠΎ особСнно Π²Π°ΠΆΠ½ΠΎ, Ссли ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° ΠΎΡ‚Π»ΠΎΠΆΠ΅Π½Π°: Π±Π΅Π· Ρ‚Π°ΠΊΠΎΠ³ΠΎ ограничСния Π½Π° Π±ΡƒΠ΄ΡƒΡ‰ΡƒΡŽ Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΡŽ, Π·Π°Π΄Π°Π½ΠΈΠ΅ прСдусловиС ΠΈ постусловий для ΠΎΡ‚Π»ΠΎΠΆΠ΅Π½Π½Ρ‹Ρ… ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ Π±Ρ‹Π»ΠΎ Π±Ρ‹ бСсполСзным ΠΈΠ»ΠΈ, Ρ…ΡƒΠΆΠ΅ Ρ‚ΠΎΠ³ΠΎ, ΠΏΡ€ΠΈΠ²Π΅Π»ΠΎ Π±Ρ‹ ΠΊ Π½Π΅ΠΆΠ΅Π»Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎΠΌΡƒ Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚Π°Ρ‚Ρƒ. Π’Π΅ ΠΆΠ΅ трСбования ΠΊ ΠΏΡ€Π΅Π΄ΡƒΡΠ»ΠΎΠ²ΠΈΡŽ ΠΈ ΠΏΠΎΡΡ‚ΡƒΡΠ»ΠΎΠ²ΠΈΡŽ ΠΎΡΡ‚Π°ΡŽΡ‚ΡΡ ΠΈ ΠΏΡ€ΠΈ ΠΏΠ΅Ρ€Π΅ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠΈ эффСктивных ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ.

Анализируя ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌΡ‹ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠ³ΠΎ объявлСния, ΠΏΠΎΠ»ΠΈΠΌΠΎΡ€Ρ„ΠΈΠ·ΠΌΠ° ΠΈ динамичСского связывания, ΠΌΠΎΠΆΠ½ΠΎ Π΄Π°Ρ‚ΡŒ Ρ‚ΠΎΡ‡Π½ΡƒΡŽ Ρ„ΠΎΡ€ΠΌΡƒΠ»ΠΈΡ€ΠΎΠ²ΠΊΡƒ искомого ΠΏΡ€Π°Π²ΠΈΠ»Π°. Но для Π½Π°Ρ‡Π°Π»Π° прСдставим Ρ‚ΠΈΠΏΠΈΡ‡Π½Ρ‹ΠΉ случай.

Рассмотрим класс ΠΈ Π΅Π³ΠΎ ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, ΠΈΠΌΠ΅ΡŽΡ‰ΠΈΠ΅ ΠΊΠ°ΠΊ прСдусловиС, Ρ‚Π°ΠΊ ΠΈ постусловиС:

Рис. 16.1.  ΠŸΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°, ΠΊΠ»ΠΈΠ΅Π½Ρ‚ ΠΈ ΠΊΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚

На рис. 16.1 ΠΏΠΎΠΊΠ°Π·Π°Π½ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ C класса A. Π§Ρ‚ΠΎΠ±Ρ‹ Π±Ρ‹Ρ‚ΡŒ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ΠΎΠΌ, класс C, ΠΊΠ°ΠΊ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, Π²ΠΊΠ»ΡŽΡ‡Π°Π΅Ρ‚ Π² ΠΎΠ΄Π½Ρƒ ΠΈΠ· своих ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ объявлСниС ΠΈ Π²Ρ‹Π·ΠΎΠ² Π²ΠΈΠ΄Π°:


a1: A

...

a1.r



Для простоты ΠΌΡ‹ ΠΏΡ€ΠΎΠΈΠ³Π½ΠΎΡ€ΠΈΡ€ΡƒΠ΅ΠΌ всС Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΌΠΎΠΆΠ΅Ρ‚ Ρ‚Ρ€Π΅Π±ΠΎΠ²Π°Ρ‚ΡŒ r, ΠΈ ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ, Ρ‡Ρ‚ΠΎ r являСтся ΠΏΡ€ΠΎΡ†Π΅Π΄ΡƒΡ€ΠΎΠΉ, хотя наши рассуТдСния Π² Ρ€Π°Π²Π½ΠΎΠΉ ΠΌΠ΅Ρ€Π΅ ΠΏΡ€ΠΈΠΌΠ΅Π½ΠΈΠΌΡ‹ ΠΈ ΠΊ функциям.

Π’Ρ‹Π·ΠΎΠ² Π±ΡƒΠ΄Π΅Ρ‚ ΠΊΠΎΡ€Ρ€Π΅ΠΊΡ‚Π΅Π½ лишь Ρ‚ΠΎΠ³Π΄Π°, ΠΊΠΎΠ³Π΄Π° ΠΎΠ½ удовлСтворяСт ΠΏΡ€Π΅Π΄ΡƒΡΠ»ΠΎΠ²ΠΈΡŽ. Π“Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ C ΡΠΎΠ±Π»ΡŽΠ΄Π°Π΅Ρ‚ свою Ρ‡Π°ΡΡ‚ΡŒ ΠΊΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚Π°, ΠΌΠΎΠΆΠ½ΠΎ, ΠΊ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Ρƒ, ΠΏΡ€Π΅Π΄Π²Π°Ρ€ΠΈΠ² Π²Ρ‹Π·ΠΎΠ² ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠΎΠΉ прСдусловия, написав вмСсто a1.r ΠΊΠΎΠ½ΡΡ‚Ρ€ΡƒΠΊΡ†ΠΈΡŽ:


if a1. then

a1.r

check a1.Ξ² end -- постусловиС Π΄ΠΎΠ»ΠΆΠ½ΠΎ Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡ‚ΡŒΡΡ

... Π˜Π½ΡΡ‚Ρ€ΡƒΠΊΡ†ΠΈΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΌΠΎΠ³ΡƒΡ‚ ΠΏΡ€Π΅Π΄ΠΏΠΎΠ»Π°Π³Π°Ρ‚ΡŒ ΠΈΡΡ‚ΠΈΠ½Π½ΠΎΡΡ‚ΡŒ a1.. ...

end



(Как ΠΎΡ‚ΠΌΠ΅Ρ‡Π°Π»ΠΎΡΡŒ ΠΏΡ€ΠΈ обсуТдСнии ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΠΉ, Π½Π΅ всСгда трСбуСтся ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠ°: достаточно, с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ if ΠΈΠ»ΠΈ Π±Π΅Π· Π½Π΅Π³ΠΎ, Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ условия a ΠΏΠ΅Ρ€Π΅Π΄ Π²Ρ‹Π·ΠΎΠ²ΠΎΠΌ r. Для простоты Π±ΡƒΠ΄Π΅ΠΌ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ if-Ρ„ΠΎΡ€ΠΌΡƒ, игнорируя ΠΏΡ€Π΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΠ΅ else.)

ΠžΠ±Π΅ΡΠΏΠ΅Ρ‡ΠΈΠ² соблюдСниС прСдусловия, ΠΊΠ»ΠΈΠ΅Π½Ρ‚ C рассчитываСт Π½Π° Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ постусловия a1.Ξ² ΠΏΡ€ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‚Π΅ ΠΈΠ· r.

ВсС это являСтся основой ΠŸΡ€ΠΎΠ΅ΠΊΡ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΡ ΠΏΠΎ ΠšΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚Ρƒ: Π² ΠΌΠΎΠΌΠ΅Π½Ρ‚ Π²Ρ‹Π·ΠΎΠ²Π° ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ Π΄ΠΎΠ»ΠΆΠ΅Π½ ΠΎΠ±Π΅ΡΠΏΠ΅Ρ‡ΠΈΡ‚ΡŒ соблюдСниС прСдусловия, Π° Π² ΠΎΡ‚Π²Π΅Ρ‚ ΠΏΡ€ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‚Π΅ ΠΈΠ· ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ ΠΎΠ½ полагаСтся Π½Π° Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ постусловия.

Π§Ρ‚ΠΎ происходит, ΠΊΠΎΠ³Π΄Π° вводится наслСдованиС?

Рис. 16.2.  ΠŸΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°, ΠΊΠ»ΠΈΠ΅Π½Ρ‚, ΠΊΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚ ΠΈ ΠΏΠΎΡ‚ΠΎΠΌΠΎΠΊ

ΠŸΡƒΡΡ‚ΡŒ Π½ΠΎΠ²Ρ‹ΠΉ класс A' ΠΏΠΎΡ€ΠΎΠΆΠ΄Π΅Π½ ΠΎΡ‚ A ΠΈ содСрТит ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠ΅ объявлСниС r. Как ΠΎΠ½ ΠΌΠΎΠΆΠ΅Ρ‚, Ссли Π²ΠΎΠΎΠ±Ρ‰Π΅ ΠΌΠΎΠΆΠ΅Ρ‚, Π·Π°ΠΌΠ΅Π½ΠΈΡ‚ΡŒ ΠΏΡ€Π΅ΠΆΠ½Π΅Π΅ прСдусловиС Π½ΠΎΠ²Ρ‹ΠΌ Ξ³, Π° ΠΏΡ€Π΅ΠΆΠ½Π΅Π΅ постусловиС Ξ² - Π½ΠΎΠ²Ρ‹ΠΌ ?

Π§Ρ‚ΠΎΠ±Ρ‹ Π½Π°ΠΉΡ‚ΠΈ ΠΎΡ‚Π²Π΅Ρ‚, рассмотрим ΠΎΠ±ΡΠ·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° ΠΊΠ»ΠΈΠ΅Π½Ρ‚Π°. Π’ Π²Ρ‹Π·ΠΎΠ²Π΅ a1.r Ρ†Π΅Π»ΡŒ a1 ΠΌΠΎΠΆΠ΅Ρ‚ - Π² силу ΠΏΠΎΠ»ΠΈΠΌΠΎΡ€Ρ„ΠΈΠ·ΠΌΠ° - ΠΈΠΌΠ΅Ρ‚ΡŒ Ρ‚ΠΈΠΏ A'. Однако C ΠΎΠ± этом Π½Π΅ Π·Π½Π°Π΅Ρ‚! ЕдинствСнным объявлСниСм a1 остаСтся исходная строка


a1: A



Π³Π΄Π΅ упоминаСтся A, Π½ΠΎ Π½Π΅ A'. На Π΄Π΅Π»Π΅ C ΠΌΠΎΠΆΠ΅Ρ‚ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ A', Π΄Π°ΠΆΠ΅ Ссли Π΅Π³ΠΎ Π°Π²Ρ‚ΠΎΡ€ Π½Π΅ Π·Π½Π°Π΅Ρ‚ ΠΎ Π½Π°Π»ΠΈΡ‡ΠΈΠΈ Ρ‚Π°ΠΊΠΎΠ³ΠΎ класса. Π’Ρ‹Π·ΠΎΠ² ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ r ΠΌΠΎΠΆΠ΅Ρ‚ ΠΏΡ€ΠΎΠΈΠ·ΠΎΠΉΡ‚ΠΈ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, Π² ΠΏΡ€ΠΎΡ†Π΅Π΄ΡƒΡ€Π΅ C Π²ΠΈΠ΄Π°:


some_routine_of_C (a1: A) is

do

...; a1.r;...

end



Π’ΠΎΠ³Π΄Π° ΠΏΡ€ΠΈ Π²Ρ‹Π·ΠΎΠ²Π΅ some_routine_of_C ΠΈΠ· Π΄Ρ€ΡƒΠ³ΠΎΠ³ΠΎ класса Π² Π½Π΅ΠΌ ΠΌΠΎΠΆΠ΅Ρ‚ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ фактичСский ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ Ρ‚ΠΈΠΏΠ° A', Π΄Π°ΠΆΠ΅ Ссли Π² тСкстС ΠΊΠ»ΠΈΠ΅Π½Ρ‚Π° C класс A' Π½ΠΈΠ³Π΄Π΅ Π½Π΅ упоминаСтся. ДинамичСскоС связываниС ΠΊΠ°ΠΊ Ρ€Π°Π· ΠΈ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ Ρ‚ΠΎΡ‚ Ρ„Π°ΠΊΡ‚, Ρ‡Ρ‚ΠΎ ΠΎΠ±Ρ€Π°Ρ‰Π΅Π½ΠΈΠ΅ ΠΊ r ΠΏΡ€ΠΈΠ²Π΅Π΄Π΅Ρ‚ Π² этом случаС ΠΊ использованию ΠΏΠ΅Ρ€Π΅ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠΉ вСрсии A'.

Π˜Ρ‚Π°ΠΊ, ΠΌΠΎΠΆΠ΅Ρ‚ ΡΠ»ΠΎΠΆΠΈΡ‚ΡŒΡΡ ситуация, Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ C, являясь Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ΠΎΠΌ A, фактичСски Π²ΠΎ врСмя выполнСния ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅Ρ‚ вСрсии ΠΊΠΎΠΌΠΏΠΎΠ½Π΅Π½Ρ‚ΠΎΠ² класса A'. (МоТно ΡΠΊΠ°Π·Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ C - "динамичСский ΠΊΠ»ΠΈΠ΅Π½Ρ‚" A', хотя Π² тСкстС C ΠΎΠ± этом ΠΈ Π½Π΅ говорится.)

Π§Ρ‚ΠΎ это Π·Π½Π°Ρ‡ΠΈΡ‚ для C? Волько ΠΎΠ΄Π½ΠΎ - ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π²ΠΎΠ·Π½ΠΈΠΊΠ½ΡƒΡ‚, Ссли Π½Π΅ ΠΏΡ€Π΅Π΄ΠΏΡ€ΠΈΠ½ΡΡ‚ΡŒ Π½ΠΈΠΊΠ°ΠΊΠΈΡ… дСйствий. ΠšΠ»ΠΈΠ΅Π½Ρ‚ C ΠΌΠΎΠΆΠ΅Ρ‚ добросовСстно Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡ‚ΡŒ свою Ρ‡Π°ΡΡ‚ΡŒ ΠΊΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚Π°, ΠΈ всС ΠΆΠ΅ Π² Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚Π°Ρ‚Π΅ ΠΎΠ½ Π±ΡƒΠ΄Π΅Ρ‚ ΠΎΠ±ΠΌΠ°Π½ΡƒΡ‚. НапримСр,


if a1. then a1.r end



Ссли a1 ΠΏΠΎΠ»ΠΈΠΌΠΎΡ€Ρ„Π½ΠΎ присоСдинСна ΠΊ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Ρƒ Ρ‚ΠΈΠΏΠ° A', инструкция Π²Ρ‹Π·ΠΎΠ²Π΅Ρ‚ ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ, ΠΎΠΆΠΈΠ΄Π°ΡŽΡ‰ΡƒΡŽ выполнСния Ξ³ ΠΈ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΡƒΡŽΡ‰ΡƒΡŽ Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ , Π² Ρ‚ΠΎ врСмя ΠΊΠ°ΠΊ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠ» ΡƒΠΊΠ°Π·Π°Π½ΠΈΠ΅ ΡΠΎΠ±Π»ΡŽΠ΄Π°Ρ‚ΡŒ ΠΈ ΠΎΠΆΠΈΠ΄Π°Ρ‚ΡŒ выполнСния Ξ². Налицо Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΠ΅ расхоТдСниС Π²ΠΎ взглядах ΠΊΠ»ΠΈΠ΅Π½Ρ‚Π° ΠΈ поставщика Π½Π° ΠΊΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚.

Как ΠΎΠ±ΠΌΠ°Π½ΡƒΡ‚ΡŒ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ΠΎΠ²

Π§Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠ½ΡΡ‚ΡŒ, ΠΊΠ°ΠΊ ΡƒΠ΄ΠΎΠ²Π»Π΅Ρ‚Π²ΠΎΡ€ΠΈΡ‚ΡŒ ΠΊΠ»ΠΈΠ΅Π½Ρ‚ΠΎΠ², ΠΌΡ‹ Π΄ΠΎΠ»ΠΆΠ½Ρ‹ ΡΡ‹Π³Ρ€Π°Ρ‚ΡŒ Ρ€ΠΎΠ»ΡŒ Π°Π΄Π²ΠΎΠΊΠ°Ρ‚ΠΎΠ² дьявола ΠΈ Π½Π° сСкунду ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²ΠΈΡ‚ΡŒ сСбС, ΠΊΠ°ΠΊ ΠΈΡ… ΠΎΠ±ΠΌΠ°Π½ΡƒΡ‚ΡŒ. Π’Π°ΠΊ поступаСт ΠΎΠΏΡ‹Ρ‚Π½Ρ‹ΠΉ криминалист, разгадывая прСступлСниС. Как ΠΌΠΎΠ³ Π±Ρ‹ ΠΏΠΎΡΡ‚ΡƒΠΏΠΈΡ‚ΡŒ поставщик, ΠΆΠ΅Π»Π°ΡŽΡ‰ΠΈΠΉ ввСсти Π² Π·Π°Π±Π»ΡƒΠΆΠ΄Π΅Π½ΠΈΠ΅ своСго чСстного ΠΊΠ»ΠΈΠ΅Π½Ρ‚Π° C, Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΡƒΡŽΡ‰Π΅Π³ΠΎ ΠΏΡ€ΠΈ Π²Ρ‹Π·ΠΎΠ²Π΅ ΠΈ ΠΎΠΆΠΈΠ΄Π°ΡŽΡ‰Π΅Π³ΠΎ выполнСния Ξ²? Π•ΡΡ‚ΡŒ Π΄Π²Π° ΠΏΡƒΡ‚ΠΈ:

[x]. ΠŸΠΎΡ‚Ρ€Π΅Π±ΠΎΠ²Π°Ρ‚ΡŒ большС, Ρ‡Π΅ΠΌ прСдписано прСдусловиСм . Ѐормулируя Π±ΠΎΠ»Π΅Π΅ сильноС прСдусловиС, ΠΌΡ‹ позволяСм сСбС ΠΈΡΠΊΠ»ΡŽΡ‡ΠΈΡ‚ΡŒ случаи, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅, согласно исходной спСцификации, Π±Ρ‹Π»ΠΈ ΡΠΎΠ²Π΅Ρ€ΡˆΠ΅Π½Π½ΠΎ ΠΏΡ€ΠΈΠ΅ΠΌΠ»Π΅ΠΌΡ‹.

[x]. Π“Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ мСньшС, Ρ‡Π΅ΠΌ это слСдуСт ΠΈΠ· Π½Π°Ρ‡Π°Π»ΡŒΠ½ΠΎΠ³ΠΎ постусловия Ξ². Π‘ΠΎΠ»Π΅Π΅ слабоС постусловиС позволяСт Π½Π°ΠΌ Π΄Π°Ρ‚ΡŒ Π² Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚Π°Ρ‚Π΅ мСньшС, Ρ‡Π΅ΠΌ Π±Ρ‹Π»ΠΎ ΠΎΠ±Π΅Ρ‰Π°Π½ΠΎ исходной спСцификациСй.

ВспомнитС, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Π½Π΅ΠΎΠ΄Π½ΠΎΠΊΡ€Π°Ρ‚Π½ΠΎ Π³ΠΎΠ²ΠΎΡ€ΠΈΠ»ΠΈ ΠΏΡ€ΠΈ обсуТдСнии ΠŸΡ€ΠΎΠ΅ΠΊΡ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΡ ΠΏΠΎ ΠšΠΎΠ½Ρ‚Ρ€Π°ΠΊΡ‚Ρƒ: усилСниС прСдусловия ΠΎΠ±Π»Π΅Π³Ρ‡Π°Π΅Ρ‚ Π·Π°Π΄Π°Ρ‡Ρƒ поставщика ("ΠΊΠ»ΠΈΠ΅Π½Ρ‚ Ρ‡Π°Ρ‰Π΅ Π½Π΅ ΠΏΡ€Π°Π²"), ΠΈΠ»Π»ΡŽΡΡ‚Ρ€Π°Ρ†ΠΈΠ΅ΠΉ Ρ‡Π΅Π³ΠΎ слуТит ΠΊΡ€Π°ΠΉΠ½ΠΈΠΉ случай - прСдусловиС false (ΠΊΠΎΠ³Π΄Π° "ΠΊΠ»ΠΈΠ΅Π½Ρ‚ всСгда Π½Π΅ ΠΏΡ€Π°Π²").

Как ΡƒΠΆΠ΅ Π±Ρ‹Π»ΠΎ сказано, ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΠ΅ A называСтся Π±ΠΎΠ»Π΅Π΅ ΡΠΈΠ»ΡŒΠ½Ρ‹ΠΌ, Ρ‡Π΅ΠΌ B, Ссли A логичСски Π²Π»Π΅Ρ‡Π΅Ρ‚ B, Π½ΠΎ отличаСтся ΠΎΡ‚ Π½Π΅Π³ΠΎ: Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, x >= 5 сильнСС, Ρ‡Π΅ΠΌ x >= 0. Если ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΠ΅ A сильнСС утвСрТдСния B, говорят Π΅Ρ‰Π΅, Ρ‡Ρ‚ΠΎ ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΠ΅ B слабСС утвСрТдСния A.

Как Π±Ρ‹Ρ‚ΡŒ чСстным

Π’Π΅ΠΏΠ΅Ρ€ΡŒ Π½Π°ΠΌ понятно, ΠΊΠ°ΠΊ ΠΎΠ±ΠΌΠ°Π½Ρ‹Π²Π°Ρ‚ΡŒ. Но ΠΊΠ°ΠΊ ΠΆΠ΅ Π±Ρ‹Ρ‚ΡŒ чСстным? Объявляя ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎ, ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΎΡ…Ρ€Π°Π½ΠΈΡ‚ΡŒ Π΅Π΅ исходныС утвСрТдСния, Π½ΠΎ Ρ‚Π°ΠΊΠΆΠ΅ ΠΌΡ‹ Π²ΠΏΡ€Π°Π²Π΅:

[x]. Π·Π°ΠΌΠ΅Π½ΠΈΡ‚ΡŒ прСдусловиС Π±ΠΎΠ»Π΅Π΅ слабым;

[x]. Π·Π°ΠΌΠ΅Π½ΠΈΡ‚ΡŒ постусловиС Π±ΠΎΠ»Π΅Π΅ ΡΠΈΠ»ΡŒΠ½Ρ‹ΠΌ.

ΠŸΠ΅Ρ€Π²Ρ‹ΠΉ ΠΏΠΎΠ΄Ρ…ΠΎΠ΄ символизируСт Ρ‰Π΅Π΄Ρ€ΠΎΡΡ‚ΡŒ ΠΈ Π²Π΅Π»ΠΈΠΊΠΎΠ΄ΡƒΡˆΠΈΠ΅: ΠΌΡ‹ допускаСм большСС число случаСв, Ρ‡Π΅ΠΌ ΠΈΠ·Π½Π°Ρ‡Π°Π»ΡŒΠ½ΠΎ. Π­Ρ‚ΠΎ Π½Π΅ ΠΏΡ€ΠΈΡ‡ΠΈΠ½ΠΈΡ‚ Π²Ρ€Π΅Π΄ ΠΊΠ»ΠΈΠ΅Π½Ρ‚Ρƒ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Π½Π° ΠΌΠΎΠΌΠ΅Π½Ρ‚ Π²Ρ‹Π·ΠΎΠ²Π° удовлСтворяСт исходному ΠΏΡ€Π΅Π΄ΡƒΡΠ»ΠΎΠ²ΠΈΡŽ. Π’Ρ‚ΠΎΡ€ΠΎΠΉ ΠΏΠΎΠ΄Ρ…ΠΎΠ΄ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Π²Ρ‹Π΄Π°Π΅ΠΌ большС, Ρ‡Π΅ΠΌ ΠΎΡ‚ нас Ρ‚Ρ€Π΅Π±ΠΎΠ²Π°Π»ΠΎΡΡŒ. Π­Ρ‚ΠΎ Π½Π΅ ΠΏΡ€ΠΈΡ‡ΠΈΠ½ΠΈΡ‚ Π²Ρ€Π΅Π΄ ΠΊΠ»ΠΈΠ΅Π½Ρ‚Ρƒ, ΠΏΠΎΠ»Π°Π³Π°ΡŽΡ‰Π΅ΠΌΡƒΡΡ Π½Π° Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ ΠΏΠΎ Π·Π°Π²Π΅Ρ€ΡˆΠ΅Π½ΠΈΠΈ Π²Ρ‹Π·ΠΎΠ²Π° исходных постусловий.

Π˜Ρ‚Π°ΠΊ, основноС ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ:

ΠŸΡ€Π°Π²ΠΈΠ»ΠΎ (1) УтвСрТдСния ΠŸΠ΅Ρ€Π΅ΠΎΠ±ΡŠΡΠ²Π»Π΅Π½ΠΈΡ (Assertion Redeclaration)

ΠŸΡ€ΠΈ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠΌ объявлСнии ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ прСдусловиС ΠΌΠΎΠΆΠ΅Ρ‚ Π·Π°ΠΌΠ΅Π½ΡΡ‚ΡŒΡΡ лишь Ρ€Π°Π²Π½Ρ‹ΠΌ Π΅ΠΌΡƒ ΠΈΠ»ΠΈ Π±ΠΎΠ»Π΅Π΅ слабым, постусловиС - лишь Ρ€Π°Π²Π½Ρ‹ΠΌ Π΅ΠΌΡƒ ΠΈΠ»ΠΈ Π±ΠΎΠ»Π΅Π΅ ΡΠΈΠ»ΡŒΠ½Ρ‹ΠΌ.

Π­Ρ‚ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ ΠΎΡ‚Ρ€Π°ΠΆΠ°Π΅Ρ‚ Ρ‚ΠΎΡ‚ Ρ„Π°ΠΊΡ‚, Ρ‡Ρ‚ΠΎ Π½ΠΎΠ²Ρ‹ΠΉ Π²Π°Ρ€ΠΈΠ°Π½Ρ‚ ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ Π½Π΅ Π΄ΠΎΠ»ΠΆΠ΅Π½ ΠΎΡ‚Π²Π΅Ρ€Π³Π°Ρ‚ΡŒ Π²Ρ‹Π·ΠΎΠ²Ρ‹, допустимыС Π² ΠΎΡ€ΠΈΠ³ΠΈΠ½Π°Π»Π΅, ΠΈ Π΄ΠΎΠ»ΠΆΠ΅Π½, ΠΊΠ°ΠΊ ΠΌΠΈΠ½ΠΈΠΌΡƒΠΌ, ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΠΈ, эквивалСнтныС гарантиям исходного Π²Π°Ρ€ΠΈΠ°Π½Ρ‚Π°. Он Π²ΠΏΡ€Π°Π²Π΅, Ρ…ΠΎΡ‚ΡŒ ΠΈ Π½Π΅ обязан, Π΄ΠΎΠΏΡƒΡΠΊΠ°Ρ‚ΡŒ большСС число Π²Ρ‹Π·ΠΎΠ²ΠΎΠ² ΠΈΠ»ΠΈ Π΄Π°Π²Π°Ρ‚ΡŒ Π±ΠΎΠ»Π΅Π΅ ΡΠΈΠ»ΡŒΠ½Ρ‹Π΅ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΠΈ.

Как явствуСт ΠΈΠ· названия, это ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ ΠΏΡ€ΠΈΠΌΠ΅Π½ΠΈΠΌΠΎ ΠΊ ΠΎΠ±Π΅ΠΈΠΌ Ρ„ΠΎΡ€ΠΌΠ°ΠΌ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠ³ΠΎ объявлСния: ΠΏΠ΅Ρ€Π΅ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΡŽ ΠΈ Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ ΠΎΡ‚Π»ΠΎΠΆΠ΅Π½Π½ΠΎΠ³ΠΎ ΠΊΠΎΠΌΠΏΠΎΠ½Π΅Π½Ρ‚Π°. Π’Ρ‚ΠΎΡ€ΠΎΠΉ случай Π²Π°ΠΆΠ΅Π½ особо, - утвСрТдСния Π±ΡƒΠ΄ΡƒΡ‚ связаны со всСми эффСктивными вСрсиями ΠΏΠΎΡ‚ΠΎΠΌΠΊΠΎΠ².

УтвСрТдСния ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, ΠΊΠ°ΠΊ ΠΎΡ‚Π»ΠΎΠΆΠ΅Π½Π½ΠΎΠΉ, Ρ‚Π°ΠΊ ΠΈ эффСктивной, Π·Π°Π΄Π°ΡŽΡ‚ Π΅Π΅ сСмантику, ΠΏΡ€ΠΈΠΌΠ΅Π½ΠΈΠΌΡƒΡŽ ΠΊ Π½Π΅ΠΉ самой ΠΈ ΠΊΠΎ всСм ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½Ρ‹ΠΌ объявлСниям Π΅Π΅ ΠΏΠΎΡ‚ΠΎΠΌΠΊΠΎΠ². Π’ΠΎΡ‡Π½Π΅Π΅ говоря, ΠΎΠ½ΠΈ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΡ†ΠΈΡ€ΡƒΡŽΡ‚ ΠΎΠ±Π»Π°ΡΡ‚ΡŒ допустимого повСдСния ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ ΠΈ Π΅Π΅ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Ρ… вСрсий. Π›ΡŽΠ±ΠΎΠ΅ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎΠ΅ объявлСниС ΠΌΠΎΠΆΠ΅Ρ‚ лишь ΡΡƒΠΆΠ°Ρ‚ΡŒ эту ΠΎΠ±Π»Π°ΡΡ‚ΡŒ, Π½Π΅ Π½Π°Ρ€ΡƒΡˆΠ°Ρ Π΅Π΅.

Как слСдствиС, ΡΠΎΠ·Π΄Π°Ρ‚Π΅Π»ΡŒ класса Π΄ΠΎΠ»ΠΆΠ΅Π½ Π±Ρ‹Ρ‚ΡŒ остороТным ΠΏΡ€ΠΈ написании ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΠΉ эффСктивной ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, Π½Π΅ привнося излишнюю ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ (overspecification). УтвСрТдСния Π΄ΠΎΠ»ΠΆΠ½Ρ‹ ΠΎΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ намСрСния ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, - Π΅Π΅ Π°Π±ΡΡ‚Ρ€Π°ΠΊΡ‚Π½ΡƒΡŽ сСмантику, - Π½ΠΎ Π½Π΅ свойства Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ. Π˜Π½Π°Ρ‡Π΅ ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΊΡ€Ρ‹Ρ‚ΡŒ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ создания ΠΈΠ½ΠΎΠΉ Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ ΠΏΠΎΠ΄ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ Ρƒ Π±ΡƒΠ΄ΡƒΡ‰ΠΈΡ… ΠΏΠΎΡ‚ΠΎΠΌΠΊΠΎΠ².