end
remove is
-- Π£Π΄Π°Π»ΠΈΡΡ ΡΠ»Π΅ΠΌΠ΅Π½Ρ Π²Π΅ΡΡΠΈΠ½Ρ ΡΡΠ΅ΠΊΠ°
require
not_empty: not empty -- i.e. count > 0
ensure
not_full: not full
one_fewer: count = old count - 1
end
invariant
count_non_negative: 0 <= count
count_bounded: count <= capacity
empty_if_no_elements: empty = (count = 0)
end
ΠΡΠ° ΠΊΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ° Π½Π΅ ΡΠ²Π»ΡΠ΅ΡΡΡ ΡΠΈΠ½ΡΠ°ΠΊΡΠΈΡΠ΅ΡΠΊΠΈ ΠΏΡΠ°Π²ΠΈΠ»ΡΠ½ΡΠΌ ΡΠ΅ΠΊΡΡΠΎΠΌ ΠΊΠ»Π°ΡΡΠ°, ΠΏΠΎΡΠ΅ΠΌΡ Π·Π΄Π΅ΡΡ ΠΈΡΠΏΠΎΠ»ΡΠ·ΡΠ΅ΡΡΡ ΡΠ΅ΡΠΌΠΈΠ½ class interface Π²ΠΌΠ΅ΡΡΠΎ ΠΎΠ±ΡΡΠ½ΠΎΠ³ΠΎ ΡΠ΅ΡΠΌΠΈΠ½Π° class. Π₯ΠΎΡΡ Π΄ΠΎΡΡΠ°ΡΠΎΡΠ½ΠΎ ΠΏΡΠΎΡΡΠΎ ΠΏΡΠ΅Π²ΡΠ°ΡΠΈΡΡ ΡΡΡ ΡΠΎΡΠΌΡ Π² ΠΏΡΠ°Π²ΠΈΠ»ΡΠ½ΡΠΉ ΠΎΡΠ»ΠΎΠΆΠ΅Π½Π½ΡΠΉ ΠΊΠ»Π°ΡΡ, ΠΈΠ·Π²Π΅ΡΡΠ½ΠΎΠ΅ ΠΏΠΎΠ½ΡΡΠΈΠ΅, ΡΠ°ΡΡΠΌΠ°ΡΡΠΈΠ²Π°Π΅ΠΌΠΎΠ΅ Π² Π΄Π΅ΡΠ°Π»ΡΡ ΠΏΡΠΈ ΠΈΠ·ΡΡΠ΅Π½ΠΈΠΈ Π½Π°ΡΠ»Π΅Π΄ΠΎΠ²Π°Π½ΠΈΡ.
Π ΡΡΠ΅Π΄Π΅ ISE ΠΏΠΎΠ»ΡΡΠΈΡΡ ΠΊΡΠ°ΡΠΊΡΡ ΡΠΎΡΠΌΡ ΠΌΠΎΠΆΠ½ΠΎ ΠΎΠ΄Π½ΠΈΠΌ ΡΠ΅Π»ΡΠΊΠΎΠΌ ΡΠΎΠΎΡΠ²Π΅ΡΡΡΠ²ΡΡΡΠ΅ΠΉ ΠΊΠ½ΠΎΠΏΠΊΠΈ Π² Class Tool; ΠΌΠΎΠΆΠ½ΠΎ Π³Π΅Π½Π΅ΡΠΈΡΠΎΠ²Π°ΡΡ Π»ΠΈΠ±ΠΎ ΠΏΠ»ΠΎΡΠΊΠΈΠΉ ΡΠ΅ΠΊΡΡ, Π»ΠΈΠ±ΠΎ ΡΠ΅ΠΊΡΡ Π² ΡΠΎΡΠΌΠ°ΡΠ°Ρ HTML, RTF, MML (FrameMaker), TEX ΠΈ Π΄ΡΡΠ³ΠΈΡ . ΠΠΎΠΆΠ½ΠΎ ΠΎΠΏΡΠ΅Π΄Π΅Π»ΠΈΡΡ ΠΈ ΡΠ²ΠΎΠΉ ΡΠΎΠ±ΡΡΠ²Π΅Π½Π½ΡΠΉ ΡΠΎΡΠΌΠ°Ρ.ΠΡΠ»ΠΈ ΡΡΠ°Π²Π½ΠΈΡΡ ΠΊΡΠ°ΡΠΊΡΡ ΡΠΎΡΠΌΡ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ Ρ ΠΈΡ ΠΎΡΠΈΠ³ΠΈΠ½Π°Π»Π°ΠΌΠΈ Π² ΠΊΠ»Π°ΡΡΠ΅, ΡΠΎ ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΌΠ΅ΡΠΈΡΡ, ΡΡΠΎ ΠΈΡΡΠ΅Π·Π»ΠΈ Π²ΡΠ΅ ΠΏΡΠ΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΡ, Π²ΠΊΠ»ΡΡΠ°ΡΡΠΈΠ΅ representation, ΡΠ°ΠΊ ΠΊΠ°ΠΊ ΡΡΠΎΡ Π°ΡΡΠΈΠ±ΡΡ Π½Π΅ ΡΠΊΡΠΏΠΎΡΡΠΈΡΡΠ΅ΡΡΡ.
ΠΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ° Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ ΠΎΡΠΎΠ±Π΅Π½Π½ΠΎ ΠΈΠ½ΡΠ΅ΡΠ΅ΡΠ½Π° ΠΏΠΎ ΡΠ»Π΅Π΄ΡΡΡΠΈΠΌ ΠΏΡΠΈΡΠΈΠ½Π°ΠΌ:
[x]. ΠΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΡ ΡΠ²Π»ΡΠ΅ΡΡΡ Π±ΠΎΠ»Π΅Π΅ Π²ΡΡΠΎΠΊΠΎΠΉ ΡΠΎΡΠΌΠΎΠΉ Π°Π±ΡΡΡΠ°ΠΊΡΠΈΠΈ, ΡΠ΅ΠΌ ΠΎΠ±ΡΠ΅ΠΊΡ, ΠΊΠΎΡΠΎΡΡΠΉ ΠΎΠ½Π° ΠΎΠΏΠΈΡΡΠ²Π°Π΅Ρ. ΠΡΠΎ ΠΎΡΠ½ΠΎΠ²Π½ΠΎΠ΅ ΡΡΠ΅Π±ΠΎΠ²Π°Π½ΠΈΠ΅, ΠΏΡΠ΅Π΄ΡΡΠ²Π»ΡΠ΅ΠΌΠΎΠ΅ ΠΊ ΠΊΠ°ΡΠ΅ΡΡΠ²Π΅Π½Π½ΠΎΠΉ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ. Π€Π°ΠΊΡΠΈΡΠ΅ΡΠΊΠ°Ρ ΡΠ΅Π°Π»ΠΈΠ·Π°ΡΠΈΡ, ΠΎΠΏΠΈΡΡΠ²Π°ΡΡΠ°Ρ "ΠΊΠ°ΠΊ", ΡΠ΄Π°Π»ΡΠ΅ΡΡΡ. Π£ΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡ, ΠΎΠ±ΡΡΡΠ½ΡΡΡΠΈΠ΅ "ΡΡΠΎ", Π° Π² Π½Π΅ΠΊΠΎΡΠΎΡΡΡ ΡΠ»ΡΡΠ°ΡΡ ΠΈ "ΠΏΠΎΡΠ΅ΠΌΡ", ΠΎΡΡΠ°ΡΡΡΡ. Π‘ΠΎΡ ΡΠ°Π½ΡΡΡΡΡ Π·Π°Π³ΠΎΠ»ΠΎΠ²ΠΎΡΠ½ΡΠ΅ ΠΊΠΎΠΌΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ ΠΊ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠ°ΠΌ ΠΈ ΠΎΠΏΠΈΡΠ°Π½ΠΈΡ, Π²ΠΊΠ»ΡΡΠ°Π΅ΠΌΡΠ΅ Π² ΠΏΡΠ΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΠ΅ indexing, Π΄ΠΎΠΏΠΎΠ»Π½ΡΡΡΠΈΠ΅ Π² ΠΌΠ΅Π½Π΅Π΅ ΡΠΎΡΠΌΠ°Π»ΡΠ½ΠΎΠΉ ΡΠΎΡΠΌΠ΅ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡ, ΠΏΠΎΡΡΠ½ΡΡ ΡΠ΅Π»Ρ ΠΈ Π½Π°Π·Π½Π°ΡΠ΅Π½ΠΈΠ΅ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΡ.
[x]. Π―Π²Π»ΡΡΡΡ ΠΏΡΡΠΌΡΠΌ ΡΠ»Π΅Π΄ΡΡΠ²ΠΈΠ΅ΠΌ ΠΏΡΠΈΠ½ΡΠΈΠΏΠ° Π‘Π°ΠΌΠΎΠ΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠΈΡΠΎΠ²Π°Π½ΠΈΡ, ΠΈΠ·ΡΡΠ°Π΅ΠΌΠΎΠ³ΠΎ Π² Π½Π°ΡΠ΅ΠΌ ΠΎΠ±Π·ΠΎΡΠ΅ ΠΊΠΎΠ½ΡΠ΅ΠΏΡΠΈΠΉ ΠΌΠΎΠ΄ΡΠ»ΡΠ½ΠΎΡΡΠΈ, ΠΊΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ° ΡΠ°ΡΡΠΌΠ°ΡΡΠΈΠ²Π°Π΅Ρ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΡ ΠΊΠ°ΠΊ ΠΈΠ½ΡΠΎΡΠΌΠ°ΡΠΈΡ, ΡΠΎΠ΄Π΅ΡΠΆΠ°ΡΡΡΡΡ Π² ΡΠ°ΠΌΠΎΠΌ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠ½ΠΎΠΌ ΠΏΡΠΎΠ΄ΡΠΊΡΠ΅. ΠΡΠΎ ΠΎΠ·Π½Π°ΡΠ°Π΅Ρ, ΡΡΠΎ Π΅ΡΡΡ ΡΠΎΠ»ΡΠΊΠΎ ΠΎΠ΄ΠΈΠ½ ΡΠΎΠΏΡΠΎΠ²ΠΎΠΆΠ΄Π°Π΅ΠΌΡΠΉ ΠΏΡΠΎΠ΄ΡΠΊΡ, - Π²Π°ΠΆΠ½ΠΎΠ΅ ΡΡΠ΅Π±ΠΎΠ²Π°Π½ΠΈΠ΅, ΠΏΡΠΎΡ ΠΎΠ΄ΡΡΠ΅Π΅ ΡΠ΅ΡΠ΅Π· Π²ΡΡ ΠΊΠ½ΠΈΠ³Ρ. ΠΠ°ΠΊ ΡΠ΅Π·ΡΠ»ΡΡΠ°Ρ, ΠΏΠΎΡΠ²Π»ΡΠ΅ΡΡΡ Π±ΠΎΠ»ΡΡΠ΅ ΡΠ°Π½ΡΠΎΠ² ΠΊΠΎΡΡΠ΅ΠΊΡΠ½ΠΎΡΡΠΈ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ. Π‘ΠΎΡ ΡΠ°Π½ΡΡ Π²ΡΠ΅ Π² ΠΎΠ΄Π½ΠΎΠΌ ΠΌΠ΅ΡΡΠ΅, Π²Ρ ΡΠΌΠ΅Π½ΡΡΠ°Π΅ΡΠ΅ ΡΠΈΡΠΊ Π½Π΅ΡΠΎΠΎΡΠ²Π΅ΡΡΡΠ²ΠΈΡ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ ΠΎΠ±Π½ΠΎΠ²Π»Π΅Π½Π½ΠΎΠΌΡ ΠΏΡΠΎΠ΄ΡΠΊΡΡ.
[x]. ΠΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ° ΠΌΠΎΠΆΠ΅Ρ Π±ΡΡΡ ΠΈΠ·Π²Π»Π΅ΡΠ΅Π½Π° ΠΈΠ· ΠΊΠ»Π°ΡΡΠ° Π°Π²ΡΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΈ. Π’Π°ΠΊ ΡΡΠΎ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠ°ΡΠΈΡ Π½Π΅ Π΅ΡΡΡ Π½Π΅ΡΡΠΎ, ΡΡΠ΅Π±ΡΡΡΠ΅Π΅ ΡΠΏΠ΅ΡΠΈΠ°Π»ΡΠ½ΠΎΠ³ΠΎ Π½Π°ΠΏΠΈΡΠ°Π½ΠΈΡ. ΠΠΌΠ΅ΡΡΠΎ ΡΡΠΎΠ³ΠΎ, ΠΊΠΎΠ³Π΄Π° ΠΎΠ½Π° Π½Π΅ΠΎΠ±Ρ ΠΎΠ΄ΠΈΠΌΠ°, Π²Ρ ΠΏΡΠΎΡΡΠΎ "ΠΏΡΠΎΡΠΈΡΠ΅ ΠΊΠΎΠΌΠΏΡΡΡΠ΅Ρ" ΠΏΡΠΎΠΈΠ·Π²Π΅ΡΡΠΈ ΡΡΠΎ Π½Π΅ΡΡΠΎ, ΡΠ΅Π»ΠΊΠ½ΡΠ² ΠΊΠ½ΠΎΠΏΠΊΠΎΠΉ ΠΌΡΡΠΈ.
ΠΠ½ΡΠ΅ΡΠ΅ΡΠ½ΠΎ ΡΡΠ°Π²Π½ΠΈΡΡ ΡΡΠΎΡ ΠΏΠΎΠ΄Ρ ΠΎΠ΄ Ρ ΠΏΠΎΠ½ΡΡΠΈΠ΅ΠΌ ΠΈΠ½ΡΠ΅ΡΡΠ΅ΠΉΡΠ° ΠΏΠ°ΠΊΠ΅ΡΠ° Π² ΡΠ·ΡΠΊΠ΅ Ada, Π³Π΄Π΅ ΠΌΠΎΠ΄ΡΠ»Ρ (ΠΏΠ°ΠΊΠ΅Ρ) ΡΠΎΡΡΠΎΠΈΡ ΠΈΠ· Π΄Π²ΡΡ ΡΠ°ΡΡΠ΅ΠΉ - ΠΈΠ½ΡΠ΅ΡΡΠ΅ΠΉΡΠ° ΠΈ ΡΠ΅Π°Π»ΠΈΠ·Π°ΡΠΈΠΈ. Java ΠΈΡΠΏΠΎΠ»ΡΠ·ΡΠ΅Ρ ΠΏΠΎΠ΄ΠΎΠ±Π½ΡΠΉ ΠΌΠ΅Ρ Π°Π½ΠΈΠ·ΠΌ. ΠΠ½ΡΠ΅ΡΡΠ΅ΠΉΡ ΠΏΠ°ΠΊΠ΅ΡΠ° ΠΈΠΌΠ΅Π΅Ρ Π½Π΅ΠΊΠΎΡΠΎΡΠΎΠ΅ ΡΡ ΠΎΠ΄ΡΡΠ²ΠΎ Ρ ΠΊΡΠ°ΡΠΊΠΎΠΉ ΡΠΎΡΠΌΠΎΠΉ, Π½ΠΎ ΠΈΠΌΠ΅Π΅Ρ ΠΈ ΡΡΡΠ΅ΡΡΠ²Π΅Π½Π½ΡΠ΅ ΡΠ°Π·Π»ΠΈΡΠΈΡ:
[x]. ΠΠ΄Π΅ΡΡ Π½Π΅Ρ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ, ΡΠ°ΠΊ ΡΡΠΎ Π²ΡΡ ΡΠΏΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΡΠ²ΠΎΠ΄ΠΈΡΡΡ ΠΊ ΠΎΠ±ΡΡΠ²Π»Π΅Π½ΠΈΡ ΡΠΈΠΏΠΎΠ² ΠΈ ΠΊΠΎΠΌΠΌΠ΅Π½ΡΠ°ΡΠΈΡΠΌ.
[x]. ΠΠ½ΡΠ΅ΡΡΠ΅ΠΉΡ Π½Π΅ ΡΠΎΠ·Π΄Π°Π΅ΡΡΡ Π°Π²ΡΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΈ, Π° ΠΏΠΈΡΠ΅ΡΡΡ Π½Π΅Π·Π°Π²ΠΈΡΠΈΠΌΠΎ ΠΎΡ ΡΠ΅Π°Π»ΠΈΠ·Π°ΡΠΈΠΈ. ΠΠΎΡΡΠΎΠΌΡ ΡΠ°Π·ΡΠ°Π±ΠΎΡΡΠΈΠΊ Π΄Π²Π°ΠΆΠ΄Ρ Π΄ΠΎΠ»ΠΆΠ΅Π½ Π·Π°Π΄Π°Π²Π°ΡΡ ΠΌΠ½ΠΎΠ³ΠΈΠ΅ Π²Π΅ΡΠΈ: Π·Π°Π³ΠΎΠ»ΠΎΠ²ΠΊΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ, ΠΈΡ ΡΠΈΠ³Π½Π°ΡΡΡΡ, ΠΊΠΎΠΌΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ ΠΊ Π·Π°Π³ΠΎΠ»ΠΎΠ²ΠΊΠ°ΠΌ, ΠΎΠ±ΡΡΠ²Π»Π΅Π½ΠΈΡ ΠΎΡΠΊΡΡΡΡΡ ΠΏΠ΅ΡΠ΅ΠΌΠ΅Π½Π½ΡΡ . ΠΡΠ° Π½Π°Π²ΡΠ·Π°Π½Π½Π°Ρ ΠΈΠ·Π±ΡΡΠΎΡΠ½ΠΎΡΡΡ ΡΡΠΎΠΌΠΈΡΠ΅Π»ΡΠ½Π° (Π²Π΄Π²ΠΎΠΉΠ½Π΅ ΠΏΡΠΈ Π²ΠΊΠ»ΡΡΠ΅Π½ΠΈΠΈ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ) ΠΈ, ΠΊΠ°ΠΊ ΠΎΠ±ΡΡΠ½ΠΎ, ΠΏΠΎΠ²ΡΡΠ°Π΅Ρ ΡΠΈΡΠΊ Π½Π΅ΡΠΎΠΎΡΠ²Π΅ΡΡΡΠ²ΠΈΡ; Π²ΡΠ΅Π³Π΄Π° Π΅ΡΡΡ ΡΠ°Π½Ρ, ΠΎΠ±Π½ΠΎΠ²ΠΈΡΡ ΠΎΠ΄Π½Ρ ΡΠ°ΡΡΡ ΠΈ Π·Π°Π±ΡΡΡ ΠΏΡΠΎ Π΄ΡΡΠ³ΡΡ.
ΠΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ°, Π΄ΠΎΠΏΠΎΠ»Π½Π΅Π½Π½Π°Ρ Π΅Π΅ Π²Π°ΡΠΈΠ°Π½ΡΠΎΠΌ - ΠΏΠ»ΠΎΡΠΊΠΎ-ΠΊΡΠ°ΡΠΊΠΎΠΉ ΡΠΎΡΠΌΠΎΠΉ (flat-short form), ΠΈΠ·ΡΡΠ°Π΅ΠΌΠΎΠΉ ΠΏΡΠΈ ΡΠ°ΡΡΠΌΠΎΡΡΠ΅Π½ΠΈΠΈ Π½Π°ΡΠ»Π΅Π΄ΠΎΠ²Π°Π½ΠΈΡ, ΡΠ²Π»ΡΠ΅ΡΡΡ ΠΏΡΠΈΠ½ΡΠΈΠΏΠΈΠ°Π»ΡΠ½ΡΠΌ Π²ΠΊΠ»Π°Π΄ΠΎΠΌ Π² ΠΠ-ΠΌΠ΅ΡΠΎΠ΄. Π ΠΏΠΎΠ²ΡΠ΅Π΄Π½Π΅Π²Π½ΠΎΠΉ ΠΏΡΠ°ΠΊΡΠΈΠΊΠ΅ ΠΠ-ΡΠ°Π·ΡΠ°Π±ΠΎΡΠΊΠΈ ΠΎΠ½Π° ΠΏΠΎΡΠ²Π»ΡΠ΅ΡΡΡ Π½Π΅ ΡΠΎΠ»ΡΠΊΠΎ ΠΊΠ°ΠΊ ΡΡΠ΅Π΄ΡΡΠ²ΠΎ Π΄ΠΎΠΊΡΠΌΠ΅Π½ΡΠΈΡΠΎΠ²Π°Π½ΠΈΡ, Π½ΠΎ ΠΈ ΠΊΠ°ΠΊ ΡΡΠ°Π½Π΄Π°ΡΡΠ½ΡΠΉ ΡΠΎΡΠΌΠ°Ρ, Π² ΠΊΠΎΡΠΎΡΠΎΠΌ ΡΠ°Π·ΡΠ°Π±ΠΎΡΡΠΈΠΊΠΈ ΠΈ ΠΌΠ΅Π½Π΅Π΄ΠΆΠ΅ΡΡ ΠΈΠ·ΡΡΠ°ΡΡ ΡΡΡΠ΅ΡΡΠ²ΡΡΡΠΈΠ΅ ΠΏΡΠΎΠ΅ΠΊΡΡ, ΡΠ°Π·ΡΠ°Π±Π°ΡΡΠ²Π°ΡΡ Π½ΠΎΠ²ΡΠ΅ ΠΈ ΠΎΠ±ΡΡΠΆΠ΄Π°ΡΡ ΠΏΡΠ΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΡ ΠΏΠΎ ΠΈΠ·ΠΌΠ΅Π½Π΅Π½ΠΈΡ ΠΏΡΠΎΠ΅ΠΊΡΠΎΠ².
ΠΡΠ°ΡΠΊΠ°Ρ ΡΠΎΡΠΌΠ° ΠΈΠ³ΡΠ°Π΅Ρ ΡΠ΅Π½ΡΡΠ°Π»ΡΠ½ΡΡ ΡΠΎΠ»Ρ Π² ΠΠ-ΡΠ°Π·ΡΠ°Π±ΠΎΡΠΊΠ΅, ΠΏΠΎΡΠΊΠΎΠ»ΡΠΊΡ ΠΎΠ½Π° ΡΠ΄ΠΎΠ²Π»Π΅ΡΠ²ΠΎΡΡΠ΅Ρ ΡΠ΅Π»ΠΈ, ΠΎΠΏΡΠ΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠΉ ΠΏΡΠΈ Π°Π½Π°Π»ΠΈΠ·Π΅ ΡΡΠ΅Π±ΠΎΠ²Π°Π½ΠΈΠΉ, ΠΎΠ±Π΅ΡΠΏΠ΅ΡΠΈΠ²Π°ΡΡΠΈΡ ΠΏΠΎΠ²ΡΠΎΡΠ½ΠΎΠ΅ ΠΈΡΠΏΠΎΠ»ΡΠ·ΠΎΠ²Π°Π½ΠΈΠ΅. Π‘ΡΡΡ ΡΡΠ΅Π±ΠΎΠ²Π°Π½ΠΈΡ: ΠΎΡΠ½ΠΎΠ²ΠΎΠΉ ΠΏΠΎΠ²ΡΠΎΡΠ½ΠΎΠ³ΠΎ ΠΈΡΠΏΠΎΠ»ΡΠ·ΠΎΠ²Π°Π½ΠΈΡ ΡΠ²Π»ΡΡΡΡΡ Π°Π±ΡΡΡΠ°ΠΊΡΠ½ΡΠ΅ ΠΌΠΎΠ΄ΡΠ»ΠΈ. ΠΠ»Π°ΡΡ Π² Π΅Π³ΠΎ ΠΊΡΠ°ΡΠΊΠΎΠΉ ΠΈΠ»ΠΈ ΠΏΠ»ΠΎΡΠΊΠΎ-ΠΊΡΠ°ΡΠΊΠΎΠΉ ΡΠΎΡΠΌΠ΅ ΡΠ²Π»ΡΠ΅ΡΡΡ ΡΠ΅ΠΌ ΡΠ°ΠΌΡΠΌ ΡΠ°Π·ΡΡΠΊΠΈΠ²Π°Π΅ΠΌΡΠΌ Π°Π±ΡΡΡΠ°ΠΊΡΠ½ΡΠΌ ΠΌΠΎΠ΄ΡΠ»Π΅ΠΌ.
ΠΠΎΠ½ΠΈΡΠΎΡΠΈΠ½Π³ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ Π² ΠΏΠ΅ΡΠΈΠΎΠ΄ Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΡ
ΠΡΠΈΡΠ»ΠΎ Π²ΡΠ΅ΠΌΡ, Π΄Π°ΡΡ ΠΏΠΎΠ»Π½ΡΠΉ ΠΎΡΠ²Π΅Ρ Π½Π° Π²ΠΎΠΏΡΠΎΡ: "ΠΊΠ°ΠΊΠΎΠΉ ΡΡΡΠ΅ΠΊΡ ΠΏΡΠΎΠΈΠ·Π²ΠΎΠ΄ΡΡ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡ Π² ΠΏΠ΅ΡΠΈΠΎΠ΄ Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΡ?". ΠΠ°ΠΊ ΠΎΡΠΌΠ΅ΡΠ°Π»ΠΎΡΡ, ΠΎΡΠ²Π΅Ρ ΠΎΠΏΡΠ΅Π΄Π΅Π»ΡΠ΅ΡΡΡ ΡΠ°Π·ΡΠ°Π±ΠΎΡΡΠΈΠΊΠΎΠΌ, ΠΈΠΌΠ΅ΡΡΠΈΠΌ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡΡ ΡΠΏΡΠ°Π²Π»ΡΡΡ ΠΏΠ°ΡΠ°ΠΌΠ΅ΡΡΠ°ΠΌΠΈ ΠΊΠΎΠΌΠΏΠΈΠ»ΡΡΠΈΠΈ. ΠΡΠ±ΠΎΡ Π½ΡΠΆΠ½ΡΡ ΠΏΠ°ΡΠ°ΠΌΠ΅ΡΡΠΎΠ² Π½Π΅ ΡΡΠ΅Π±ΡΠ΅Ρ ΠΈΠ·ΠΌΠ΅Π½Π΅Π½ΠΈΡ ΡΠ΅ΠΊΡΡΠ° ΠΊΠ»Π°ΡΡΠ°, Π²ΠΌΠ΅ΡΡΠΎ ΡΡΠΎΠ³ΠΎ ΠΌΠ΅Π½ΡΠ΅ΡΡΡ ΡΠΎΠ΄Π΅ΡΠΆΠΈΠΌΠΎΠ΅ Ace ΡΠ°ΠΉΠ»Π°. ΠΠ°ΠΏΠΎΠΌΠ½Ρ, Ace ΡΠ°ΠΉΠ» Π½Π°ΠΏΠΈΡΠ°Π½ Π½Π° ΡΠ·ΡΠΊΠ΅ Lace, ΠΎΠΏΠΈΡΡΠ²Π°ΡΡΠ΅ΠΌ ΠΊΠΎΠΌΠΏΠΈΠ»ΡΡΠΈΡ ΠΈ ΡΠ±ΠΎΡΠΊΡ ΡΠΈΡΡΠ΅ΠΌΡ.
ΠΠ°ΠΏΠΎΠΌΠ½Ρ ΡΠ°ΠΊΠΆΠ΅, ΡΡΠΎ Lace ΠΎΠ΄ΠΈΠ½ ΠΈΠ· Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΡΡ ΡΠ·ΡΠΊΠΎΠ², ΠΏΠΎΠ·Π²ΠΎΠ»ΡΡΡΠΈΡ ΡΠΏΡΠ°Π²Π»ΡΡΡ ΡΠ±ΠΎΡΠΊΠΎΠΉ ΡΠΈΡΡΠ΅ΠΌΡ; ΠΎΠ½ Π½Π΅ ΡΠ²Π»ΡΠ΅ΡΡΡ Π½Π΅ΠΈΠ·ΠΌΠ΅Π½ΡΠ΅ΠΌΡΠΌ ΠΊΠΎΠΌΠΏΠΎΠ½Π΅Π½ΡΠΎΠΌ ΠΌΠ΅ΡΠΎΠ΄Π°. ΠΠΎ Π²ΡΠ΅Π³Π΄Π° Π½Π΅ΠΎΠ±Ρ ΠΎΠ΄ΠΈΠΌΠΎ ΠΏΠΎΠ΄ΠΎΠ±Π½ΠΎΠ΅ ΡΡΠ΅Π΄ΡΡΠ²ΠΎ Π΄Π»Ρ ΠΏΠ΅ΡΠ΅Ρ ΠΎΠ΄Π° ΠΎΡ ΠΎΡΠ΄Π΅Π»ΡΠ½ΡΡ ΠΊΠΎΠΌΠΏΠΎΠ½Π΅Π½Ρ ΠΊ ΠΏΠΎΠ»Π½ΠΎΠΉ ΠΊΠΎΠΌΠΏΠΈΠ»ΠΈΡΡΠ΅ΠΌΠΎΠΉ ΡΠΈΡΡΠ΅ΠΌΠ΅.ΠΠΎΡ ΠΏΡΠΈΠΌΠ΅Ρ ΠΏΡΠΈΠΌΠ΅Π½Π΅Π½ΠΈΡ Ace ΡΠ°ΠΉΠ»Π°, ΡΡΡΠ°Π½Π°Π²Π»ΠΈΠ²Π°ΡΡΠ΅Π³ΠΎ Π½Π΅ΠΊΠΎΡΠΎΡΡΠ΅ ΠΏΠ°ΡΠ°ΠΌΠ΅ΡΡΡ ΠΌΠΎΠ½ΠΈΡΠΎΡΠΈΠ½Π³Π° ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ:
system painting root
GRAPHICS
default
assertion (require)
cluster
base_library: "\library\base"
graphical_library: "\library\graphics"
option
assertion (all): BUTTON, color_BITMAP
end
painting_application: "\user\application"
option
assertion (no)
end
end -- system painting
ΠΡΠ΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΠ΅ default ΡΠΊΠ°Π·ΡΠ²Π°Π΅Ρ, ΡΡΠΎ Π΄Π»Ρ Π±ΠΎΠ»ΡΡΠΈΠ½ΡΡΠ²Π° ΠΊΠ»Π°ΡΡΠΎΠ² ΡΠΈΡΡΠ΅ΠΌΡ ΠΏΡΠΎΠ²Π΅ΡΡΡΡΡΡ Π±ΡΠ΄ΡΡ ΡΠΎΠ»ΡΠΊΠΎ ΠΏΡΠ΅Π΄ΡΡΠ»ΠΎΠ²ΠΈΡ (require). ΠΠ²Π° ΠΊΠ»Π°ΡΡΠ΅ΡΠ° ΠΏΠ΅ΡΠ΅ΠΎΠΏΡΠ΅Π΄Π΅Π»ΡΡΡ ΡΡΡΠ°Π½ΠΎΠ²ΠΊΠΈ ΡΠΌΠΎΠ»ΡΠ°Π½ΠΈΡ. ΠΠ»Π°ΡΡΠ΅Ρ graphical_library Π±ΡΠ΄Π΅Ρ Π½Π°Π±Π»ΡΠ΄Π°ΡΡ Π·Π° Π²ΡΠ΅ΠΌΠΈ (all) ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡΠΌΠΈ Π² ΠΊΠ»Π°ΡΡΠ°Ρ BUTTON ΠΈ color_BITMAP. ΠΠ»Π°ΡΡΠ΅Ρ painting_application Π²ΠΎΠΎΠ±ΡΠ΅ ΠΎΡΠΌΠ΅Π½ΡΠ΅Ρ Π½Π°Π±Π»ΡΠ΄Π΅Π½ΠΈΠ΅ Π·Π° ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡΠΌΠΈ Π²ΠΎ Π²ΡΠ΅Ρ Π΅Π³ΠΎ ΠΊΠ»Π°ΡΡΠ°Ρ . ΠΡΠΎΡ ΠΏΡΠΈΠΌΠ΅Ρ ΠΈΠ»Π»ΡΡΡΡΠΈΡΡΠ΅Ρ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡΠΈ ΠΌΠΎΠ½ΠΈΡΠΎΡΠΈΠ½Π³Π° Π½Π° ΡΠ°Π·Π½ΡΡ ΡΡΠΎΠ²Π½ΡΡ - Π²ΡΠ΅ΠΉ ΡΠΈΡΡΠ΅ΠΌΡ, ΠΎΡΠ΄Π΅Π»ΡΠ½ΡΡ ΠΊΠ»Π°ΡΡΠ΅ΡΠΎΠ², ΠΎΡΠ΄Π΅Π»ΡΠ½ΡΡ ΠΊΠ»Π°ΡΡΠΎΠ².
Π‘Π»Π΅Π΄ΡΡΡΠΈΠ΅ ΠΊΠ»ΡΡΠ΅Π²ΡΠ΅ ΡΠ»ΠΎΠ²Π°, ΡΠΏΡΠ°Π²Π»ΡΡΡΠΈΠ΅ ΠΏΡΠΎΠ²Π΅ΡΠΊΠΎΠΉ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ, ΠΌΠΎΠ³ΡΡ ΠΏΠΎΡΠ²ΠΈΡΡΡΡ Π² ΠΊΡΡΠ³Π»ΡΡ ΡΠΊΠΎΠ±ΠΊΠ°Ρ assertion(...):
[x]. no - Π½Π΅ Π²ΡΠΏΠΎΠ»Π½ΡΡΡ Π½ΠΈΠΊΠ°ΠΊΠΎΠ΅ ΠΈΠ· ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ. Π ΡΡΠΎΠΌ ΡΠ΅ΠΆΠΈΠΌΠ΅ ΠΎΠΊΠ°Π·ΡΠ²Π°ΡΡ Π½Π° Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ Π½Π΅ Π±ΠΎΠ»ΡΡΠΈΠΉ ΡΡΡΠ΅ΠΊΡ, ΡΠ΅ΠΌ ΠΊΠΎΠΌΠΌΠ΅Π½ΡΠ°ΡΠΈΠΈ;
[x]. require - ΡΠΎΠ»ΡΠΊΠΎ ΠΏΡΠΎΠ²Π΅ΡΠΊΠ° Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΠΈ ΠΏΡΠ΅Π΄ΡΡΠ»ΠΎΠ²ΠΈΠΉ Π½Π° Π²Ρ ΠΎΠ΄Π΅ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ;
[x]. ensure - ΠΏΡΠΎΠ²Π΅ΡΠΊΠ° Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΠΈ ΠΏΠΎΡΡΡΡΠ»ΠΎΠ²ΠΈΠΉ Π½Π° Π²ΡΡ ΠΎΠ΄Π΅ ΠΈΠ· ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΡ;
[x]. invariant - ΠΏΡΠΎΠ²Π΅ΡΠΊΠ° Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΠΈ ΠΈΠ½Π²Π°ΡΠΈΠ°Π½ΡΠΎΠ² ΠΊΠ»Π°ΡΡΠ° Π½Π° Π²Ρ ΠΎΠ΄Π΅ ΠΈ Π²ΡΡ ΠΎΠ΄Π΅ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΡ Π΄Π»Ρ ΠΊΠ²Π°Π»ΠΈΡΠΈΡΠΈΡΠΎΠ²Π°Π½Π½ΡΡ Π²ΡΠ·ΠΎΠ²ΠΎΠ² (obj.f);
[x]. loop - ΠΏΡΠΎΠ²Π΅ΡΠΊΠ° Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΠΈ ΠΈΠ½Π²Π°ΡΠΈΠ°Π½ΡΠΎΠ² ΡΠΈΠΊΠ»Π° ΠΏΠ΅ΡΠ΅Π΄ ΠΈ ΠΏΠΎΡΠ»Π΅ ΠΊΠ°ΠΆΠ΄ΠΎΠΉ ΠΈΡΠ΅ΡΠ°ΡΠΈΠΈ; ΠΏΡΠΎΠ²Π΅ΡΠΊΠ° ΡΠΌΠ΅Π½ΡΡΠ΅Π½ΠΈΡ Π²Π°ΡΠΈΠ°Π½ΡΠΎΠ² Π½Π° ΠΊΠ°ΠΆΠ΄ΠΎΠΉ ΠΈΡΠ΅ΡΠ°ΡΠΈΠΈ Ρ ΡΠΎΡ ΡΠ°Π½Π΅Π½ΠΈΠ΅ΠΌ ΠΈΡ Π½Π΅ ΠΎΡΡΠΈΡΠ°ΡΠ΅Π»ΡΠ½ΠΎΡΡΠΈ;
[x]. check - Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ ΠΏΡΠ΅Π΄Π»ΠΎΠΆΠ΅Π½ΠΈΠΉ check, ΠΏΡΠΎΠ²Π΅ΡΡΡΡΠΈΡ Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΡ ΡΠΎΠΎΡΠ²Π΅ΡΡΡΠ²ΡΡΡΠΈΡ ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ. ΠΠ»ΡΡΠ΅Π²ΠΎΠ΅ ΡΠ»ΠΎΠ²ΠΎ all ΡΠ²Π»ΡΠ΅ΡΡΡ ΡΠΈΠ½ΠΎΠ½ΠΈΠΌΠΎΠΌ check.
ΠΠ° ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΠ΅ΠΌ "no" ΠΊΠ°ΠΆΠ΄ΡΠΉ ΡΡΠΎΠ²Π΅Π½Ρ Π°Π²ΡΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΈ Π²Π»Π΅ΡΠ΅Ρ Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ Π²ΡΠ΅Ρ ΠΏΡΠ΅Π΄ΡΠ΄ΡΡΠΈΡ ΡΡΠΎΠ²Π½Π΅ΠΉ. Π ΡΠ°ΡΡΠ½ΠΎΡΡΠΈ, Π½Π΅ ΠΈΠΌΠ΅Π΅Ρ ΡΠΌΡΡΠ»Π° ΡΠΏΡΠ°Π²Π»ΡΡΡ ΠΏΠΎΡΡΡΡΠ»ΠΎΠ²ΠΈΡΠΌΠΈ, Π΅ΡΠ»ΠΈ Π½Π΅ ΠΏΡΠΎΠ²Π΅ΡΠΈΡΡ Π²ΡΠΏΠΎΠ»Π½ΠΈΠΌΠΎΡΡΡ ΠΏΡΠ΅Π΄ΡΡΠ»ΠΎΠ²ΠΈΠΉ. ΠΡΠΈΠΌ ΠΎΠ±ΡΡΡΠ½ΡΠ΅ΡΡΡ ΡΠΊΠ²ΠΈΠ²Π°Π»Π΅Π½ΡΠ½ΠΎΡΡΡ check ΠΈ all.
ΠΡΠΈ Π²ΠΊΠ»ΡΡΠ΅Π½Π½ΠΎΠΌ ΠΌΠΎΠ½ΠΈΡΠΎΡΠΈΠ½Π³Π΅ ΠΏΠΎΠΊΠ° ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡ Π²ΡΠΏΠΎΠ»Π½ΡΡΡΡΡ Π½ΠΈΠΊΠ°ΠΊΠΎΠ³ΠΎ Π²ΠΈΠ΄ΠΈΠΌΠΎΠ³ΠΎ ΡΡΡΠ΅ΠΊΡΠ° Π½Π° ΠΏΡΠΎΡΠ΅ΡΡ Π²ΡΡΠΈΡΠ»Π΅Π½ΠΈΠΉ ΠΎΠ½ΠΈ Π½Π΅ ΠΎΠΊΠ°Π·ΡΠ²Π°ΡΡ, Π΅ΡΠ»ΠΈ Π½Π΅ ΡΡΠΈΡΠ°ΡΡ Π·Π°ΡΡΠ°Ρ ΠΏΡΠΎΡΠ΅ΡΡΠΎΡΠ½ΠΎΠ³ΠΎ Π²ΡΠ΅ΠΌΠ΅Π½ΠΈ. ΠΠΎ Π΅ΡΠ»ΠΈ ΠΎΠ΄Π½ΠΎ ΠΈΠ· ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΠΉ ΠΏΡΠΈΠ½ΠΈΠΌΠ°Π΅Ρ Π·Π½Π°ΡΠ΅Π½ΠΈΠ΅ false, ΡΠΎ ΡΡΠΎ Π΄ΠΎΠ²ΠΎΠ»ΡΠ½ΠΎ ΡΠ΅ΡΡΠ΅Π·Π½ΠΎΠ΅ ΡΠΎΠ±ΡΡΠΈΠ΅, ΠΏΡΠΈΠ²ΠΎΠ΄ΡΡΠ΅Π΅ ΠΎΠ±ΡΡΠ½ΠΎ ΠΊ Π·Π°Π²Π΅ΡΡΠ΅Π½ΠΈΡ ΡΠ°Π±ΠΎΡΡ. Π€Π°ΠΊΡΠΈΡΠ΅ΡΠΊΠΈ, Π²ΠΎΠ·Π±ΡΠΆΠ΄Π°Π΅ΡΡΡ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΠ΅, ΠΈ, Π΅ΡΠ»ΠΈ Π½Π΅ ΠΏΡΠΈΠ½ΡΡΡ ΡΠΏΠ΅ΡΠΈΠ°Π»ΡΠ½ΡΡ ΠΌΠ΅Ρ ΠΏΠΎ Π·Π°Ρ Π²Π°ΡΡ ΡΡΠΎΠ³ΠΎ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΡ, ΡΠΎ Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ ΠΎΡΡΠ°Π½ΠΎΠ²ΠΈΡΡΡ. ΠΡΠΈ ΡΡΠΎΠΌ, ΠΎΠ΄Π½Π°ΠΊΠΎ, Π±ΡΠ΄Π΅Ρ ΡΠΎΠ·Π΄Π°Π½Π° ΡΠ°Π±Π»ΠΈΡΠ° ΠΈΡΡΠΎΡΠΈΠΈ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΡ (exception history table) Π² Π΅Π΅ ΠΎΠ±ΡΠ΅ΠΉ ΡΠΎΡΠΌΠ΅:
Failure: object: O2 class: YOUR_CLASS routine: your_routine
Cause: precondition violation, clause: not_too_small
Called by: object: O2 class: YOUR_CLASS routine: his_routine
Called by: object: O1 class: HER_CLASS routine: her_routine
...
ΠΡΠΎ Π΄Π°Π΅Ρ Π½Π°ΠΌ ΡΠ΅ΠΏΠΎΡΠΊΡ Π²ΡΠ·ΠΎΠ²ΠΎΠ², Π½Π°ΡΠΈΠ½Π°ΡΡΡΡΡΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΎΠΉ, Π²ΡΠ·Π²Π°Π²ΡΠ΅ΠΉ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΠ΅, Ρ ΡΠΊΠ°Π·Π°Π½ΠΈΠ΅ΠΌ Π²ΡΠ΅Ρ ΠΎΠ±ΡΠ΅ΠΊΡΠΎΠ² ΠΈ ΠΈΡ ΠΊΠ»Π°ΡΡΠΎΠ² - ΠΊΠ»ΠΈΠ΅Π½ΡΠΎΠ², Π² ΠΊΠΎΠ½Π΅ΡΠ½ΠΎΠΌ ΡΡΠ΅ΡΠ΅, Π²ΡΠ·Π²Π°Π²ΡΠΈΡ ΡΡΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΡ. ΠΠΎΠΊΠ°Π·Π°Π½Π½Π°Ρ Π·Π΄Π΅ΡΡ ΡΠΎΡΠΌΠ° ΡΠ²Π»ΡΠ΅ΡΡΡ ΡΠΎΠ»ΡΠΊΠΎ Π½Π°Π±ΡΠΎΡΠΊΠΎΠΌ; ΠΎΠ±ΡΡΠΆΠ΄Π΅Π½ΠΈΠ΅ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΠΉ Π² ΡΠ»Π΅Π΄ΡΡΡΠ΅ΠΉ Π»Π΅ΠΊΡΠΈΠΈ Π΄Π°ΡΡ Π±ΠΎΠ»Π΅Π΅ ΠΏΠΎΠ»Π½ΡΠΉ ΠΏΡΠΈΠΌΠ΅Ρ ΡΠ°Π±Π»ΠΈΡΡ ΠΈΡΡΠΎΡΠΈΠΈ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΡ.
ΠΠΎΠ·ΠΌΠΎΠΆΠ½ΡΠ΅ ΠΌΠ΅ΡΠΊΠΈ, Π΄ΠΎΠΏΡΡΠΊΠ°Π΅ΠΌΡΠ΅ Π² ΡΡΠ²Π΅ΡΠΆΠ΄Π΅Π½ΠΈΡΡ , ΡΠ°ΠΊΠΈΠ΅ ΠΊΠ°ΠΊ not_too_small Π²
your_routine (x: INTEGER) is
require
not_too_small: x >= Minimum_value
...
ΠΏΠ΅ΡΠ΅ΡΠΈΡΠ»ΡΡΡΡΡ ΠΏΡΠΈ ΡΡΠ°ΡΡΠΈΡΠΎΠ²ΠΊΠ΅ ΠΈΡΠΊΠ»ΡΡΠ΅Π½ΠΈΡ, ΡΡΠΎ ΠΏΠΎΠΌΠΎΠ³Π°Π΅Ρ ΠΈΠ΄Π΅Π½ΡΠΈΡΠΈΡΠΈΡΠΎΠ²Π°ΡΡ, ΡΡΠΎ ΠΆΠ΅ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΏΠΎΡΠ»ΠΎ Π½Π΅ ΡΠ°ΠΊ.
ΠΠ°ΠΊΠΎΠ² ΠΎΠΏΡΠΈΠΌΠ°Π»ΡΠ½ΡΠΉ ΡΡΠΎΠ²Π΅Π½Ρ ΠΌΠΎΠ½ΠΈΡΠΎΡΠΈΠ½Π³Π°?
ΠΠ°ΠΊΠΎΠΉ ΡΡΠΎΠ²Π΅Π½Ρ ΡΡΠ°ΡΡΠΈΡΠΎΠ²ΠΊΠΈ ΡΠ»Π΅Π΄ΡΠ΅Ρ Π²ΠΊΠ»ΡΡΠ°ΡΡ? ΠΡΠ²Π΅Ρ Π²ΡΡΠ°Π±Π°ΡΡΠ²Π°Π΅ΡΡΡ Π² ΡΠ΅Π·ΡΠ»ΡΡΠ°ΡΠ΅ ΠΊΠΎΠΌΠΏΡΠΎΠΌΠΈΡΡΠ°, Ρ ΡΡΠ΅ΡΠΎΠΌ ΡΠ»Π΅Π΄ΡΡΡΠΈΡ ΡΠ°ΠΊΡΠΎΡΠΎΠ²: ΡΡΠΎΠ²Π½Ρ Π΄ΠΎΠ²Π΅ΡΠΈΡ ΠΊ ΠΊΠΎΡΡΠ΅ΠΊΡΠ½ΠΎΡΡΠΈ ΠΠ, Π½Π°ΡΠΊΠΎΠ»ΡΠΊΠΎ ΠΊΡΠΈΡΠΈΡΠ½Ρ ΠΏΠΎΡΠ΅ΡΠΈ ΡΡΡΠ΅ΠΊΡΠΈΠ²Π½ΠΎΡΡΠΈ, Π½Π°ΡΠΊΠΎΠ»ΡΠΊΠΎ ΡΠ΅ΡΡΠ΅Π·Π½Ρ ΠΏΠΎΡΠ»Π΅Π΄ΡΡΠ²ΠΈΡ Π½Π΅ ΠΎΠ±Π½Π°ΡΡΠΆΠ΅Π½Π½ΡΡ ΠΎΡΠΈΠ±ΠΎΠΊ Π² ΠΏΠ΅ΡΠΈΠΎΠ΄ Π²ΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΡ.