ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ β€” большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π­Ρ‚ΠΎ ΡΡ‚Π°Ρ‚ΡŒΡ-ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄ Бтэнфордского сСминара. Но ΠΏΠ΅Ρ€Π΅Π΄ Π½Π΅ΠΉ нСбольшоС вступлСниС. Как ΠΎΠ±Ρ€Π°Π·ΡƒΡŽΡ‚ΡΡ Π·ΠΎΠΌΠ±ΠΈ? ΠšΠ°ΠΆΠ΄Ρ‹ΠΉ ΠΏΠΎΠΏΠ°Π΄Π°Π» Π² ΡΠΈΡ‚ΡƒΠ°Ρ†ΠΈΡŽ, ΠΊΠΎΠ³Π΄Π° хочСтся ΠΏΠΎΠ΄Ρ‚ΡΠ½ΡƒΡ‚ΡŒ Π΄Ρ€ΡƒΠ³Π° ΠΈΠ»ΠΈ ΠΊΠΎΠ»Π»Π΅Π³Ρƒ Π΄ΠΎ своСго уровня, Π° Π½Π΅ получаСтся. ΠŸΡ€ΠΈΡ‡Ρ‘ΠΌ Β«Π½Π΅ получаСтся» Π½Π΅ ΡΡ‚ΠΎΠ»ΡŒΠΊΠΎ Ρƒ тСбя, сколько Ρƒ Π½Π΅Π³ΠΎ: Π½Π° ΠΎΠ΄Π½ΠΎΠΉ Ρ‡Π°ΡˆΠ΅ вСсов находится Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ Π·Π°Ρ€ΠΏΠ»Π°Ρ‚Π°, Π·Π°Π΄Π°Ρ‡ΠΈ ΠΈ Ρ‚Π°ΠΊ Π΄Π°Π»Π΅Π΅, Π° Π½Π° Π΄Ρ€ΡƒΠ³ΠΎΠΉ β€” Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎΡΡ‚ΡŒ Π΄ΡƒΠΌΠ°Ρ‚ΡŒ. Π”ΡƒΠΌΠ°Ρ‚ΡŒ нСприятно ΠΈ больно. Он быстро сдаётся ΠΈ ΠΏΡ€ΠΎΠ΄ΠΎΠ»ΠΆΠ°Π΅Ρ‚ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠ΄, ΡΠΎΠ²Π΅Ρ€ΡˆΠ΅Π½Π½ΠΎ Π½Π΅ Π²ΠΊΠ»ΡŽΡ‡Π°Ρ ΠΌΠΎΠ·Π³. Π’Ρ‹ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΠ΅ΡˆΡŒ, насколько ΠΌΠ½ΠΎΠ³ΠΎ сил Π½ΡƒΠΆΠ½ΠΎ ΠΏΠΎΡ‚Ρ€Π°Ρ‚ΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΡ€Π΅ΠΎΠ΄ΠΎΠ»Π΅Ρ‚ΡŒ Π±Π°Ρ€ΡŒΠ΅Ρ€ Π²Ρ‹ΡƒΡ‡Π΅Π½Π½ΠΎΠΉ бСспомощности, ΠΈ просто Π½Π΅ дСлаСшь этого. Π’Π°ΠΊ ΠΎΠ±Ρ€Π°Π·ΡƒΡŽΡ‚ΡΡ Π·ΠΎΠΌΠ±ΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… Π²Ρ€ΠΎΠ΄Π΅ Π±Ρ‹ ΠΌΠΎΠΆΠ½ΠΎ Π²Ρ‹Π»Π΅Ρ‡ΠΈΡ‚ΡŒ, Π½ΠΎ Π²Ρ€ΠΎΠ΄Π΅ Π±Ρ‹ ΠΈ Π½ΠΈΠΊΡ‚ΠΎ этим Π·Π°Π½ΠΈΠΌΠ°Ρ‚ΡŒΡΡ Π½Π΅ станСт.

Когда я ΡƒΠ²ΠΈΠ΄Π΅Π», Ρ‡Ρ‚ΠΎ ЛСсли Лэмпорт (Π΄Π°-Π΄Π°, Ρ‚ΠΎΡ‚ самый Ρ‚ΠΎΠ²Π°Ρ€ΠΈΡ‰ ΠΈΠ· ΡƒΡ‡Π΅Π±Π½ΠΈΠΊΠΎΠ²) ΠΏΡ€ΠΈΠ΅Π·ΠΆΠ°Π΅Ρ‚ Π² Россию ΠΈ Π΄Π΅Π»Π°Π΅Ρ‚ Π½Π΅ Π΄ΠΎΠΊΠ»Π°Π΄, Π° сСссию вопросов-ΠΎΡ‚Π²Π΅Ρ‚ΠΎΠ², я Π½Π΅ΠΌΠ½ΠΎΠ³ΠΎ настороТился. На всякий случай, ЛСсли β€” всСмирно извСстный ΡƒΡ‡Ρ‘Π½Ρ‹ΠΉ, Π°Π²Ρ‚ΠΎΡ€ ΠΎΡΠ½ΠΎΠ²ΠΎΠΏΠΎΠ»Π°Π³Π°ΡŽΡ‰ΠΈΡ… Ρ€Π°Π±ΠΎΡ‚ Π² распрСдСлённых вычислСниях, Π° Π΅Ρ‰Ρ‘ Π²Ρ‹ Π΅Π³ΠΎ ΠΌΠΎΠΆΠ΅Ρ‚Π΅ Π·Π½Π°Ρ‚ΡŒ ΠΏΠΎ Π±ΡƒΠΊΠ²Π°ΠΌ La Π² словС LaTeX β€” Β«Lamport TeXΒ». Π’Ρ‚ΠΎΡ€Ρ‹ΠΌ Π½Π°ΡΡ‚ΠΎΡ€Π°ΠΆΠΈΠ²Π°ΡŽΡ‰ΠΈΠΌ Ρ„Π°ΠΊΡ‚ΠΎΡ€ΠΎΠΌ являСтся Π΅Π³ΠΎ Ρ‚Ρ€Π΅Π±ΠΎΠ²Π°Π½ΠΈΠ΅: ΠΊΠ°ΠΆΠ΄Ρ‹ΠΉ, ΠΊΡ‚ΠΎ ΠΏΡ€ΠΈΠ΄Ρ‘Ρ‚, Π΄ΠΎΠ»ΠΆΠ΅Π½ (ΡΠΎΠ²Π΅Ρ€ΡˆΠ΅Π½Π½ΠΎ бСсплатно) Π·Π°Ρ€Π°Π½Π΅Π΅ ΠΏΡ€ΠΎΡΠ»ΡƒΡˆΠ°Ρ‚ΡŒ ΠΏΠ°Ρ€Ρƒ Π΅Π³ΠΎ Π΄ΠΎΠΊΠ»Π°Π΄ΠΎΠ², ΠΏΡ€ΠΈΠ΄ΡƒΠΌΠ°Ρ‚ΡŒ ΠΏΠΎ Π½ΠΈΠΌ ΠΌΠΈΠ½ΠΈΠΌΡƒΠΌ ΠΎΠ΄ΠΈΠ½ вопрос ΠΈ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ Ρ‚ΠΎΠ³Π΄Π° ΡƒΠΆΠ΅ ΠΏΡ€ΠΈΡ…ΠΎΠ΄ΠΈΡ‚ΡŒ. РСшил ΠΏΠΎΡΠΌΠΎΡ‚Ρ€Π΅Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ Ρ‚Π°ΠΌ Лэмпорт Π²Π΅Ρ‰Π°Π΅Ρ‚ β€” ΠΈ это Π²Π΅Π»ΠΈΠΊΠΎΠ»Π΅ΠΏΠ½ΠΎ! Π­Ρ‚ΠΎ Π² точности Ρ‚Π° ΡˆΡ‚ΡƒΠΊΠ°, волшСбная ссылка-Ρ‚Π°Π±Π»Π΅Ρ‚ΠΊΠ° для лСчСния зомбятины. ΠŸΡ€Π΅Π΄ΡƒΠΏΡ€Π΅ΠΆΠ΄Π°ΡŽ: ΠΎΡ‚ тСкста ΠΌΠΎΠΆΠ΅Ρ‚ Π·Π½Π°Ρ‚Π½ΠΎ ΠΏΠΎΠ΄Π³ΠΎΡ€Π΅Ρ‚ΡŒ Ρƒ Π»ΡŽΠ±ΠΈΡ‚Π΅Π»Π΅ΠΉ свСрхгибких ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ»ΠΎΠ³ΠΈΠΉ ΠΈ Π½Π΅Π»ΡŽΠ±ΠΈΡ‚Π΅Π»Π΅ΠΉ Ρ‚Π΅ΡΡ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ написанноС.

ПослС Ρ…Π°Π±Ρ€ΠΎΠΊΠ°Ρ‚Π°, собствСнно, начинаСтся ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄ сСминара. ΠŸΡ€ΠΈΡΡ‚Π½ΠΎΠ³ΠΎ чтСния!

Π—Π° ΠΊΠ°ΠΊΠΎΠ΅ Π±Ρ‹ Π·Π°Π΄Π°Π½ΠΈΠ΅ Π²Ρ‹ Π½ΠΈ взялись, Π²Π°ΠΌ всСгда Π½ΡƒΠΆΠ½ΠΎ ΠΏΡ€ΠΎΠΉΡ‚ΠΈ Ρ‚Ρ€ΠΈ шага:

  • ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒΡΡ, ΠΊΠ°ΠΊΠΎΠΉ Ρ†Π΅Π»ΠΈ Π²Ρ‹ Ρ…ΠΎΡ‚ΠΈΡ‚Π΅ Π΄ΠΎΡΡ‚ΠΈΡ‡ΡŒ;
  • Ρ€Π΅ΡˆΠΈΡ‚ΡŒ, ΠΊΠ°ΠΊ ΠΈΠΌΠ΅Π½Π½ΠΎ Π²Ρ‹ Π±ΡƒΠ΄Π΅Ρ‚Π΅ Π΄ΠΎΠ±ΠΈΠ²Π°Ρ‚ΡŒΡΡ своСй Ρ†Π΅Π»ΠΈ;
  • ΠΏΡ€ΠΈΠΉΡ‚ΠΈ ΠΊ своСй Ρ†Π΅Π»ΠΈ.

Π­Ρ‚ΠΎ касаСтся ΠΈ программирования. Когда ΠΌΡ‹ пишСм ΠΊΠΎΠ΄, Π½Π°ΠΌ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ:

  • Ρ€Π΅ΡˆΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ Π΄ΠΎΠ»ΠΆΠ½Π° Π΄Π΅Π»Π°Ρ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°;
  • ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ, ΠΊΠ°ΠΊ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΎΠ½Π° Π΄ΠΎΠ»ΠΆΠ½Π° Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡ‚ΡŒ свою Π·Π°Π΄Π°Ρ‡Ρƒ;
  • Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ ΡΠΎΠΎΡ‚Π²Π΅Ρ‚ΡΡ‚Π²ΡƒΡŽΡ‰ΠΈΠΉ ΠΊΠΎΠ΄.

ПослСдний шаг, ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎ, ΠΎΡ‡Π΅Π½ΡŒ Π²Π°ΠΆΠ΅Π½, Π½ΠΎ ΠΎ Π½Π΅ΠΌ я Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ΡŒ сСгодня Π½Π΅ Π±ΡƒΠ΄Ρƒ. ВмСсто этого ΠΌΡ‹ обсудим ΠΏΠ΅Ρ€Π²Ρ‹Π΅ Π΄Π²Π°. Π˜Ρ… выполняСт ΠΊΠ°ΠΆΠ΄Ρ‹ΠΉ программист ΠΏΡ€Π΅ΠΆΠ΄Π΅, Ρ‡Π΅ΠΌ Π½Π°Ρ‡Π°Ρ‚ΡŒ Ρ€Π°Π±ΠΎΡ‚Π°Ρ‚ΡŒ. Π’Ρ‹ Π½Π΅ ΡΠ°Π΄ΠΈΡ‚Π΅ΡΡŒ ΠΏΠΈΡΠ°Ρ‚ΡŒ, Ссли Π½Π΅ Ρ€Π΅ΡˆΠΈΠ»ΠΈ, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΏΠΈΡˆΠ΅Ρ‚Π΅: Π±Ρ€Π°ΡƒΠ·Π΅Ρ€ ΠΈΠ»ΠΈ Π±Π°Π·Ρƒ Π΄Π°Π½Π½Ρ‹Ρ…. ΠžΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠ΅ прСдставлСниС ΠΎ Ρ†Π΅Π»ΠΈ ΠΎΠ±ΡΠ·Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ Π΄ΠΎΠ»ΠΆΠ½ΠΎ ΠΏΡ€ΠΈΡΡƒΡ‚ΡΡ‚Π²ΠΎΠ²Π°Ρ‚ΡŒ. И Π²Ρ‹ ΠΎΠ±ΡΠ·Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Π΅Ρ‚Π΅, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° Π±ΡƒΠ΄Π΅Ρ‚ Π΄Π΅Π»Π°Ρ‚ΡŒ, Π° Π½Π΅ ΠΏΠΈΡˆΠ΅Ρ‚Π΅ ΠΊΠΎΠ΅-ΠΊΠ°ΠΊ Π² Π½Π°Π΄Π΅ΠΆΠ΄Π΅, Ρ‡Ρ‚ΠΎ ΠΊΠΎΠ΄ сам ΠΊΠ°ΠΊ-Π½ΠΈΠ±ΡƒΠ΄ΡŒ прСвратится Π² Π±Ρ€Π°ΡƒΠ·Π΅Ρ€.

Как ΠΈΠΌΠ΅Π½Π½ΠΎ происходит это ΠΏΡ€Π΅Π΄Π²Π°Ρ€ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎΠ΅ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Π½ΠΈΠ΅ ΠΊΠΎΠ΄Π°? Бколько усилий Π½Π°ΠΌ слСдуСт Π½Π° это Ρ‚Ρ€Π°Ρ‚ΠΈΡ‚ΡŒ? ВсС зависит ΠΎΡ‚ Ρ‚ΠΎΠ³ΠΎ, насколько ΡΠ»ΠΎΠΆΠ½ΡƒΡŽ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡƒ ΠΌΡ‹ Ρ€Π΅ΡˆΠ°Π΅ΠΌ. ΠŸΡ€Π΅Π΄ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ, ΠΌΡ‹ Ρ…ΠΎΡ‚ΠΈΠΌ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΎΡ‚ΠΊΠ°Π·ΠΎΡƒΡΡ‚ΠΎΠΉΡ‡ΠΈΠ²ΡƒΡŽ Ρ€Π°ΡΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΡƒΡŽ систСму. Π’ этом случаС Π½Π°ΠΌ слСдуСт ΠΎΠ±Π΄ΡƒΠΌΠ°Ρ‚ΡŒ всС ΠΊΠ°ΠΊ слСдуСт, ΠΏΡ€Π΅ΠΆΠ΄Π΅ Ρ‡Π΅ΠΌ ΡΠ°Π΄ΠΈΡ‚ΡŒΡΡ Π·Π° ΠΊΠΎΠ΄. А Ссли Π½Π°ΠΌ просто Π½ΡƒΠΆΠ½ΠΎ ΡƒΠ²Π΅Π»ΠΈΡ‡ΠΈΡ‚ΡŒ Ρ†Π΅Π»ΠΎΡ‡ΠΈΡΠ»Π΅Π½Π½ΡƒΡŽ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ Π½Π° 1? На ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ взгляд, здСсь всС Ρ‚Ρ€ΠΈΠ²ΠΈΠ°Π»ΡŒΠ½ΠΎ, ΠΈ Π½ΠΈΠΊΠ°ΠΊΠΈΡ… Ρ€Π°Π·ΠΌΡ‹ΡˆΠ»Π΅Π½ΠΈΠΉ Π½Π΅ Π½ΡƒΠΆΠ½ΠΎ, Π½ΠΎ ΠΏΠΎΡ‚ΠΎΠΌ ΠΌΡ‹ вспоминаСм, Ρ‡Ρ‚ΠΎ ΠΌΠΎΠΆΠ΅Ρ‚ ΠΏΡ€ΠΎΠΈΠ·ΠΎΠΉΡ‚ΠΈ ΠΏΠ΅Ρ€Π΅ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ, Π΄Π°ΠΆΠ΅ для Ρ‚ΠΎΠ³ΠΎ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠ½ΡΡ‚ΡŒ, простая ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΠ° ΠΈΠ»ΠΈ слоТная β€” Π²Π½Π°Ρ‡Π°Π»Π΅ Π½ΡƒΠΆΠ½ΠΎ ΠΏΠΎΠ΄ΡƒΠΌΠ°Ρ‚ΡŒ.

Если ΠΏΡ€Π΅Π΄Π²Π°Ρ€ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΠ°Ρ‚ΡŒ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Π΅ Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡ‹, ΠΌΠΎΠΆΠ½ΠΎ ΠΈΠ·Π±Π΅ΠΆΠ°Ρ‚ΡŒ ошибок. Но для этого Π½ΡƒΠΆΠ½ΠΎ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ вашС ΠΌΡ‹ΡˆΠ»Π΅Π½ΠΈΠ΅ Π±Ρ‹Π»ΠΎ ясным. Π§Ρ‚ΠΎΠ±Ρ‹ этого Π΄ΠΎΠ±ΠΈΡ‚ΡŒΡΡ, Π½ΡƒΠΆΠ½ΠΎ Π·Π°ΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ свои мысли. МнС ΠΎΡ‡Π΅Π½ΡŒ нравится Ρ†ΠΈΡ‚Π°Ρ‚Π° Π”ΠΈΠΊΠ° Π“ΠΈΠ½Π΄ΠΎΠ½Π°: «Когда Π²Ρ‹ ΠΏΠΈΡˆΠ΅Ρ‚Π΅, ΠΏΡ€ΠΈΡ€ΠΎΠ΄Π° дСмонстрируСт Π²Π°ΠΌ, насколько Π½Π΅Ρ€ΡΡˆΠ»ΠΈΠ²ΠΎ вашС ΠΌΡ‹ΡˆΠ»Π΅Π½ΠΈΠ΅Β». Если Π²Ρ‹ Π½Π΅ ΠΏΠΈΡˆΠ΅Ρ‚Π΅, Π²Π°ΠΌ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ каТСтся, Ρ‡Ρ‚ΠΎ Π²Ρ‹ мыслитС. А Π·Π°ΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ свои мысли Π½ΡƒΠΆΠ½ΠΎ Π² Ρ„ΠΎΡ€ΠΌΠ΅ спСцификаций.

Π‘ΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡŽΡ‚ мноТСство Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ, Π² особСнности Π² ΠΊΡ€ΡƒΠΏΠ½Ρ‹Ρ… ΠΏΡ€ΠΎΠ΅ΠΊΡ‚Π°Ρ…. Но я Π±ΡƒΠ΄Ρƒ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ΡŒ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΠΎΠ± ΠΎΠ΄Π½ΠΎΠΉ ΠΈΠ· Π½ΠΈΡ…: ΠΎΠ½ΠΈ ΠΏΠΎΠΌΠΎΠ³Π°ΡŽΡ‚ Π½Π°ΠΌ ясно ΠΌΡ‹ΡΠ»ΠΈΡ‚ΡŒ. Ясно ΠΌΡ‹ΡΠ»ΠΈΡ‚ΡŒ ΠΎΡ‡Π΅Π½ΡŒ Π²Π°ΠΆΠ½ΠΎ ΠΈ довольно Ρ‚Ρ€ΡƒΠ΄Π½ΠΎ, поэтому здСсь Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ любоС ΠΏΠΎΠ΄ΡΠΏΠΎΡ€ΡŒΠ΅. На ΠΊΠ°ΠΊΠΎΠΌ языкС Π½Π°ΠΌ слСдуСт ΠΏΠΈΡΠ°Ρ‚ΡŒ спСцификации? Π­Ρ‚ΠΎ Π²ΠΎΠΎΠ±Ρ‰Π΅ всСгда ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ вопрос для программистов: Π½Π° ΠΊΠ°ΠΊΠΎΠΌ языкС ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΏΠΈΡΠ°Ρ‚ΡŒ. Одного ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎΠ³ΠΎ ΠΎΡ‚Π²Π΅Ρ‚Π° Π½Π° Π½Π΅Π³ΠΎ Π½Π΅Ρ‚: ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΌΡ‹ Ρ€Π΅ΡˆΠ°Π΅ΠΌ, слишком ΠΌΠ½ΠΎΠ³ΠΎΠΎΠ±Ρ€Π°Π·Π½Ρ‹Π΅. Для Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΏΠΎΠ»Π΅Π·Π΅Π½ TLA+ β€” это язык спСцификаций, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ я Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚Π°Π». Для Π΄Ρ€ΡƒΠ³ΠΈΡ… ΡƒΠ΄ΠΎΠ±Π½Π΅Π΅ ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ китайским. ВсС зависит ΠΎΡ‚ ситуации.

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

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

Π§Ρ‚ΠΎ Ρ‚Π°ΠΊΠΎΠ΅ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°? Π­Ρ‚ΠΎ любой ΠΊΠΎΠ΄, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ ΠΌΠΎΠΆΠ½ΠΎ Ρ€Π°ΡΡΠΌΠ°Ρ‚Ρ€ΠΈΠ²Π°Ρ‚ΡŒ ΡΠ°ΠΌΠΎΡΡ‚ΠΎΡΡ‚Π΅Π»ΡŒΠ½ΠΎ. ΠŸΡ€Π΅Π΄ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ, Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ Π±Ρ€Π°ΡƒΠ·Π΅Ρ€. ΠœΡ‹ выполняСм Ρ‚Ρ€ΠΈ Π·Π°Π΄Π°Ρ‡ΠΈ: ΠΏΡ€ΠΎΠ΅ΠΊΡ‚ΠΈΡ€ΡƒΠ΅ΠΌ прСдставлСниС ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ для ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»Ρ, Π·Π°Ρ‚Π΅ΠΌ пишСм Π²Ρ‹ΡΠΎΠΊΠΎΡƒΡ€ΠΎΠ²Π½Π΅Π²ΡƒΡŽ схСму ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, ΠΈ, Π½Π°ΠΊΠΎΠ½Π΅Ρ†, пишСм ΠΊΠΎΠ΄. По Ρ…ΠΎΠ΄Ρƒ написания ΠΊΠΎΠ΄Π° ΠΌΡ‹ ΠΏΠΎΠ½ΠΈΠΌΠ°Π΅ΠΌ, Ρ‡Ρ‚ΠΎ Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ срСдство для форматирования тСкста. Π—Π΄Π΅ΡΡŒ Π½Π°ΠΌ ΠΎΠΏΡΡ‚ΡŒ Π½ΡƒΠΆΠ½ΠΎ Ρ€Π΅ΡˆΠΈΡ‚ΡŒ Ρ‚Ρ€ΠΈ Π·Π°Π΄Π°Ρ‡ΠΈ: ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ, ΠΊΠ°ΠΊΠΎΠΉ тСкст это срСдство Π±ΡƒΠ΄Π΅Ρ‚ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Ρ‚ΡŒ; Π²Ρ‹Π±Ρ€Π°Ρ‚ΡŒ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ для форматирования; Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠ΄. Π£ этой Π·Π°Π΄Π°Ρ‡ΠΈ своя ΠΏΠΎΠ΄Π·Π°Π΄Π°Ρ‡Π°: ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎ Π²ΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ дСфис Π² слова. Π­Ρ‚Ρƒ ΠΏΠΎΠ΄Π·Π°Π΄Π°Ρ‡Ρƒ ΠΌΡ‹ Ρ‚ΠΎΠΆΠ΅ Ρ€Π΅ΡˆΠ°Π΅ΠΌ Π² Ρ‚Ρ€ΠΈ шага β€” ΠΊΠ°ΠΊ Π²ΠΈΠ΄ΠΈΠΌ, ΠΎΠ½ΠΈ ΠΏΠΎΠ²Ρ‚ΠΎΡ€ΡΡŽΡ‚ΡΡ Π½Π° ΠΌΠ½ΠΎΠ³ΠΈΡ… уровнях.

Рассмотрим Π±ΠΎΠ»Π΅Π΅ ΠΏΠΎΠ΄Ρ€ΠΎΠ±Π½ΠΎ ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ шаг: ΠΊΠ°ΠΊΡƒΡŽ Π·Π°Π΄Π°Ρ‡Ρƒ Ρ€Π΅ΡˆΠ°Π΅Ρ‚ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°. Π—Π΄Π΅ΡΡŒ ΠΌΡ‹ Ρ‡Π°Ρ‰Π΅ всСго ΠΌΠΎΠ΄Π΅Π»ΠΈΡ€ΡƒΠ΅ΠΌ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ ΠΊΠ°ΠΊ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, которая ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅Ρ‚ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π²Ρ…ΠΎΠ΄Π½Ρ‹Π΅ Π΄Π°Π½Π½Ρ‹Π΅ ΠΈ Π΄Π°Π΅Ρ‚ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π΄Π°Π½Π½Ρ‹Π΅ Π½Π° Π²Ρ‹Ρ…ΠΎΠ΄Π΅. Π’ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ΅ функция ΠΎΠ±Ρ‹Ρ‡Π½ΠΎ описываСтся ΠΊΠ°ΠΊ упорядочСнноС мноТСство ΠΏΠ°Ρ€. НапримСр, функция возвСдСния Π² ΠΊΠ²Π°Π΄Ρ€Π°Ρ‚ для Π½Π°Ρ‚ΡƒΡ€Π°Π»ΡŒΠ½Ρ‹Ρ… чисСл описываСтся ΠΊΠ°ΠΊ мноТСство {<0,0>, <1,1>, <2,4>, <3,9>, …}. ΠžΠ±Π»Π°ΡΡ‚ΡŒ опрСдСлСния Ρ‚Π°ΠΊΠΎΠΉ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ β€” мноТСство ΠΏΠ΅Ρ€Π²Ρ‹Ρ… элСмСнтов ΠΊΠ°ΠΆΠ΄ΠΎΠΉ ΠΏΠ°Ρ€Ρ‹, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ Π½Π°Ρ‚ΡƒΡ€Π°Π»ΡŒΠ½Ρ‹Π΅ числа. Π§Ρ‚ΠΎΠ±Ρ‹ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ ΡƒΠΊΠ°Π·Π°Ρ‚ΡŒ Π΅Π΅ ΠΎΠ±Π»Π°ΡΡ‚ΡŒ опрСдСлСния ΠΈ Ρ„ΠΎΡ€ΠΌΡƒΠ»Ρƒ.

Но Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π² ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ΅ β€” это Π½Π΅ Ρ‚ΠΎ ΠΆΠ΅, Ρ‡Ρ‚ΠΎ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π² языках программирования. ΠœΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ° Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΡ€ΠΎΡ‰Π΅. ΠŸΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ Π½Π° слоТныС ΠΏΡ€ΠΈΠΌΠ΅Ρ€Ρ‹ Ρƒ мСня Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ Π½Π΅Ρ‚, рассмотрим простой: функция Π² языкС Π‘ ΠΈΠ»ΠΈ статичСский ΠΌΠ΅Ρ‚ΠΎΠ΄ Π² Java, Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°ΡŽΡ‰ΠΈΠΉ наибольший ΠΎΠ±Ρ‰ΠΈΠΉ Π΄Π΅Π»ΠΈΡ‚Π΅Π»ΡŒ Π΄Π²ΡƒΡ… Ρ†Π΅Π»Ρ‹Ρ… чисСл. Π’ спСцификации этого ΠΌΠ΅Ρ‚ΠΎΠ΄Π° ΠΌΡ‹ напишСм: вычисляСт GCD(M,N) для Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² M ΠΈ N, Π³Π΄Π΅ GCD(M,N) β€” функция, ΠΎΠ±Π»Π°ΡΡ‚ΡŒ опрСдСлСния ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ β€” мноТСство ΠΏΠ°Ρ€ Ρ†Π΅Π»Ρ‹Ρ… чисСл, Π° Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅ΠΌΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ β€” наибольшСС Ρ†Π΅Π»ΠΎΠ΅ число, Π½Π° ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ дСлится M ΠΈ N. Как с этой модСлью соотносится Ρ€Π΅Π°Π»ΡŒΠ½ΠΎΡΡ‚ΡŒ? МодСль ΠΎΠΏΠ΅Ρ€ΠΈΡ€ΡƒΠ΅Ρ‚ с Ρ†Π΅Π»Ρ‹ΠΌΠΈ числами, Π° Π² C ΠΈΠ»ΠΈ Java ΠΌΡ‹ ΠΈΠΌΠ΅Π΅ΠΌ 32-Π±ΠΈΡ‚Π½Ρ‹ΠΉ int. Π­Ρ‚Π° модСль позволяСт Π½Π°ΠΌ Ρ€Π΅ΡˆΠΈΡ‚ΡŒ, ΠΏΡ€Π°Π²ΠΈΠ»Π΅Π½ Π»ΠΈ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ GCD, Π½ΠΎ ΠΎΠ½Π° Π½Π΅ ΠΏΡ€Π΅Π΄ΠΎΡ‚Π²Ρ€Π°Ρ‚ΠΈΡ‚ ошибки пСрСполнСния. Для этого ΠΏΠΎΡ‚Ρ€Π΅Π±ΠΎΠ²Π°Π»Π°ΡΡŒ Π±Ρ‹ Π±ΠΎΠ»Π΅Π΅ слоТная модСль, Π½Π° ΠΊΠΎΡ‚ΠΎΡ€ΡƒΡŽ Π½Π΅Ρ‚ Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ.

ΠŸΠΎΠ³ΠΎΠ²ΠΎΡ€ΠΈΠΌ ΠΎΠ± ограничСниях Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΊΠ°ΠΊ ΠΌΠΎΠ΄Π΅Π»ΠΈ. Π Π°Π±ΠΎΡ‚Π° Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ (Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΎΠ½Π½Ρ‹Ρ… систСм) Π½Π΅ сводится ΠΊ Ρ‚ΠΎΠΌΡƒ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ Π²Π΅Ρ€Π½ΡƒΡ‚ΡŒ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ для ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½Ρ‹Ρ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ², ΠΎΠ½ΠΈ ΠΌΠΎΠ³ΡƒΡ‚ Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡ‚ΡŒΡΡ Π½Π΅ΠΏΡ€Π΅Ρ€Ρ‹Π²Π½ΠΎ. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, функция ΠΊΠ°ΠΊ модСль ΠΏΠ»ΠΎΡ…ΠΎ ΠΏΠΎΠ΄Ρ…ΠΎΠ΄ΠΈΡ‚ для Π²Ρ‚ΠΎΡ€ΠΎΠ³ΠΎ шага: планирования способа Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ Π·Π°Π΄Π°Ρ‡ΠΈ. Быстрая сортировка ΠΈ сортировка ΠΏΡƒΠ·Ρ‹Ρ€ΡŒΠΊΠΎΠΌ Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡŽΡ‚ ΠΎΠ΄Π½Ρƒ ΠΈ Ρ‚Ρƒ ΠΆΠ΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, Π½ΠΎ это ΡΠΎΠ²Π΅Ρ€ΡˆΠ΅Π½Π½ΠΎ Ρ€Π°Π·Π½Ρ‹Π΅ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΡ‹. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ для описания способа достиТСния Ρ†Π΅Π»ΠΈ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ я ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΡŽ Π΄Ρ€ΡƒΠ³ΡƒΡŽ модСль, Π½Π°Π·ΠΎΠ²Π΅ΠΌ Π΅Π΅ стандартная повСдСнчСская модСль. ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° Π² Π½Π΅ΠΉ прСдставлСна ΠΊΠ°ΠΊ мноТСство всСх допустимых ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠΉ, ΠΊΠ°ΠΆΠ΄ΠΎΠ΅ ΠΈΠ· ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ…, Π² свою ΠΎΡ‡Π΅Ρ€Π΅Π΄ΡŒ, являСтся ΠΏΠΎΡΠ»Π΅Π΄ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎΡΡ‚ΡŒΡŽ состояний, Π° состояниС β€” это присвоСниС Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹ΠΌ.

Π”Π°Π²Π°ΠΉΡ‚Π΅ посмотрим, ΠΊΠ°ΠΊ Π±ΡƒΠ΄Π΅Ρ‚ Π²Ρ‹Π³Π»ΡΠ΄Π΅Ρ‚ΡŒ Π²Ρ‚ΠΎΡ€ΠΎΠΉ шаг для Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° Π•Π²ΠΊΠ»ΠΈΠ΄Π°. Нам Π½ΡƒΠΆΠ½ΠΎ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚ΡŒ GCD(M, N). ΠœΡ‹ ΠΈΠ½ΠΈΡ†ΠΈΠ°Π»ΠΈΠ·ΠΈΡ€ΡƒΠ΅ΠΌ M ΠΊΠ°ΠΊ x, Π° N ΠΊΠ°ΠΊ y, Π·Π°Ρ‚Π΅ΠΌ ΠΏΠΎΠ²Ρ‚ΠΎΡ€Π½ΠΎ ΠΎΡ‚Π½ΠΈΠΌΠ°Π΅ΠΌ ΠΌΠ΅Π½ΡŒΡˆΡƒΡŽ ΠΈΠ· этих ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΎΡ‚ большСй Π΄ΠΎ Ρ‚Π΅Ρ… ΠΏΠΎΡ€, ΠΏΠΎΠΊΠ° ΠΎΠ½ΠΈ Π½Π΅ Π±ΡƒΠ΄ΡƒΡ‚ Ρ€Π°Π²Π½Ρ‹. НапримСр, Ссли M = 12, Π° N = 18, ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΎΠΏΠΈΡΠ°Ρ‚ΡŒ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅Π΅ ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅:

[x = 12, y = 18] β†’ [x = 12, y = 6] β†’ [x = 6, y = 6]

А Ссли M = 0 ΠΈ N = 0? Ноль дСлится Π½Π° всС числа, поэтому наибольшСго дСлитСля Π² этом случаС Π½Π΅Ρ‚. Π’ этой ситуации Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π²Π΅Ρ€Π½ΡƒΡ‚ΡŒΡΡ ΠΊ ΠΏΠ΅Ρ€Π²ΠΎΠΌΡƒ ΡˆΠ°Π³Ρƒ ΠΈ ΡΠΏΡ€ΠΎΡΠΈΡ‚ΡŒ: Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Π»ΠΈ Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡ‚ΡŒ ΠΠžΠ” для Π½Π΅ΠΏΠΎΠ»ΠΎΠΆΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹Ρ… чисСл? Если Π² этом Π½Π΅Ρ‚ нСобходимости, Ρ‚ΠΎ Π½ΡƒΠΆΠ½ΠΎ просто ΠΈΠ·ΠΌΠ΅Π½ΠΈΡ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ.

Π—Π΄Π΅ΡΡŒ слСдуСт ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ нСбольшоС отступлСниС ΠΎ продуктивности. Π•Ρ‘ часто ΠΈΠ·ΠΌΠ΅Ρ€ΡΡŽΡ‚ Π² количСствС строк ΠΊΠΎΠ΄Π°, написанных Π·Π° дСнь. Но ваш Ρ‚Ρ€ΡƒΠ΄ Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΠΎΠ»Π΅Π·Π½Π΅Π΅, Ссли Π²Ρ‹ избавились ΠΎΡ‚ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠ³ΠΎ количСства строк, ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ Ρƒ вас стало мСньшС мСста для Π±Π°Π³ΠΎΠ². И ΠΈΠ·Π±Π°Π²Π»ΡΡ‚ΡŒΡΡ ΠΎΡ‚ ΠΊΠΎΠ΄Π° ΠΏΡ€ΠΎΡ‰Π΅ всСго ΠΈΠΌΠ΅Π½Π½ΠΎ Π½Π° ΠΏΠ΅Ρ€Π²ΠΎΠΌ шагС. Π’ΠΏΠΎΠ»Π½Π΅ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, Ρ‡Ρ‚ΠΎ Π²Π°ΠΌ просто Π½Π΅ Π½ΡƒΠΆΠ½Ρ‹ всС Ρ‚Π΅ Π½Π°Π²ΠΎΡ€ΠΎΡ‚Ρ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π²Ρ‹ ΠΏΡ‹Ρ‚Π°Π΅Ρ‚Π΅ΡΡŒ Ρ€Π΅Π°Π»ΠΈΠ·ΠΎΠ²Π°Ρ‚ΡŒ. Π‘Π°ΠΌΡ‹ΠΉ быстрый способ ΡƒΠΏΡ€ΠΎΡΡ‚ΠΈΡ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ ΠΈ ΡΡΠΊΠΎΠ½ΠΎΠΌΠΈΡ‚ΡŒ врСмя β€” Π½Π΅ Π΄Π΅Π»Π°Ρ‚ΡŒ Π²Π΅Ρ‰ΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π½Π΅ стоит Π΄Π΅Π»Π°Ρ‚ΡŒ. Π’Ρ‚ΠΎΡ€ΠΎΠΉ шаг β€” Π½Π° Π²Ρ‚ΠΎΡ€ΠΎΠΌ мСстС ΠΏΠΎ ΠΏΠΎΡ‚Π΅Π½Ρ†ΠΈΠ°Π»Ρƒ для экономии Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ. Если Π²Ρ‹ измСряСтС ΠΏΡ€ΠΎΠ΄ΡƒΠΊΡ‚ΠΈΠ²Π½ΠΎΡΡ‚ΡŒ Π² количСствС написанных строк, Ρ‚ΠΎ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Π½ΠΈΠ΅ способа выполнСния Π·Π°Π΄Π°Ρ‡ΠΈ сдСлаСт вас ΠΌΠ΅Π½Π΅Π΅ ΠΏΡ€ΠΎΠ΄ΡƒΠΊΡ‚ΠΈΠ²Π½Ρ‹ΠΌΠΈ, ΠΏΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ Π²Ρ‹ смоТСтС Ρ€Π΅ΡˆΠΈΡ‚ΡŒ Ρ‚Ρƒ ΠΆΠ΅ Π·Π°Π΄Π°Ρ‡Ρƒ мСньшим объСмом ΠΊΠΎΠ΄Π°. Π’ΠΎΡ‡Π½ΡƒΡŽ статистику я здСсь привСсти Π½Π΅ ΠΌΠΎΠ³Ρƒ, ΠΏΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ Ρƒ мСня Π½Π΅Ρ‚ способа ΠΏΠΎΡΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ Ρ‚ΠΎ количСство строк, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ я Π½Π΅ написал благодаря Ρ‚ΠΎΠΌΡƒ, Ρ‡Ρ‚ΠΎ ΠΏΠΎΡ‚Ρ€Π°Ρ‚ΠΈΠ» врСмя Π½Π° ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ Π½Π° ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ ΠΈ Π²Ρ‚ΠΎΡ€ΠΎΠΉ шаги. И экспСримСнт Ρ‚ΡƒΡ‚ Ρ‚ΠΎΠΆΠ΅ Π½Π΅ ΠΏΠΎΡΡ‚Π°Π²ΠΈΡ‚ΡŒ, ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ Π² экспСримСнтС ΠΌΡ‹ Π½Π΅ ΠΈΠΌΠ΅Π΅ΠΌ ΠΏΡ€Π°Π²Π° Π²Ρ‹ΠΏΠΎΠ»Π½ΠΈΡ‚ΡŒ ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ шаг, Π·Π°Π΄Π°Π½ΠΈΠ΅ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΎ Π·Π°Ρ€Π°Π½Π΅Π΅.

Π’ Π½Π΅Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… спСцификациях Π»Π΅Π³ΠΊΠΎ Π½Π΅ ΡƒΡ‡Π΅ΡΡ‚ΡŒ ΠΌΠ½ΠΎΠ³ΠΈΠ΅ трудности. НичСго слоТного Π² написании строгих спСцификаций для Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π½Π΅Ρ‚, ΠΎΠ±ΡΡƒΠΆΠ΄Π°Ρ‚ΡŒ это я Π½Π΅ Π±ΡƒΠ΄Ρƒ. ВмСсто этого ΠΌΡ‹ ΠΏΠΎΠ³ΠΎΠ²ΠΎΡ€ΠΈΠΌ ΠΎ написании строгих спСцификаций для стандартных повСдСнчСских ΠΌΠΎΠ΄Π΅Π»Π΅ΠΉ. Π•ΡΡ‚ΡŒ Ρ‚Π΅ΠΎΡ€Π΅ΠΌΠ°, которая гласит, Ρ‡Ρ‚ΠΎ любоС мноТСство ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠΉ ΠΌΠΎΠΆΠ½ΠΎ ΠΎΠΏΠΈΡΠ°Ρ‚ΡŒ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ свойства бСзопасности (safety) ΠΈ свойства ТивучСсти (liveness). Π‘Π΅Π·ΠΎΠΏΠ°ΡΠ½ΠΎΡΡ‚ΡŒ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Π½ΠΈΡ‡Π΅Π³ΠΎ ΠΏΠ»ΠΎΡ…ΠΎΠ³ΠΎ Π½Π΅ ΠΏΡ€ΠΎΠΈΠ·ΠΎΠΉΠ΄Π΅Ρ‚, ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° Π½Π΅ выдаст Π½Π΅Π²Π΅Ρ€Π½Ρ‹ΠΉ ΠΎΡ‚Π²Π΅Ρ‚. Π–ΠΈΠ²ΡƒΡ‡Π΅ΡΡ‚ΡŒ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Ρ€Π°Π½ΠΎ ΠΈΠ»ΠΈ ΠΏΠΎΠ·Π΄Π½ΠΎ ΠΏΡ€ΠΎΠΈΠ·ΠΎΠΉΠ΄Π΅Ρ‚ Ρ‡Ρ‚ΠΎ-Ρ‚ΠΎ Ρ…ΠΎΡ€ΠΎΡˆΠ΅Π΅, Ρ‚. Π΅. ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° Ρ€Π°Π½ΠΎ ΠΈΠ»ΠΈ ΠΏΠΎΠ·Π΄Π½ΠΎ даст ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½Ρ‹ΠΉ ΠΎΡ‚Π²Π΅Ρ‚. Как ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, Π±Π΅Π·ΠΎΠΏΠ°ΡΠ½ΠΎΡΡ‚ΡŒ являСтся Π±ΠΎΠ»Π΅Π΅ Π²Π°ΠΆΠ½Ρ‹ΠΌ ΠΏΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»Π΅ΠΌ, ошибки Ρ‡Π°Ρ‰Π΅ всСго Π²ΠΎΠ·Π½ΠΈΠΊΠ°ΡŽΡ‚ ΠΈΠΌΠ΅Π½Π½ΠΎ здСсь. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ для экономии Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ я Π½Π΅ Π±ΡƒΠ΄Ρƒ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ΡŒ ΠΎΠ± ТивучСсти, хотя ΠΎΠ½Π°, ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎ, Ρ‚ΠΎΠΆΠ΅ Π²Π°ΠΆΠ½Π°.

ΠœΡ‹ добиваСмся бСзопасности, прописывая, Π²ΠΎ-ΠΏΠ΅Ρ€Π²Ρ‹Ρ…, мноТСство Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Ρ… исходных состояний. И, Π²ΠΎ-Π²Ρ‚ΠΎΡ€Ρ‹Ρ…, ΠΎΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΡ со всСми Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹ΠΌΠΈ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌΠΈ состояниями для ΠΊΠ°ΠΆΠ΄ΠΎΠ³ΠΎ состояния. Π‘ΡƒΠ΄Π΅ΠΌ вСсти сСбя ΠΊΠ°ΠΊ ΡƒΡ‡Π΅Π½Ρ‹Π΅ ΠΈ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ состояния матСматичСски. Набор исходных состояний описываСтся Ρ„ΠΎΡ€ΠΌΡƒΠ»ΠΎΠΉ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, Π² случаС Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° Π•Π²ΠΊΠ»ΠΈΠ΄Π°: (x = M) ∧ (y = N). Для ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½Ρ‹Ρ… Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ M ΠΈ N сущСствуСт Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΠΎΠ΄Π½ΠΎ исходноС состояниС. ΠžΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΠ΅ со ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌ состояниСм описываСтся Ρ„ΠΎΡ€ΠΌΡƒΠ»ΠΎΠΉ, Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅Π³ΠΎ состояния Π·Π°ΠΏΠΈΡΡ‹Π²Π°ΡŽΡ‚ΡΡ со ΡˆΡ‚Ρ€ΠΈΡ…ΠΎΠΌ, Π° Ρ‚Π΅ΠΊΡƒΡ‰Π΅Π³ΠΎ состояния β€” Π±Π΅Π· ΡˆΡ‚Ρ€ΠΈΡ…Π°. Π’ случаС с Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΎΠΌ Π•Π²ΠΊΠ»ΠΈΠ΄Π° ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΈΠΌΠ΅Ρ‚ΡŒ Π΄Π΅Π»ΠΎ с Π΄ΠΈΠ·ΡŠΡŽΠ½ΠΊΡ†ΠΈΠ΅ΠΉ Π΄Π²ΡƒΡ… Ρ„ΠΎΡ€ΠΌΡƒΠ», Π² ΠΎΠ΄Π½ΠΎΠΉ ΠΈΠ· ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… x являСтся наибольшим Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ΠΌ, Π° Π²ΠΎ Π²Ρ‚ΠΎΡ€ΠΎΠΉ β€” y:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π’ ΠΏΠ΅Ρ€Π²ΠΎΠΌ случаС Π½ΠΎΠ²ΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ y Ρ€Π°Π²Π½ΠΎ ΠΏΡ€Π΅ΠΆΠ½Π΅ΠΌΡƒ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ y, Π° Π½ΠΎΠ²ΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ x ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅ΠΌ, отняв ΠΎΡ‚ большСй ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ ΠΌΠ΅Π½ΡŒΡˆΡƒΡŽ. Π’ΠΎ Π²Ρ‚ΠΎΡ€ΠΎΠΌ случаС ΠΌΡ‹ Π΄Π΅Π»Π°Π΅ΠΌ Π½Π°ΠΎΠ±ΠΎΡ€ΠΎΡ‚.

ВСрнСмся ΠΊ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΡƒ Π•Π²ΠΊΠ»ΠΈΠ΄Π°. ΠŸΡ€Π΅Π΄ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ вновь, Ρ‡Ρ‚ΠΎ M = 12, N = 18. Π­Ρ‚ΠΎ опрСдСляСт СдинствСнноС исходноС состояниС, (x = 12) ∧ (y = 18). Π—Π°Ρ‚Π΅ΠΌ ΠΌΡ‹ подставляСм эти значСния Π² Ρ„ΠΎΡ€ΠΌΡƒΠ»Ρƒ Π²Ρ‹ΡˆΠ΅ ΠΈ ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅ΠΌ:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π—Π΄Π΅ΡΡŒ СдинствСнноС Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΠ΅ Ρ€Π΅ΡˆΠ΅Π½ΠΈΠ΅: x' = 18 - 12 ∧ y' = 12, ΠΈ ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅ΠΌ ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅: [x = 12, y = 18]. Π’ΠΎΡ‡Π½ΠΎ Ρ‚Π°ΠΊ ΠΆΠ΅ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΎΠΏΠΈΡΠ°Ρ‚ΡŒ всС состояния Π² нашСм ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠΈ: [x = 12, y = 18] β†’ [x = 12, y = 6] β†’ [x = 6, y = 6].

Π’ послСднСм состоянии [x = 6, y = 6] ΠΎΠ±Π΅ части выраТСния Π±ΡƒΠ΄ΡƒΡ‚ Π»ΠΎΠΆΠ½Ρ‹, ΡΠ»Π΅Π΄ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ, ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅Π³ΠΎ состояния Ρƒ Π½Π΅Π³ΠΎ Π½Π΅Ρ‚. Π˜Ρ‚Π°ΠΊ, ΠΌΡ‹ ΠΈΠΌΠ΅Π΅ΠΌ ΠΏΠΎΠ»Π½ΡƒΡŽ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ Π²Ρ‚ΠΎΡ€ΠΎΠ³ΠΎ шага β€” ΠΊΠ°ΠΊ Π²ΠΈΠ΄ΠΈΠΌ, это Π²ΠΏΠΎΠ»Π½Π΅ обычная ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ°, ΠΊΠ°ΠΊ Ρƒ ΠΈΠ½ΠΆΠ΅Π½Π΅Ρ€ΠΎΠ² ΠΈ ΡƒΡ‡Π΅Π½Ρ‹Ρ…, Π° Π½Π΅ странная, ΠΊΠ°ΠΊ Π² computer science.

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

Π’ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ΅ Π•Π²ΠΊΠ»ΠΈΠ΄Π° для ΠΊΠ°ΠΆΠ΄ΠΎΠ³ΠΎ значСния x ΠΈ y Π΅ΡΡ‚ΡŒ ΡƒΠ½ΠΈΠΊΠ°Π»ΡŒΠ½Ρ‹Π΅ значСния x' ΠΈ y', ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π΄Π΅Π»Π°ΡŽΡ‚ ΠΎΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΠ΅ со ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌ состояниСм истинным. Π”Ρ€ΡƒΠ³ΠΈΠΌΠΈ словами, Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ Π•Π²ΠΊΠ»ΠΈΠ΄Π° Π΄Π΅Ρ‚Π΅Ρ€ΠΌΠΈΠ½ΠΈΡ€ΠΎΠ²Π°Π½Π½Ρ‹ΠΉ. Π§Ρ‚ΠΎΠ±Ρ‹ ΡΠΌΠΎΠ΄Π΅Π»ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ Π½Π΅Π΄Π΅Ρ‚Π΅Ρ€ΠΌΠΈΠ½ΠΈΡ€ΠΎΠ²Π°Π½Π½Ρ‹ΠΉ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ, Π½ΡƒΠΆΠ½ΠΎ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ Ρƒ Ρ‚Π΅ΠΊΡƒΡ‰Π΅Π³ΠΎ состояния Π±Ρ‹Π»ΠΎ нСсколько Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Ρ… Π±ΡƒΠ΄ΡƒΡ‰ΠΈΡ… состояний, ΠΈ Ρ‡Ρ‚ΠΎΠ±Ρ‹ Ρƒ ΠΊΠ°ΠΆΠ΄ΠΎΠ³ΠΎ значСния ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ Π±Π΅Π· ΡˆΡ‚Ρ€ΠΈΡ…Π° Π±Ρ‹Π»ΠΎ нСсколько Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ со ΡˆΡ‚Ρ€ΠΈΡ…ΠΎΠΌ, ΠΏΡ€ΠΈ ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΎΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΠ΅ со ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌ состояниСм являСтся истинным. Π­Ρ‚ΠΎ нСслоТно ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ, Π½ΠΎ сСйчас ΠΏΡ€ΠΈΠ²ΠΎΠ΄ΠΈΡ‚ΡŒ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Ρ‹ я Π½Π΅ Π±ΡƒΠ΄Ρƒ.

Π§Ρ‚ΠΎΠ±Ρ‹ ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ Ρ€Π°Π±ΠΎΡ‚Π°ΡŽΡ‰ΠΈΠΉ инструмСнт, Π½ΡƒΠΆΠ½Π° Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ°. Как ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ? Для этого Π½Π°ΠΌ понадобится Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹ΠΉ язык, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, TLA+. БпСцификация Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° Π•Π²ΠΊΠ»ΠΈΠ΄Π° Π±ΡƒΠ΄Π΅Ρ‚ Π½Π° этом языкС Π²Ρ‹Π³Π»ΡΠ΄Π΅Ρ‚ΡŒ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π‘ΠΈΠΌΠ²ΠΎΠ» Π·Π½Π°ΠΊΠ° равСнства с Ρ‚Ρ€Π΅ΡƒΠ³ΠΎΠ»ΡŒΠ½ΠΈΠΊΠΎΠΌ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ слСва ΠΎΡ‚ Π·Π½Π°ΠΊΠ° ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΎ ΠΊΠ°ΠΊ Ρ€Π°Π²Π½ΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ справа ΠΎΡ‚ Π·Π½Π°ΠΊΠ°. Π’ сущности, спСцификация β€” это ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅, Π² нашСм случаС Π΄Π²Π° опрСдСлСния. К спСцификации Π² TLA+ Π½ΡƒΠΆΠ½ΠΎ Π΄ΠΎΠ±Π°Π²ΠΈΡ‚ΡŒ объявлСния ΠΈ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ синтаксис, ΠΊΠ°ΠΊ Π½Π° слайдС Π²Ρ‹ΡˆΠ΅. Π’ ASCII это Π±ΡƒΠ΄Π΅Ρ‚ Π²Ρ‹Π³Π»ΡΠ΄Π΅Ρ‚ΡŒ Ρ‚Π°ΠΊ:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Как Π²ΠΈΠ΄ΠΈΠΌ, Π½ΠΈΡ‡Π΅Π³ΠΎ слоТного. Π‘ΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ Π½Π° TLA+ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒ, Ρ‚. Π΅. ΠΎΠ±ΠΎΠΉΡ‚ΠΈ всС Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Π΅ повСдСния Π² нСбольшой ΠΌΠΎΠ΄Π΅Π»ΠΈ. Π’ нашСм случаС этой модСлью Π±ΡƒΠ΄ΡƒΡ‚ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½Ρ‹Π΅ значСния M ΠΈ N. Π­Ρ‚ΠΎ ΠΎΡ‡Π΅Π½ΡŒ эффСктивный ΠΈ простой способ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Ρ†Π΅Π»ΠΈΠΊΠΎΠΌ выполняСтся автоматичСски. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, ΠΌΠΎΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Π΅ Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° истинности ΠΈ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒ ΠΈΡ… мСханичСски, Π½ΠΎ для этого Π½ΡƒΠΆΠ½ΠΎ ΠΌΠ½ΠΎΠ³ΠΎ Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ, поэтому Ρ‚Π°ΠΊ ΠΏΠΎΡ‡Ρ‚ΠΈ Π½ΠΈΠΊΡ‚ΠΎ Π½Π΅ Π΄Π΅Π»Π°Π΅Ρ‚.

Π“Π»Π°Π²Π½Ρ‹ΠΉ нСдостаток TLA+ Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ это ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ°, Π° программисты ΠΈ computer scientists боятся ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠΈ. На ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ взгляд это Π·Π²ΡƒΡ‡ΠΈΡ‚ ΠΊΠ°ΠΊ ΡˆΡƒΡ‚ΠΊΠ°, Π½ΠΎ, ΠΊ соТалСнию, я Π³ΠΎΠ²ΠΎΡ€ΡŽ это Π½Π° ΠΏΠΎΠ»Π½ΠΎΠΌ ΡΠ΅Ρ€ΡŒΠ΅Π·Π΅. Мой ΠΊΠΎΠ»Π»Π΅Π³Π° Ρ‚ΠΎΠ»ΡŒΠΊΠΎ Ρ‡Ρ‚ΠΎ рассказывал ΠΌΠ½Π΅, ΠΊΠ°ΠΊ ΠΎΠ½ пытался ΠΎΠ±ΡŠΡΡΠ½ΠΈΡ‚ΡŒ TLA+ нСскольким Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚Ρ‡ΠΈΠΊΠ°ΠΌ. Как Ρ‚ΠΎΠ»ΡŒΠΊΠΎ Π½Π° экранС появились Ρ„ΠΎΡ€ΠΌΡƒΠ»Ρ‹, Ρƒ Π½ΠΈΡ… сразу ΠΆΠ΅ сдСлались стСклянныС Π³Π»Π°Π·Π°. Π’Π°ΠΊ Ρ‡Ρ‚ΠΎ Ссли TLA+ ΠΏΡƒΠ³Π°Π΅Ρ‚, ΠΌΠΎΠΆΠ½ΠΎ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ PlusCal, это своСго Ρ€ΠΎΠ΄Π° ΠΈΠ³Ρ€ΡƒΡˆΠ΅Ρ‡Π½Ρ‹ΠΉ язык программирования. Π’Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ Π² PlusCal ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ Π»ΡŽΠ±Ρ‹ΠΌ Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ΠΌ TLA+, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ, ΠΏΠΎ Π±ΠΎΠ»ΡŒΡˆΠΎΠΌΡƒ счСту, Π»ΡŽΠ±Ρ‹ΠΌ матСматичСским Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ΠΌ. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, Π² PlusCal Π΅ΡΡ‚ΡŒ синтаксис для нСдСтСрминистичных Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΎΠ². Благодаря Ρ‚ΠΎΠΌΡƒ, Ρ‡Ρ‚ΠΎ Π² PlusCal ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ любоС Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ TLA+, ΠΎΠ½ являСтся Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Π±ΠΎΠ»Π΅Π΅ Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹ΠΌ любого Ρ€Π΅Π°Π»ΡŒΠ½ΠΎΠ³ΠΎ языка программирования. Π”Π°Π»Π΅Π΅, PlusCal компилируСтся Π² Π»Π΅Π³ΠΊΠΎ Ρ‡ΠΈΡ‚Π°Π΅ΠΌΡƒΡŽ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ TLA+. Π­Ρ‚ΠΎ Π½Π΅ Π·Π½Π°Ρ‡ΠΈΡ‚, ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎ, Ρ‡Ρ‚ΠΎ слоТная спСцификация PlusCal прСвратится Π² ΠΏΡ€ΠΎΡΡ‚ΡƒΡŽ Π½Π° TLA+ β€” просто соотвСтствиС ΠΌΠ΅ΠΆΠ΄Ρƒ Π½ΠΈΠΌΠΈ ΠΎΡ‡Π΅Π²ΠΈΠ΄Π½ΠΎΠ΅, Π½Π΅ появится Π΄ΠΎΠΏΠΎΠ»Π½ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎΠΉ слоТности. НаконСц, эту ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ ΠΌΠΎΠΆΠ½ΠΎ Π±ΡƒΠ΄Π΅Ρ‚ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒ инструмСнтами TLA+. Π’ ΠΎΠ±Ρ‰Π΅ΠΌ, PlusCal ΠΌΠΎΠΆΠ΅Ρ‚ ΠΏΠΎΠΌΠΎΡ‡ΡŒ ΠΏΡ€Π΅ΠΎΠ΄ΠΎΠ»Π΅Ρ‚ΡŒ Ρ„ΠΎΠ±ΠΈΡŽ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠΈ, Π΅Π³ΠΎ Π»Π΅Π³ΠΊΠΎ ΠΏΠΎΠ½ΡΡ‚ΡŒ Π΄Π°ΠΆΠ΅ программистам ΠΈ computer scientists. Π’ ΠΏΡ€ΠΎΡˆΠ»ΠΎΠΌ я ΠΊΠ°ΠΊΠΎΠ΅-Ρ‚ΠΎ врСмя (ΠΎΠΊΠΎΠ»ΠΎ 10 Π»Π΅Ρ‚) ΠΏΡƒΠ±Π»ΠΈΠΊΠΎΠ²Π°Π» Π½Π° Π½Π΅ΠΌ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΡ‹.

Π’ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, ΠΊΡ‚ΠΎ-Ρ‚ΠΎ Π²ΠΎΠ·Ρ€Π°Π·ΠΈΡ‚, Ρ‡Ρ‚ΠΎ TLA+ ΠΈ PlusCal β€” это ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ°, Π° ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ° Ρ€Π°Π±ΠΎΡ‚Π°Π΅Ρ‚ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ Π½Π° ΠΏΡ€ΠΈΠ΄ΡƒΠΌΠ°Π½Π½Ρ‹Ρ… ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π°Ρ…. На ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ΅ ΠΆΠ΅ Π½ΡƒΠΆΠ΅Π½ Ρ€Π΅Π°Π»ΡŒΠ½Ρ‹ΠΉ язык с Ρ‚ΠΈΠΏΠ°ΠΌΠΈ, ΠΏΡ€ΠΎΡ†Π΅Π΄ΡƒΡ€Π°ΠΌΠΈ, ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π°ΠΌΠΈ ΠΈ Ρ‚Π°ΠΊ Π΄Π°Π»Π΅Π΅. Π­Ρ‚ΠΎ Π½Π΅ Ρ‚Π°ΠΊ. Π’ΠΎΡ‚, Ρ‡Ρ‚ΠΎ ΠΏΠΈΡˆΠ΅Ρ‚ ΠšΡ€ΠΈΡ Ньюкомб, Ρ€Π°Π±ΠΎΡ‚Π°Π²ΡˆΠΈΠΉ Π² Amazon: Β«ΠœΡ‹ использовали TLA+ Π² дСсяти ΠΊΡ€ΡƒΠΏΠ½Ρ‹Ρ… ΠΏΡ€ΠΎΠ΅ΠΊΡ‚Π°Ρ…, ΠΈ Π² ΠΊΠ°ΠΆΠ΄ΠΎΠΌ случаС Π΅Π³ΠΎ использованиС вносило Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹ΠΉ Π²ΠΊΠ»Π°Π΄ Π² Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚ΠΊΡƒ, ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ ΠΌΡ‹ смогли ΠΎΡ‚Π»ΠΎΠ²ΠΈΡ‚ΡŒ опасныС Π±Π°Π³ΠΈ Π΄ΠΎ попадания Π² ΠΏΡ€ΠΎΠ΄Π°ΠΊΡˆΠ½, ΠΈ ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ ΠΎΠ½ Π΄Π°Π» Π½Π°ΠΌ ΠΏΠΎΠ½ΠΈΠΌΠ°Π½ΠΈΠ΅ ΠΈ ΡƒΠ²Π΅Ρ€Π΅Π½Π½ΠΎΡΡ‚ΡŒ, Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΡ‹Π΅ для агрСссивных ΠΎΠΏΡ‚ΠΈΠΌΠΈΠ·Π°Ρ†ΠΈΠΉ ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ΄ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎΡΡ‚ΠΈ, Π½Π΅ Π²Π»ΠΈΡΡŽΡ‰ΠΈΡ… Π½Π° ΠΈΡΡ‚ΠΈΠ½Π½ΠΎΡΡ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹Β». Часто ΠΌΠΎΠΆΠ½ΠΎ ΡƒΡΠ»Ρ‹ΡˆΠ°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΏΡ€ΠΈ использовании Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ² ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅ΠΌ нСэффСктивный ΠΊΠΎΠ΄ β€” Π½Π° ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ΅ ΠΆΠ΅ всС Ρ€ΠΎΠ²Π½ΠΎ Π½Π°ΠΎΠ±ΠΎΡ€ΠΎΡ‚. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, Π±Ρ‹Ρ‚ΡƒΠ΅Ρ‚ ΠΌΠ½Π΅Π½ΠΈΠ΅, Ρ‡Ρ‚ΠΎ ΠΌΠ΅Π½Π΅Π΄ΠΆΠ΅Ρ€ΠΎΠ² Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ ΡƒΠ±Π΅Π΄ΠΈΡ‚ΡŒ Π² нСобходимости Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ², Π΄Π°ΠΆΠ΅ Ссли программисты ΡƒΠ±Π΅ΠΆΠ΄Π΅Π½Ρ‹ Π² ΠΈΡ… полСзности. А Ньюкомб ΠΏΠΈΡˆΠ΅Ρ‚: Β«ΠœΠ΅Π½Π΅Π΄ΠΆΠ΅Ρ€Ρ‹ Ρ‚Π΅ΠΏΠ΅Ρ€ΡŒ всячСски ΠΏΠΎΠ΄Ρ‚Π°Π»ΠΊΠΈΠ²Π°ΡŽΡ‚ ΠΊ Ρ‚ΠΎΠΌΡƒ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΈΡΠ°Ρ‚ΡŒ спСцификации Π½Π° TLA+, ΠΈ ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎ Π²Ρ‹Π΄Π΅Π»ΡΡŽΡ‚ Π½Π° это врСмя». Π’Π°ΠΊ Ρ‡Ρ‚ΠΎ ΠΊΠΎΠ³Π΄Π° ΠΌΠ΅Π½Π΅Π΄ΠΆΠ΅Ρ€Ρ‹ видят, Ρ‡Ρ‚ΠΎ TLA+ Ρ€Π°Π±ΠΎΡ‚Π°Π΅Ρ‚, ΠΎΠ½ΠΈ с Ρ€Π°Π΄ΠΎΡΡ‚ΡŒΡŽ Π΅Π³ΠΎ ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°ΡŽΡ‚. ΠšΡ€ΠΈΡ Ньюкомб написал это Π³Π΄Π΅-Ρ‚ΠΎ ΡˆΠ΅ΡΡ‚ΡŒ мСсяцСв Ρ‚ΠΎΠΌΡƒ Π½Π°Π·Π°Π΄ (Π² октябрС 2014 Π³ΠΎΠ΄Π°), сСйчас ΠΆΠ΅, насколько я знаю, TLA+ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅Ρ‚ΡΡ Π² 14 ΠΏΡ€ΠΎΠ΅ΠΊΡ‚Π°Ρ…, Π° Π½Π΅ 10. Π”Ρ€ΡƒΠ³ΠΎΠΉ ΠΏΡ€ΠΈΠΌΠ΅Ρ€ относится ΠΊ ΠΏΡ€ΠΎΠ΅ΠΊΡ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΡŽ XBox 360. К Π§Π°Ρ€Π»ΡŒΠ·Ρƒ Π’Π΅ΠΊΠ΅Ρ€Ρƒ ΠΏΡ€ΠΈΡˆΠ΅Π» стаТСр ΠΈ написал ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ для систСмы памяти. Благодаря этой спСцификации Π±Ρ‹Π» Π½Π°ΠΉΠ΄Π΅Π½ Π±Π°Π³, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ ΠΈΠ½Π°Ρ‡Π΅ Π±Ρ‹Π» Π±Ρ‹ Π½Π΅ Π·Π°ΠΌΠ΅Ρ‡Π΅Π½, ΠΈ ΠΈΠ·-Π·Π° ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ каТдая XBox 360 ΠΏΠ°Π΄Π°Π»Π° Π±Ρ‹ послС Ρ‡Π΅Ρ‚Ρ‹Ρ€Π΅Ρ… часов использования. Π˜Π½ΠΆΠ΅Π½Π΅Ρ€Ρ‹ ΠΈΠ· IBM ΠΏΠΎΠ΄Ρ‚Π²Π΅Ρ€Π΄ΠΈΠ»ΠΈ, Ρ‡Ρ‚ΠΎ ΠΈΡ… тСсты Π½Π΅ ΠΎΠ±Π½Π°Ρ€ΡƒΠΆΠΈΠ»ΠΈ Π±Ρ‹ этот Π±Π°Π³.

Π‘ΠΎΠ»Π΅Π΅ ΠΏΠΎΠ΄Ρ€ΠΎΠ±Π½ΠΎ ΠΏΡ€ΠΎ TLA+ Π²Ρ‹ ΠΌΠΎΠΆΠ΅Ρ‚Π΅ ΠΏΠΎΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ Π² ΠΈΠ½Ρ‚Π΅Ρ€Π½Π΅Ρ‚Π΅, Π° сСйчас Π΄Π°Π²Π°ΠΉΡ‚Π΅ ΠΏΠΎΠ³ΠΎΠ²ΠΎΡ€ΠΈΠΌ ΠΎ Π½Π΅Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… спСцификациях. Нам Ρ€Π΅Π΄ΠΊΠΎ приходится ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡŽΡ‚ наимСньший ΠΎΠ±Ρ‰ΠΈΠΉ Π΄Π΅Π»ΠΈΡ‚Π΅Π»ΡŒ ΠΈ Ρ‚ΠΎΠΌΡƒ ΠΏΠΎΠ΄ΠΎΠ±Π½ΠΎΠ΅. Π—Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Ρ‡Π°Ρ‰Π΅ ΠΌΡ‹ пишСм ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ Π²Ρ€ΠΎΠ΄Π΅ инструмСнта структурной распСчатки (pretty-printer), ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ я написал для TLA+. ПослС самой простой ΠΎΠ±Ρ€Π°Π±ΠΎΡ‚ΠΊΠΈ ΠΊΠΎΠ΄ Π½Π° TLA+ выглядСл Π±Ρ‹ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Но Π² ΠΏΡ€ΠΈΠ²Π΅Π΄Π΅Π½Π½ΠΎΠΌ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π΅ ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒ скорСС всСго Ρ…ΠΎΡ‚Π΅Π», Ρ‡Ρ‚ΠΎΠ±Ρ‹ Π·Π½Π°ΠΊΠΈ ΠΊΠΎΠ½ΡŠΡŽΠ½ΠΊΡ†ΠΈΠΈ ΠΈ равСнства Π±Ρ‹Π»ΠΈ Π²Ρ‹Ρ€Π°Π²Π½Π΅Π½Ρ‹. Π’Π°ΠΊ Ρ‡Ρ‚ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎΠ΅ Ρ„ΠΎΡ€ΠΌΠ°Ρ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ выглядСло Π±Ρ‹ скорСС Ρ‚Π°ΠΊ:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Рассмотрим Π΄Ρ€ΡƒΠ³ΠΎΠΉ ΠΏΡ€ΠΈΠΌΠ΅Ρ€:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π—Π΄Π΅ΡΡŒ, Π½Π°ΠΎΠ±ΠΎΡ€ΠΎΡ‚, Π²Ρ‹Ρ€Π°Π²Π½ΠΈΠ²Π°Π½ΠΈΠ΅ Π·Π½Π°ΠΊΠΎΠ² равСнства, слоТСния ΠΈ умноТСния Π² источникС Π±Ρ‹Π»ΠΎ случайным, поэтому самой простой ΠΎΠ±Ρ€Π°Π±ΠΎΡ‚ΠΊΠΈ Π²ΠΏΠΎΠ»Π½Π΅ достаточно. Π’ ΠΎΠ±Ρ‰Π΅ΠΌ, Ρ‚ΠΎΡ‡Π½ΠΎΠ³ΠΎ матСматичСского опрСдСлСния Π²Π΅Ρ€Π½ΠΎΠ³ΠΎ форматирования Π½Π΅Ρ‚, ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ Β«ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎΠ΅Β» Π² Π΄Π°Π½Π½ΠΎΠΌ случаС Π·Π½Π°Ρ‡ΠΈΡ‚ Β«Ρ‚Π°ΠΊΠΎΠ΅, ΠΊΠ°ΠΊΠΎΠ΅ Ρ…ΠΎΡ‡Π΅Ρ‚ ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΒ», Π° это матСматичСски ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ нСльзя.

Казалось Π±Ρ‹, Ссли Ρƒ нас Π½Π΅Ρ‚ опрСдСлСния истинности, Ρ‚ΠΎ спСцификация бСсполСзна. Но это Π½Π΅ Ρ‚Π°ΠΊ. Если ΠΌΡ‹ Π½Π΅ Π·Π½Π°Π΅ΠΌ, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° Π΄ΠΎΠ»ΠΆΠ½Π° ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ, это Π½Π΅ Π·Π½Π°Ρ‡ΠΈΡ‚, Ρ‡Ρ‚ΠΎ Π½Π°ΠΌ Π½Π΅ Π½ΡƒΠΆΠ½ΠΎ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Ρ‚ΡŒ Π΅Π΅ Ρ€Π°Π±ΠΎΡ‚Ρƒ β€” Π½Π°ΠΎΠ±ΠΎΡ€ΠΎΡ‚, ΠΌΡ‹ Π΄ΠΎΠ»ΠΆΠ½Ρ‹ ΠΏΠΎΡ‚Ρ€Π°Ρ‚ΠΈΡ‚ΡŒ Π½Π° это Π΅Ρ‰Π΅ большС усилий. БпСцификация здСсь особСнно Π²Π°ΠΆΠ½Π°. ΠžΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ ΠΎΠΏΡ‚ΠΈΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ для структурной распСчатки Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, Π½ΠΎ это Π½Π΅ Π·Π½Π°Ρ‡ΠΈΡ‚, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Π½Π΅ Π΄ΠΎΠ»ΠΆΠ½Ρ‹ Π·Π° Π½Π΅Π΅ Π±Ρ€Π°Ρ‚ΡŒΡΡ Π²ΠΎΠΎΠ±Ρ‰Π΅, Π° ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠ΄ ΠΊΠ°ΠΊ ΠΏΠΎΡ‚ΠΎΠΊ сознания β€” это Π½Π΅ Π΄Π΅Π»ΠΎ. Π’ ΠΈΡ‚ΠΎΠ³Π΅ я написал ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ ΠΈΠ· ΡˆΠ΅ΡΡ‚ΠΈ ΠΏΡ€Π°Π²ΠΈΠ» с опрСдСлСниями Π² Ρ„ΠΎΡ€ΠΌΠ΅ ΠΊΠΎΠΌΠΌΠ΅Π½Ρ‚Π°Ρ€ΠΈΠ΅Π² Π² Java-Ρ„Π°ΠΉΠ»Π΅. Π’ΠΎΡ‚ ΠΏΡ€ΠΈΠΌΠ΅Ρ€ ΠΎΠ΄Π½ΠΎΠ³ΠΎ ΠΈΠ· ΠΏΡ€Π°Π²ΠΈΠ»: a left-comment token is LeftComment aligned with its covering token. Π­Ρ‚ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ написано Π½Π°, скаТСм Ρ‚Π°ΠΊ, матСматичСском английском: LeftComment aligned, left-comment ΠΈ covering token β€” Ρ‚Π΅Ρ€ΠΌΠΈΠ½Ρ‹ с опрСдСлСниями. Π­Ρ‚ΠΎ Ρ‚ΠΎ, ΠΊΠ°ΠΊ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠΈ ΠΎΠΏΠΈΡΡ‹Π²Π°ΡŽΡ‚ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΡƒ: ΠΏΠΈΡˆΡƒΡ‚ опрСдСлСния Ρ‚Π΅Ρ€ΠΌΠΈΠ½ΠΎΠ² ΠΈ Π½Π° основС Π½ΠΈΡ… β€” ΠΏΡ€Π°Π²ΠΈΠ»Π°. Польза ΠΎΡ‚ Ρ‚Π°ΠΊΠΎΠΉ спСцификации Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ ΠΏΠΎΠ½ΡΡ‚ΡŒ ΠΈ ΠΎΡ‚Π»Π°Π΄ΠΈΡ‚ΡŒ ΡˆΠ΅ΡΡ‚ΡŒ ΠΏΡ€Π°Π²ΠΈΠ» Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΡ€ΠΎΡ‰Π΅, Ρ‡Π΅ΠΌ 850 строк ΠΊΠΎΠ΄Π°. Надо ΡΠΊΠ°Π·Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ эти ΠΏΡ€Π°Π²ΠΈΠ»Π° Π±Ρ‹Π»ΠΎ нСпросто, довольно ΠΌΠ½ΠΎΠ³ΠΎ Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ ΡƒΡˆΠ»ΠΎ Π½Π° ΠΈΡ… ΠΎΡ‚Π»Π°Π΄ΠΊΡƒ. Π‘ΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎ для этой Ρ†Π΅Π»ΠΈ я написал ΠΊΠΎΠ΄, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ сообщал, ΠΊΠ°ΠΊΠΎΠ΅ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅Ρ‚ΡΡ. Благодаря Ρ‚ΠΎΠΌΡƒ, Ρ‡Ρ‚ΠΎ я ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΠ» эти ΡˆΠ΅ΡΡ‚ΡŒ ΠΏΡ€Π°Π²ΠΈΠ» Π½Π° Π½Π΅ΡΠΊΠΎΠ»ΡŒΠΊΠΈΡ… ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π°Ρ…, ΠΌΠ½Π΅ Π½Π΅ Π½ΡƒΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ ΠΎΡ‚Π»Π°ΠΆΠΈΠ²Π°Ρ‚ΡŒ 850 строк ΠΊΠΎΠ΄Π°, ΠΈ Π±Π°Π³ΠΈ оказалось довольно Π»Π΅Π³ΠΊΠΎ Π½Π°ΠΉΡ‚ΠΈ. Π’ Java для этого Π΅ΡΡ‚ΡŒ ΠΎΡ‚Π»ΠΈΡ‡Π½Ρ‹Π΅ инструмСнты. Если Π±Ρ‹ я просто написал ΠΊΠΎΠ΄, Ρ‚ΠΎ Ρƒ мСня ΡƒΡˆΠ»ΠΎ Π±Ρ‹ Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ большС Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ, ΠΈ Ρ„ΠΎΡ€ΠΌΠ°Ρ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠ»ΠΎΡΡŒ Π±Ρ‹ Ρ…ΡƒΠ΄ΡˆΠ΅Π³ΠΎ качСства.

ΠŸΠΎΡ‡Π΅ΠΌΡƒ нСльзя Π±Ρ‹Π»ΠΎ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ? Π‘ ΠΎΠ΄Π½ΠΎΠΉ стороны, ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎΡΡ‚ΡŒ выполнСния здСсь Π½Π΅ слишком Π²Π°ΠΆΠ½Π°. Бтруктурная распСчатка ΠΎΠ±ΡΠ·Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ ΠΊΠΎΠΌΡƒ-Ρ‚ΠΎ Π½Π΅ ΡƒΠ³ΠΎΠ΄ΠΈΡ‚, Ρ‚Π°ΠΊ Ρ‡Ρ‚ΠΎ ΠΌΠ½Π΅ Π½Π΅ Π½ΡƒΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ Π΄ΠΎΠ±ΠΈΠ²Π°Ρ‚ΡŒΡΡ ΠΏΡ€Π°Π²ΠΈΠ»ΡŒΠ½ΠΎΠΉ Ρ€Π°Π±ΠΎΡ‚Ρ‹ Π²ΠΎ всСх Π½Π΅ΠΎΡ€Π΄ΠΈΠ½Π°Ρ€Π½Ρ‹Ρ… ситуациях. Π•Ρ‰Π΅ Π²Π°ΠΆΠ½Π΅Π΅ Ρ‚ΠΎΡ‚ Ρ„Π°ΠΊΡ‚, Ρ‡Ρ‚ΠΎ Ρƒ мСня Π½Π΅ Π±Ρ‹Π»ΠΎ Π°Π΄Π΅ΠΊΠ²Π°Ρ‚Π½Ρ‹Ρ… инструмСнтов. БрСдство для ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠΈ ΠΌΠΎΠ΄Π΅Π»Π΅ΠΉ TLA+ здСсь бСсполСзно, Ρ‚Π°ΠΊ Ρ‡Ρ‚ΠΎ ΠΌΠ½Π΅ ΠΏΡ€ΠΈΡˆΠ»ΠΎΡΡŒ Π±Ρ‹ Π²Ρ€ΡƒΡ‡Π½ΡƒΡŽ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Ρ‹.

Π£ ΠΏΡ€ΠΈΠ²Π΅Π΄Π΅Π½Π½ΠΎΠΉ спСцификации Π΅ΡΡ‚ΡŒ Ρ‡Π΅Ρ€Ρ‚Ρ‹, ΠΎΠ±Ρ‰ΠΈΠ΅ для всСх спСцификаций. Она Π±ΠΎΠ»Π΅Π΅ высокого уровня, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄. Π Π΅Π°Π»ΠΈΠ·ΠΎΠ²Π°Ρ‚ΡŒ Π΅Π΅ ΠΌΠΎΠΆΠ½ΠΎ Π½Π° любом языкС. Для Π΅Π΅ написания бСсполСзны ΠΊΠ°ΠΊΠΈΠ΅-Π»ΠΈΠ±ΠΎ инструмСнты ΠΈΠ»ΠΈ ΠΌΠ΅Ρ‚ΠΎΠ΄Ρ‹. Никакой курс программирования Π²Π°ΠΌ Π½Π΅ ΠΏΠΎΠΌΠΎΠΆΠ΅Ρ‚ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ эту ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ. И Π½Π΅ сущСствуСт инструмСнтов, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΌΠΎΠ³Π»ΠΈ Π±Ρ‹ ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ эту ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ Π½Π΅Π½ΡƒΠΆΠ½ΠΎΠΉ, Ссли, ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎ, Π²Ρ‹ Π½Π΅ ΠΏΠΈΡˆΠ΅Ρ‚Π΅ язык ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎ для написания ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ структурной распСчатки Π½Π° TLA+. НаконСц, эта спСцификация Π½ΠΈΡ‡Π΅Π³ΠΎ Π½Π΅ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, ΠΊΠ°ΠΊ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠ΄, Π² Π½Π΅ΠΉ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ указываСтся, Ρ‡Ρ‚ΠΎ этот ΠΊΠΎΠ΄ Π΄Π΅Π»Π°Π΅Ρ‚. ΠœΡ‹ пишСм ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠΌΠΎΡ‡ΡŒ Π½Π°ΠΌ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΠ°Ρ‚ΡŒ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡƒ, ΠΏΡ€Π΅ΠΆΠ΄Π΅ Ρ‡Π΅ΠΌ ΠΌΡ‹ Π½Π°Ρ‡Π½Π΅ΠΌ Π΄ΡƒΠΌΠ°Ρ‚ΡŒ ΠΎ ΠΊΠΎΠ΄Π΅.

Но Ρƒ этой спСцификации Π΅ΡΡ‚ΡŒ ΠΈ особСнности, ΠΎΡ‚Π»ΠΈΡ‡Π°ΡŽΡ‰ΠΈΠ΅ Π΅Π΅ ΠΎΡ‚ Π΄Ρ€ΡƒΠ³ΠΈΡ… спСцификаций. 95% Π΄Ρ€ΡƒΠ³ΠΈΡ… спСцификаций Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ ΠΊΠΎΡ€ΠΎΡ‡Π΅ ΠΈ ΠΏΡ€ΠΎΡ‰Π΅:

ΠŸΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ — большС, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΠ½Π³

Π”Π°Π»Π΅Π΅, эта спСцификация являСтся Π½Π°Π±ΠΎΡ€ΠΎΠΌ ΠΏΡ€Π°Π²ΠΈΠ». Как ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, это ΠΏΡ€ΠΈΠ·Π½Π°ΠΊ ΠΏΠ»ΠΎΡ…ΠΎΠΉ спСцификации. ΠŸΠΎΠ½ΡΡ‚ΡŒ послСдствия Π½Π°Π±ΠΎΡ€Π° ΠΏΡ€Π°Π²ΠΈΠ» довольно Ρ‚Ρ€ΡƒΠ΄Π½ΠΎ, ΠΈ ΠΈΠΌΠ΅Π½Π½ΠΎ поэтому ΠΌΠ½Π΅ ΠΏΡ€ΠΈΡˆΠ»ΠΎΡΡŒ ΠΏΠΎΡ‚Ρ€Π°Ρ‚ΠΈΡ‚ΡŒ ΠΌΠ½ΠΎΠ³ΠΎ Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ Π½Π° ΠΈΡ… ΠΎΡ‚Π»Π°Π΄ΠΊΡƒ. Π’Π΅ΠΌ Π½Π΅ ΠΌΠ΅Π½Π΅Π΅, Π² Π΄Π°Π½Π½ΠΎΠΌ случаС Π»ΡƒΡ‡ΡˆΠ΅Π³ΠΎ способа ΠΌΠ½Π΅ Π±Ρ‹Π»ΠΎ Π½Π΅ Π½Π°ΠΉΡ‚ΠΈ.

Π‘Ρ‚ΠΎΠΈΡ‚ ΡΠΊΠ°Π·Π°Ρ‚ΡŒ нСсколько слов ΠΎ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°Ρ…, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Ρ€Π°Π±ΠΎΡ‚Π°ΡŽΡ‚ Π½Π΅ΠΏΡ€Π΅Ρ€Ρ‹Π²Π½ΠΎ. Как ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, ΠΎΠ½ΠΈ Ρ€Π°Π±ΠΎΡ‚Π°ΡŽΡ‚ ΠΏΠ°Ρ€Π°Π»Π»Π΅Π»ΡŒΠ½ΠΎ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΎΠ½Π½Ρ‹Π΅ систСмы ΠΈΠ»ΠΈ распрСдСлСнныС систСмы. Π Π°Π·ΠΎΠ±Ρ€Π°Ρ‚ΡŒΡΡ Π² Π½ΠΈΡ… Π² ΡƒΠΌΠ΅ ΠΈΠ»ΠΈ Π½Π° Π±ΡƒΠΌΠ°Π³Π΅ ΠΌΠΎΠ³ΡƒΡ‚ ΠΎΡ‡Π΅Π½ΡŒ Π½Π΅ΠΌΠ½ΠΎΠ³ΠΈΠ΅, ΠΈ я ΠΊ ΠΈΡ… числу Π½Π΅ ΠΏΡ€ΠΈΠ½Π°Π΄Π»Π΅ΠΆΡƒ, хотя ΠΊΠΎΠ³Π΄Π°-Ρ‚ΠΎ ΠΌΠ½Π΅ это Π±Ρ‹Π»ΠΎ ΠΏΠΎ силам. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΡ‹ инструмСнты, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π±ΡƒΠ΄ΡƒΡ‚ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΡΡ‚ΡŒ Π½Π°ΡˆΡƒ Ρ€Π°Π±ΠΎΡ‚Ρƒ β€” Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, TLA+ ΠΈΠ»ΠΈ PlusCal.

Π—Π°Ρ‡Π΅ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ, Ссли я ΠΈ Ρ‚Π°ΠΊ Π·Π½Π°Π», Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΊΠΎΠ΄ Π΄ΠΎΠ»ΠΆΠ΅Π½ Π΄Π΅Π»Π°Ρ‚ΡŒ? На самом Π΄Π΅Π»Π΅, ΠΌΠ½Π΅ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ казалось, Π±ΡƒΠ΄Ρ‚ΠΎ Π±Ρ‹ я это знаю. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, ΠΏΡ€ΠΈ Π½Π°Π»ΠΈΡ‡ΠΈΠΈ спСцификации постороннСму Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊΡƒ ΡƒΠΆΠ΅ Π½Π΅ Π½ΡƒΠΆΠ½ΠΎ Π·Π°Π»Π΅Π·Π°Ρ‚ΡŒ Π² ΠΊΠΎΠ΄, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠ½ΡΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΎΠ½ Π΄Π΅Π»Π°Π΅Ρ‚. Π£ мСня Π΅ΡΡ‚ΡŒ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ: Π½Π΅ Π΄ΠΎΠ»ΠΆΠ½ΠΎ Π±Ρ‹Ρ‚ΡŒ Π½ΠΈΠΊΠ°ΠΊΠΈΡ… ΠΎΠ±Ρ‰ΠΈΡ… ΠΏΡ€Π°Π²ΠΈΠ». Π£ этого ΠΏΡ€Π°Π²ΠΈΠ»Π°, ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎ ΠΆΠ΅, Π΅ΡΡ‚ΡŒ ΠΈΡΠΊΠ»ΡŽΡ‡Π΅Π½ΠΈΠ΅, это СдинствСнноС ΠΎΠ±Ρ‰Π΅Π΅ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌΡƒ я ΡΠ»Π΅Π΄ΡƒΡŽ: спСцификация Ρ‚ΠΎΠ³ΠΎ, Ρ‡Ρ‚ΠΎ Π΄Π΅Π»Π°Π΅Ρ‚ ΠΊΠΎΠ΄, Π΄ΠΎΠ»ΠΆΠ½Π° ΡΠΎΠΎΠ±Ρ‰Π°Ρ‚ΡŒ людям всС, Ρ‡Ρ‚ΠΎ ΠΈΠΌ Π½ΡƒΠΆΠ½ΠΎ Π·Π½Π°Ρ‚ΡŒ ΠΏΡ€ΠΈ использовании этого ΠΊΠΎΠ΄Π°.

Π˜Ρ‚Π°ΠΊ, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ программистам Π½ΡƒΠΆΠ½ΠΎ Π·Π½Π°Ρ‚ΡŒ ΠΎ ΠΌΡ‹ΡˆΠ»Π΅Π½ΠΈΠΈ? Для Π½Π°Ρ‡Π°Π»Π°, Ρ‚ΠΎ ΠΆΠ΅, Ρ‡Ρ‚ΠΎ ΠΈ всСм: Ссли Ρ‚Ρ‹ Π½Π΅ пишСшь, Ρ‚ΠΎ Ρ‚Π΅Π±Π΅ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ каТСтся, Ρ‡Ρ‚ΠΎ Ρ‚Ρ‹ ΠΌΡ‹ΡΠ»ΠΈΡˆΡŒ. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, Π½ΡƒΠΆΠ½ΠΎ Π΄ΡƒΠΌΠ°Ρ‚ΡŒ, ΠΏΡ€Π΅ΠΆΠ΄Π΅ Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΡ‚ΡŒ, Π° это Π·Π½Π°Ρ‡ΠΈΡ‚, Π½ΡƒΠΆΠ½ΠΎ ΠΏΠΈΡΠ°Ρ‚ΡŒ, ΠΏΡ€Π΅ΠΆΠ΄Π΅ Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΡ‚ΡŒ. БпСцификация β€” это Ρ‚ΠΎ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ пишСм ΠΏΠ΅Ρ€Π΅Π΄ Ρ‚Π΅ΠΌ, ΠΊΠ°ΠΊ Π½Π°Ρ‡Π°Ρ‚ΡŒ ΠΊΠΎΠ΄ΠΈΡ‚ΡŒ. БпСцификация Π½ΡƒΠΆΠ½Π° для любого ΠΊΠΎΠ΄Π°, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ ΠΊΠ΅ΠΌ-Π»ΠΈΠ±ΠΎ использован ΠΈΠ»ΠΈ ΠΈΠ·ΠΌΠ΅Π½Π΅Π½. И этим Β«ΠΊΡ‚ΠΎ-Π»ΠΈΠ±ΠΎΒ» ΠΌΠΎΠΆΠ΅Ρ‚ ΠΎΠΊΠ°Π·Π°Ρ‚ΡŒΡΡ сам Π°Π²Ρ‚ΠΎΡ€ ΠΊΠΎΠ΄Π° Ρ‡Π΅Ρ€Π΅Π· мСсяц послС Π΅Π³ΠΎ написания. БпСцификация Π½ΡƒΠΆΠ½Π° для Π±ΠΎΠ»ΡŒΡˆΠΈΡ… ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ ΠΈ систСм, для классов, для ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ² ΠΈ ΠΈΠ½ΠΎΠ³Π΄Π° Π΄Π°ΠΆΠ΅ для слоТных участков ΠΎΡ‚Π΄Π΅Π»ΡŒΠ½ΠΎΠ³ΠΎ ΠΌΠ΅Ρ‚ΠΎΠ΄Π°. Π§Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π½ΠΎ Π½ΡƒΠΆΠ½ΠΎ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΎ ΠΊΠΎΠ΄Π΅? НуТно ΠΎΠΏΠΈΡΠ°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΎΠ½ Π΄Π΅Π»Π°Π΅Ρ‚, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ Ρ‚ΠΎ, Ρ‡Ρ‚ΠΎ ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ ΠΏΠΎΠ»Π΅Π·Π½ΠΎ Π»ΡŽΠ±ΠΎΠΌΡƒ Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊΡƒ, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΡŽΡ‰Π΅ΠΌΡƒ этот ΠΊΠΎΠ΄. Иногда ΠΌΠΎΠΆΠ΅Ρ‚ Ρ‚Π°ΠΊΠΆΠ΅ Π±Ρ‹Ρ‚ΡŒ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡƒΠΊΠ°Π·Π°Ρ‚ΡŒ, ΠΊΠ°ΠΊ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΊΠΎΠ΄ достигаСт своСй Ρ†Π΅Π»ΠΈ. Если этот способ ΠΌΡ‹ ΠΏΡ€ΠΎΡ…ΠΎΠ΄ΠΈΠ»ΠΈ Π² курсС Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΎΠ², Ρ‚ΠΎ ΠΌΡ‹ Π½Π°Π·Ρ‹Π²Π°Π΅ΠΌ это Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΎΠΌ. Если ΠΆΠ΅ это Π½Π΅Ρ‡Ρ‚ΠΎ Π±ΠΎΠ»Π΅Π΅ ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎΠ΅ ΠΈ Π½ΠΎΠ²ΠΎΠ΅, Ρ‚ΠΎ ΠΌΡ‹ Π½Π°Π·Ρ‹Π²Π°Π΅ΠΌ это высокоуровнСвым ΠΏΡ€ΠΎΠ΅ΠΊΡ‚ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ΠΌ. Π€ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ€Π°Π·Π½ΠΈΡ†Ρ‹ здСсь Π½Π΅Ρ‚: ΠΈ Ρ‚ΠΎ, ΠΈ Π΄Ρ€ΡƒΠ³ΠΎΠ΅ являСтся абстрактной модСлью ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹.

Как ΠΈΠΌΠ΅Π½Π½ΠΎ слСдуСт ΠΏΠΈΡΠ°Ρ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ ΠΊΠΎΠ΄Π°? Π“Π»Π°Π²Π½ΠΎΠ΅: ΠΎΠ½Π° Π΄ΠΎΠ»ΠΆΠ½Π° Π±Ρ‹Ρ‚ΡŒ Π½Π° ΡƒΡ€ΠΎΠ²Π΅Π½ΡŒ Π²Ρ‹ΡˆΠ΅ самого ΠΊΠΎΠ΄Π°. Она Π΄ΠΎΠ»ΠΆΠ½Π° ΠΎΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ состояния ΠΈ повСдСния. Она Π΄ΠΎΠ»ΠΆΠ½Π° Π±Ρ‹Ρ‚ΡŒ Π½Π°ΡΡ‚ΠΎΠ»ΡŒΠΊΠΎ строгой, насколько этого Ρ‚Ρ€Π΅Π±ΡƒΠ΅Ρ‚ Π·Π°Π΄Π°Ρ‡Π°. Если Π²Ρ‹ ΠΏΠΈΡˆΠ΅Ρ‚Π΅ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ способа Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ Π·Π°Π΄Π°Ρ‡ΠΈ, Ρ‚ΠΎ Π΅Π΅ ΠΌΠΎΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ Π½Π° псСвдокодС ΠΈΠ»ΠΈ ΠΏΡ€ΠΈ ΠΏΠΎΠΌΠΎΡ‰ΠΈ PlusCal. Π£Ρ‡ΠΈΡ‚ΡŒΡΡ ΠΏΠΈΡΠ°Ρ‚ΡŒ спСцификации Π½ΡƒΠΆΠ½ΠΎ Π½Π° Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… спСцификациях. Π­Ρ‚ΠΎ даст Π²Π°ΠΌ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΡ‹Π΅ Π½Π°Π²Ρ‹ΠΊΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΏΠΎΠΌΠΎΠ³ΡƒΡ‚ Π² Ρ‚ΠΎΠΌ числС ΠΈ с Π½Π΅Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹ΠΌΠΈ. А ΠΊΠ°ΠΊ Π½Π°ΡƒΡ‡ΠΈΡ‚ΡŒΡΡ ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Π΅ спСцификации? Когда ΠΌΡ‹ ΡƒΡ‡ΠΈΠ»ΠΈΡΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΡŽ, ΠΌΡ‹ писали ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, Π° Π·Π°Ρ‚Π΅ΠΌ ΠΎΡ‚Π»Π°ΠΆΠΈΠ²Π°Π»ΠΈ ΠΈΡ…. Π’ΠΎ ΠΆΠ΅ самоС здСсь: Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ, ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒ Π΅Π΅ ΠΏΡ€ΠΈ ΠΏΠΎΠΌΠΎΡ‰ΠΈ срСдства ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠΈ ΠΌΠΎΠ΄Π΅Π»Π΅ΠΉ ΠΈ ΠΈΡΠΏΡ€Π°Π²ΠΈΡ‚ΡŒ ошибки. TLA+, Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, Π½Π΅ самый Π»ΡƒΡ‡ΡˆΠΈΠΉ язык для Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ спСцификации, ΠΈ для Π²Π°ΡˆΠΈΡ… ΠΊΠΎΠ½ΠΊΡ€Π΅Ρ‚Π½Ρ‹Ρ… Π½ΡƒΠΆΠ΄ скорСС всСго Π»ΡƒΡ‡ΡˆΠ΅ ΠΏΠΎΠ΄ΠΎΠΉΠ΄Π΅Ρ‚ Π΄Ρ€ΡƒΠ³ΠΎΠΉ язык. ΠŸΡ€Π΅ΠΈΠΌΡƒΡ‰Π΅ΡΡ‚Π²ΠΎ TLA+ Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ ΠΎΠ½ ΠΎΡ‚Π»ΠΈΡ‡Π½ΠΎ ΡƒΡ‡ΠΈΡ‚ матСматичСскому ΠΌΡ‹ΡˆΠ»Π΅Π½ΠΈΡŽ.

Как ΡΠ²ΡΠ·Π°Ρ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ ΠΈ ΠΊΠΎΠ΄? ΠŸΡ€ΠΈ ΠΏΠΎΠΌΠΎΡ‰ΠΈ ΠΊΠΎΠΌΠΌΠ΅Π½Ρ‚Π°Ρ€ΠΈΠ΅Π², ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΡΠ²ΡΠ·Ρ‹Π²Π°ΡŽΡ‚ матСматичСскиС понятия ΠΈ ΠΈΡ… Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΡŽ. Если Π²Ρ‹ Ρ€Π°Π±ΠΎΡ‚Π°Π΅Ρ‚Π΅ с Π³Ρ€Π°Ρ„Π°ΠΌΠΈ, Ρ‚ΠΎ Π½Π° ΡƒΡ€ΠΎΠ²Π½Π΅ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ Ρƒ вас Π±ΡƒΠ΄ΡƒΡ‚ массивы ΡƒΠ·Π»ΠΎΠ² ΠΈ массивы связСй. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ Π²Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ, ΠΊΠ°ΠΊ ΠΈΠΌΠ΅Π½Π½ΠΎ Π³Ρ€Π°Ρ„ рСализуСтся этими структурами программирования.

НуТно Π·Π°ΠΌΠ΅Ρ‚ΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ Π½ΠΈΡ‡Ρ‚ΠΎ ΠΈΠ· Π²Ρ‹ΡˆΠ΅ΡΠΊΠ°Π·Π°Π½Π½ΠΎΠ³ΠΎ Π½Π΅ относится ΠΊ самому процСссу написания ΠΊΠΎΠ΄Π°. Когда Π²Ρ‹ ΠΏΠΈΡˆΠ΅Ρ‚Π΅ ΠΊΠΎΠ΄, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ выполняСтС Ρ‚Ρ€Π΅Ρ‚ΠΈΠΉ шаг, Π²Π°ΠΌ Ρ‚ΠΎΠΆΠ΅ Π½ΡƒΠΆΠ½ΠΎ ΠΌΡ‹ΡΠ»ΠΈΡ‚ΡŒ ΠΈ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Ρ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ. Если ΠΏΠΎΠ΄Π·Π°Π΄Π°Ρ‡Π° оказываСтся слоТной ΠΈΠ»ΠΈ Π½Π΅ΠΎΡ‡Π΅Π²ΠΈΠ΄Π½ΠΎΠΉ, Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ для Π½Π΅Π΅ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ. Но ΠΎ самом ΠΊΠΎΠ΄Π΅ я здСсь Π½Π΅ Π³ΠΎΠ²ΠΎΡ€ΡŽ. Π’Ρ‹ ΠΌΠΎΠΆΠ΅Ρ‚Π΅ ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ Π»ΡŽΠ±Ρ‹ΠΌ языком программирования, любой ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ»ΠΎΠ³ΠΈΠ΅ΠΉ, Ρ€Π΅Ρ‡ΡŒ Π½Π΅ ΠΎ Π½ΠΈΡ…. ΠšΡ€ΠΎΠΌΠ΅ Ρ‚ΠΎΠ³ΠΎ, Π½ΠΈΡ‡Ρ‚ΠΎ ΠΈΠ· Π²Ρ‹ΡˆΠ΅ΡΠΊΠ°Π·Π°Π½Π½ΠΎΠ³ΠΎ Π½Π΅ избавляСт ΠΎΡ‚ нСобходимости Ρ‚Π΅ΡΡ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ ΠΈ ΠΎΡ‚Π»Π°ΠΆΠΈΠ²Π°Ρ‚ΡŒ ΠΊΠΎΠ΄. Π”Π°ΠΆΠ΅ Ссли абстрактная модСль написана Π²Π΅Ρ€Π½ΠΎ, Π² Π΅Π΅ Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ Π±Π°Π³ΠΈ.

НаписаниС спСцификаций β€” Π΄ΠΎΠΏΠΎΠ»Π½ΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹ΠΉ этап Π² процСссС написания ΠΊΠΎΠ΄Π°. Благодаря Π½Π΅ΠΌΡƒ ΠΌΠ½ΠΎΠ³ΠΈΠ΅ ошибки ΠΌΠΎΠΆΠ½ΠΎ ΠΎΡ‚Π»ΠΎΠ²ΠΈΡ‚ΡŒ мСньшими усилиями β€” ΠΌΡ‹ это Π·Π½Π°Π΅ΠΌ ΠΏΠΎ ΠΎΠΏΡ‹Ρ‚Ρƒ программистов ΠΈΠ· Amazon. Π‘ΠΎ спСцификациями качСство ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌ становится Π²Ρ‹ΡˆΠ΅. Π’Π°ΠΊ ΠΏΠΎΡ‡Π΅ΠΌΡƒ ΠΆΠ΅ Ρ‚ΠΎΠ³Π΄Π° ΠΌΡ‹ Ρ‚Π°ΠΊ часто обходимся Π±Π΅Π· Π½ΠΈΡ…? ΠŸΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ‚Ρ€ΡƒΠ΄Π½ΠΎ. А ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ‚Ρ€ΡƒΠ΄Π½ΠΎ, ΠΏΠΎΡ‚ΠΎΠΌΡƒ Ρ‡Ρ‚ΠΎ для этого Π½ΡƒΠΆΠ½ΠΎ Π΄ΡƒΠΌΠ°Ρ‚ΡŒ, Π° Π΄ΡƒΠΌΠ°Ρ‚ΡŒ Ρ‚ΠΎΠΆΠ΅ Ρ‚Ρ€ΡƒΠ΄Π½ΠΎ. ВсСгда ΠΏΡ€ΠΎΡ‰Π΅ Π΄Π΅Π»Π°Ρ‚ΡŒ Π²ΠΈΠ΄, Ρ‡Ρ‚ΠΎ Π΄ΡƒΠΌΠ°Π΅ΡˆΡŒ. Π—Π΄Π΅ΡΡŒ ΠΌΠΎΠΆΠ½ΠΎ провСсти аналогию с Π±Π΅Π³ΠΎΠΌ β€” Ρ‡Π΅ΠΌ мСньшС Π²Ρ‹ Π±Π΅Π³Π°Π΅Ρ‚Π΅, Ρ‚Π΅ΠΌ ΠΌΠ΅Π΄Π»Π΅Π½Π½Π΅Π΅ Π²Ρ‹ Π±Π΅ΠΆΠΈΡ‚Π΅. НуТно Ρ‚Ρ€Π΅Π½ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ свои мускулы ΠΈ ΡƒΠΏΡ€Π°ΠΆΠ½ΡΡ‚ΡŒΡΡ Π² письмС. НуТна ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ°.

БпСцификация ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ Π½Π΅Π²Π΅Ρ€Π½ΠΎΠΉ. Π’Ρ‹ ΠΌΠΎΠ³Π»ΠΈ Π³Π΄Π΅-Ρ‚ΠΎ ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ ΠΎΡˆΠΈΠ±ΠΊΡƒ, ΠΈΠ»ΠΈ ΠΌΠΎΠ³Π»ΠΈ ΠΈΠ·ΠΌΠ΅Π½ΠΈΡ‚ΡŒΡΡ трСбования, ΠΈΠ»ΠΈ оказалось Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡΠ΄Π΅Π»Π°Ρ‚ΡŒ ΡƒΠ»ΡƒΡ‡ΡˆΠ΅Π½ΠΈΠ΅. Π›ΡŽΠ±ΠΎΠΉ ΠΊΠΎΠ΄, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΌ ΠΊΡ‚ΠΎ-Π»ΠΈΠ±ΠΎ ΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅Ρ‚ΡΡ, приходится ΠΌΠ΅Π½ΡΡ‚ΡŒ, поэтому Ρ€Π°Π½ΠΎ ΠΈΠ»ΠΈ ΠΏΠΎΠ·Π΄Π½ΠΎ спСцификация пСрСстанСт ΡΠΎΠΎΡ‚Π²Π΅Ρ‚ΡΡ‚Π²ΠΎΠ²Π°Ρ‚ΡŒ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ΅. Π’ ΠΈΠ΄Π΅Π°Π»Π΅ Π² этом случаС Π½ΡƒΠΆΠ½ΠΎ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ Π½ΠΎΠ²ΡƒΡŽ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ ΠΈ ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ ΠΏΠ΅Ρ€Π΅ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠ΄. ΠœΡ‹ прСкрасно Π·Π½Π°Π΅ΠΌ, Ρ‡Ρ‚ΠΎ Ρ‚Π°ΠΊ Π½ΠΈΠΊΡ‚ΠΎ Π½Π΅ Π΄Π΅Π»Π°Π΅Ρ‚. На ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ΅ ΠΌΡ‹ ΠΏΠ°Ρ‚Ρ‡ΠΈΠΌ ΠΊΠΎΠ΄ ΠΈ, Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, обновляСм ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ. Если это ΠΎΠ±ΡΠ·Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ Ρ€Π°Π½ΠΎ ΠΈΠ»ΠΈ ΠΏΠΎΠ·Π΄Π½ΠΎ происходит, Ρ‚ΠΎ Π·Π°Ρ‡Π΅ΠΌ Π²ΠΎΠΎΠ±Ρ‰Π΅ ΠΏΠΈΡΠ°Ρ‚ΡŒ спСцификации? Π’ΠΎ-ΠΏΠ΅Ρ€Π²Ρ‹Ρ…, для Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊΠ°, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Π±ΡƒΠ΄Π΅Ρ‚ ΠΏΡ€Π°Π²ΠΈΡ‚ΡŒ ваш ΠΊΠΎΠ΄, ΠΊΠ°ΠΆΠ΄ΠΎΠ΅ лишнСС слово Π² спСцификации Π±ΡƒΠ΄Π΅Ρ‚ Π½Π° вСс Π·ΠΎΠ»ΠΎΡ‚Π°, ΠΈ этим Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊΠΎΠΌ Π²ΠΏΠΎΠ»Π½Π΅ ΠΌΠΎΠΆΠ΅Ρ‚Π΅ Π±Ρ‹Ρ‚ΡŒ Π²Ρ‹ сами. Π― часто Ρ€ΡƒΠ³Π°ΡŽ сСбя Π·Π° Π½Π΅Π΄ΠΎΡΡ‚Π°Ρ‚ΠΎΡ‡Π½ΡƒΡŽ ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ, ΠΊΠΎΠ³Π΄Π° ΠΏΡ€Π°Π²Π»ΡŽ свой ΠΊΠΎΠ΄. А я ΠΏΠΈΡˆΡƒ большС спСцификаций, Ρ‡Π΅ΠΌ ΠΊΠΎΠ΄Π°. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ, ΠΊΠΎΠ³Π΄Π° Π²Ρ‹ ΠΏΡ€Π°Π²ΠΈΡ‚Π΅ ΠΊΠΎΠ΄, ΡΠΏΠ΅Ρ†ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ всСгда Π½ΡƒΠΆΠ½ΠΎ ΠΎΠ±Π½ΠΎΠ²Π»ΡΡ‚ΡŒ. Π’ΠΎ-Π²Ρ‚ΠΎΡ€Ρ‹Ρ…, с ΠΊΠ°ΠΆΠ΄ΠΎΠΉ ΠΏΡ€Π°Π²ΠΊΠΎΠΉ ΠΊΠΎΠ΄ становится Ρ…ΡƒΠΆΠ΅, Π΅Π³ΠΎ становится всС Ρ‚Ρ€ΡƒΠ΄Π½Π΅Π΅ Ρ‡ΠΈΡ‚Π°Ρ‚ΡŒ ΠΈ ΠΏΠΎΠ΄Π΄Π΅Ρ€ΠΆΠΈΠ²Π°Ρ‚ΡŒ. Π­Ρ‚ΠΎ нарастаниС энтропии. Но Ссли Π²Ρ‹ Π½Π΅ Π½Π°Ρ‡ΠΈΠ½Π°Π΅Ρ‚Π΅ со спСцификации, Ρ‚ΠΎ каТдая написанная строка Π±ΡƒΠ΄Π΅Ρ‚ ΠΏΡ€Π°Π²ΠΊΠΎΠΉ, ΠΈ ΠΊΠΎΠ΄ с самого Π½Π°Ρ‡Π°Π»Π° Π±ΡƒΠ΄Π΅Ρ‚ Π³Ρ€ΠΎΠΌΠΎΠ·Π΄ΠΊΠΈΠΌ ΠΈ Ρ‚Ρ€ΡƒΠ΄Π½ΠΎΡ‡ΠΈΡ‚Π°Π΅ΠΌΡ‹ΠΌ.

Как Π³ΠΎΠ²ΠΎΡ€ΠΈΠ» Π­ΠΉΠ·Π΅Π½Ρ…Π°ΡƒΠ΅Ρ€, Π½ΠΈ ΠΎΠ΄Π½Π° Π±ΠΈΡ‚Π²Π° Π½Π΅ Π±Ρ‹Π»Π° Π²Ρ‹ΠΈΠ³Ρ€Π°Π½Π° ΠΏΠΎ ΠΏΠ»Π°Π½Ρƒ, ΠΈ Π½ΠΈ ΠΎΠ΄Π½Π° Π±ΠΈΡ‚Π²Π° Π½Π΅ Π±Ρ‹Π»Π° Π²Ρ‹ΠΈΠ³Ρ€Π°Π½Π° Π±Π΅Π· ΠΏΠ»Π°Π½Π°. А ΠΎΠ½ Π·Π½Π°Π» ΠΊΠΎΠ΅-Ρ‡Ρ‚ΠΎ ΠΎ Π±ΠΈΡ‚Π²Π°Ρ…. БущСствуСт ΠΌΠ½Π΅Π½ΠΈΠ΅, Ρ‡Ρ‚ΠΎ написаниС спСцификаций β€” пустая Ρ‚Ρ€Π°Ρ‚Π° Π²Ρ€Π΅ΠΌΠ΅Π½ΠΈ. Иногда это Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Ρ‚Π°ΠΊ, ΠΈ Π·Π°Π΄Π°Ρ‡Π° Π½Π°ΡΡ‚ΠΎΠ»ΡŒΠΊΠΎ проста, Ρ‡Ρ‚ΠΎ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Ρ‚ΡŒ Π΅Π΅ Π½Π΅Ρ‡Π΅Π³ΠΎ. Но всСгда Π½ΡƒΠΆΠ½ΠΎ ΠΏΠΎΠΌΠ½ΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ, ΠΊΠΎΠ³Π΄Π° Π²Π°ΠΌ ΡΠΎΠ²Π΅Ρ‚ΡƒΡŽΡ‚ Π½Π΅ ΠΏΠΈΡΠ°Ρ‚ΡŒ спСцификаций, это Π·Π½Π°Ρ‡ΠΈΡ‚, Ρ‡Ρ‚ΠΎ Π²Π°ΠΌ ΡΠΎΠ²Π΅Ρ‚ΡƒΡŽΡ‚ Π½Π΅ Π΄ΡƒΠΌΠ°Ρ‚ΡŒ. И ΠΎΠ± этом ΠΊΠ°ΠΆΠ΄Ρ‹ΠΉ Ρ€Π°Π· слСдуСт ΠΏΠΎΠ΄ΡƒΠΌΠ°Ρ‚ΡŒ. ΠŸΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Π½ΠΈΠ΅ Π·Π°Π΄Π°Ρ‡ΠΈ Π½Π΅ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΡƒΠ΅Ρ‚, Ρ‡Ρ‚ΠΎ Π²Ρ‹ Π½Π΅ ΡΠΎΠ²Π΅Ρ€ΡˆΠΈΡ‚Π΅ ошибок. Как ΠΌΡ‹ Π·Π½Π°Π΅ΠΌ, волшСбной ΠΏΠ°Π»ΠΎΡ‡ΠΊΠΈ Π½ΠΈΠΊΡ‚ΠΎ Π½Π΅ ΠΈΠ·ΠΎΠ±Ρ€Π΅Π», ΠΈ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ β€” слоТноС занятиС. Но Ссли Π²Ρ‹ Π½Π΅ ΠΏΡ€ΠΎΠ΄ΡƒΠΌΡ‹Π²Π°Π΅Ρ‚Π΅ Π·Π°Π΄Π°Ρ‡Ρƒ, Π²Ρ‹ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΠΎΠ²Π°Π½Π½ΠΎ сдСлаСтС ошибки.

ΠŸΠΎΠ΄Ρ€ΠΎΠ±Π½Π΅Π΅ ΠΏΡ€ΠΎ TLA+ ΠΈ PlusCal ΠΌΠΎΠΆΠ½ΠΎ ΠΏΠΎΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ Π½Π° ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎΠΌ сайтС, Ρ‚ΡƒΠ΄Π° ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΉΡ‚ΠΈ с ΠΌΠΎΠ΅ΠΉ домашнСй страницы ΠΏΠΎ ссылкС. На этом Ρƒ мСня всС, спасибо Π·Π° Π²Π½ΠΈΠΌΠ°Π½ΠΈΠ΅.

Напоминаю, Ρ‡Ρ‚ΠΎ это ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄. Когда Π²Ρ‹ Π±ΡƒΠ΄Π΅Ρ‚Π΅ ΠΏΠΈΡΠ°Ρ‚ΡŒ ΠΊΠΎΠΌΠΌΠ΅Π½Ρ‚Π°Ρ€ΠΈΠΈ β€” ΠΏΠΎΠΌΠ½ΠΈΡ‚Π΅, Ρ‡Ρ‚ΠΎ Π°Π²Ρ‚ΠΎΡ€ ΠΈΡ… Π½Π΅ ΠΏΡ€ΠΎΡ‡ΠΈΡ‚Π°Π΅Ρ‚. Если Π²Π°ΠΌ Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ хочСтся ΠΏΠΎΠΎΠ±Ρ‰Π°Ρ‚ΡŒΡΡ с Π°Π²Ρ‚ΠΎΡ€ΠΎΠΌ, Ρ‚ΠΎ ΠΎΠ½ Π±ΡƒΠ΄Π΅Ρ‚ Π½Π° ΠΊΠΎΠ½Ρ„Π΅Ρ€Π΅Π½Ρ†ΠΈΠΈ Hydra 2019, которая ΠΏΡ€ΠΎΠΉΠ΄Ρ‘Ρ‚ 11-12 июля 2019 Π³ΠΎΠ΄Π° Π² Π‘Π°Π½ΠΊΡ‚-ΠŸΠ΅Ρ‚Π΅Ρ€Π±ΡƒΡ€Π³Π΅. Π‘ΠΈΠ»Π΅Ρ‚Ρ‹ ΠΌΠΎΠΆΠ½ΠΎ приобрСсти Π½Π° ΠΎΡ„ΠΈΡ†ΠΈΠ°Π»ΡŒΠ½ΠΎΠΌ сайтС.

Π˜ΡΡ‚ΠΎΡ‡Π½ΠΈΠΊ: habr.com