Бул котормо макаласы . Бирок ага чейин кыскача киришүү бар. Зомбилер кантип пайда болот? Ар бир адам досун же кесиптешин өз деңгээлине жеткирүүнү каалаган кырдаалга туш болду, бирок андан майнап чыкпайт. Анын үстүнө, "бул болбойт" эмес, анчалык сиз үчүн, бирок ал үчүн: шкала бир жагында нормалдуу эмгек акы, милдеттери, ж.б. Ой жүгүртүү жагымсыз жана азаптуу. Ал бат эле баш тартып, мээсин такыр колдонбостон код жазууну улантат. Үйрөнгөн алсыздыктын тосмосун жеңүү үчүн канчалык күч-аракет талап кылынарын түшүнөсүз жана аны жөн эле кылбайсыз. Мына ошентип зомбилер пайда болот, аларды айыктырса болот, бирок муну эч ким кылбайт окшойт.
Мен муну көргөндө (ооба, окуу китептериндеги ошол эле дос) жана доклад эмес, суроо-жооп иретинде жүрүп жатат, мен бир аз сак болдум. Кандай болгон күндө да, Лесли дүйнөгө таанымал окумуштуу, бөлүштүрүлгөн эсептөөлөр боюнча негизги эмгектердин автору жана сиз аны LaTeX - “Lamport TeX” тамгаларынан да билесиз. Экинчи кооптуу жагдай - анын талабы: келген ар бир адам (толугу менен акысыз) анын бир-эки отчетун алдын ала угуп, алар боюнча жок дегенде бир суроо менен чыгып, андан кийин гана келиши керек. Мен Лампорттун ал жерде эмне уктурууларын көрүүнү чечтим - бул эң сонун! Бул так ошол нерсе, зомбилерди дарылоо үчүн сыйкырдуу шилтеме-таблетка. Мен сизге эскертем: текст супер ийкемдүү методологияларды жакшы көргөндөрдү жана жазгандарын сынап көрүүнү жактырбагандарды катуу күйгүзүшү мүмкүн.
Хаброкаттан кийин семинардын котормосу иш жүзүндө башталат. Окуудан ырахат алыңыз!
Кандай гана ишти аткарбаңыз, сиз ар дайым үч кадамдан өтүшүңүз керек:
- кандай максатка жетүүнү каалап жатканыңызды чечиңиз;
- максатыңызга кантип жетээриңизди чечиңиз;
- максатыңа жет.
Бул программалоого да тиешелүү. Код жазганда, бизге керек:
- программа так эмне кылышы керектигин чечет;
- ал өз милдетин так кантип аткаруу керек экенин аныктоо;
- тиешелүү кодду жаз.
Акыркы кадам, албетте, абдан маанилүү, бирок мен бүгүн бул тууралуу сөз кылбайм. Анын ордуна биз биринчи экөөнү талкуулайбыз. Ар бир программист ишке киришер алдында аларды аткарат. Эмне жазып жатканыңызды чечмейинче, жазуу үчүн отурбайсыз: браузер же маалымат базасы. Максаттын белгилүү бир идеясы болушу керек. Жана сиз сөзсүз түрдө программа эмне кыла тургандыгы жөнүндө ойлонуңуз жана коддун өзү кандайдыр бир жол менен браузерге айланат деген үмүт менен аны туш келди жазбаңыз.
Бул кодду алдын ала ойлонуу так кантип ишке ашат? Буга канча күч жумшашыбыз керек? Мунун баары биз чечип жаткан маселе канчалык татаал экендигине байланыштуу. Келгиле, биз каталарга чыдамдуу бөлүштүрүлгөн системаны жазгыбыз келет дейли. Бул учурда, биз кодго отурардан мурун жакшылап ойлонушубуз керек. Эгерде биз жөн гана бүтүн өзгөрмө 1ге көбөйтүү керек болсочу? Бир караганда, бул жерде баары тривиалдуу жана эч кандай ой талап кылынбайт, бирок андан кийин биз толуп кетиши мүмкүн экенин эстейбиз. Ошондуктан, маселенин жөнөкөй же татаал экенин түшүнүү үчүн да, алгач ойлонуу керек.
Эгер көйгөйдү чечүүнүн жолдорун алдын ала ойлонсоңуз, каталардан качсаңыз болот. Бирок бул сиздин ой жүгүртүүңүздүн так болушун талап кылат. Буга жетүү үчүн өз оюңузду жазуу керек. Мага Дик Гиндондун: "Сиз жазганыңызда табият сиздин ой жүгүртүүңүздүн канчалык шалаакы экениңизди көрсөтөт" деген сөзүн жакшы көрөм. Жазбасаңыз, сиз ойлонуп жатам деп ойлойсуз. Ал эми спецификация түрүндө оюңузду жазышыңыз керек.
Өзгөчөлүктөр көп функцияларды аткарат, айрыкча ири долбоорлордо. Бирок мен алардын бирөө жөнүндө гана айта кетейин: алар бизге так ойлонууга жардам берет. Ой жүгүртүү абдан маанилүү жана абдан кыйын, ошондуктан бул жерде кандайдыр бир жардам керек. Техникалык шарттарды кайсы тилде жазышыбыз керек? Дегеле, бул программисттер үчүн ар дайым биринчи суроо: биз кайсы тилде жазабыз? Эч бир туура жооп жок: биз чечкен көйгөйлөр өтө ар түрдүү. Кээ бир адамдар үчүн TLA+ бул мен иштеп чыккан спецификация тили. Башкалар үчүн кытай тилин колдонуу ыңгайлуу. Мунун баары кырдаалга жараша болот.
Маанилүү суроо: кантип биз так ой жүгүртүүгө жетише алабыз? Жооп: Биз окумуштуулардай ойлонушубуз керек. Бул акыркы 500 жылда жакшы иштеген ой жүгүртүү ыкмасы. Илимде биз чындыктын математикалык моделдерин курабыз. Астрономия, балким, сөздүн так маанисинде биринчи илим болгон. Астрономияда колдонулган математикалык моделде асман телолору массасы, абалы жана импульсу бар чекиттер катары көрүнөт, бирок чындыгында алар тоолор жана океандар, агымдары жана агымдары бар өтө татаал объектилер. Бул модель, башка сыяктуу эле, белгилүү бир маселелерди чечүү үчүн түзүлгөн. Эгер сиз планетаны тапкыңыз келсе, телескопту кайда багыттоо керектигин аныктоо үчүн абдан жакшы. Бирок бул планетадагы аба ырайын алдын ала айткыңыз келсе, бул модель иштебейт.
Математика моделдин касиеттерин аныктоого мүмкүндүк берет. Жана бул касиеттердин чындыкка кандай тиешеси бар экенин илим көрсөтөт. Биздин илим, информатика жөнүндө сүйлөшөлү. Биз иштеп жаткан чындык – бул бардык түрдөгү эсептөө системалары: процессорлор, оюн консолдору, программаларды иштеткен компьютерлер жана башкалар. Мен программаны компьютерде аткаруу жөнүндө сөз кылам, бирок, жалпысынан, бул корутундулардын бардыгы ар кандай эсептөө системасына тиешелүү. Биздин илимде биз көптөгөн ар кандай моделдерди колдонобуз: Тьюринг машинасы, окуялардын жарым-жартылай иреттелген топтому жана башкалар.
Программа кандай? Бул өз алдынча каралышы мүмкүн болгон ар кандай код. Биз браузер жазуу керек дейли. Биз үч тапшырманы аткарабыз: колдонуучунун программанын презентациясын долбоорлойбуз, андан кийин программанын жогорку деңгээлдеги диаграммасын жазабыз жана акырында кодду жазабыз. Биз кодду жазып жатканда, биз текст форматтоочу жазуу керек экенин түшүнөбүз. Бул жерде дагы үч маселени чечишибиз керек: бул курал кайсы текстти кайтарып берерин аныктоо; форматтоо үчүн алгоритмди тандоо; код жаз. Бул тапшырманын өзүнүн кошумча милдети бар: сөздөргө дефистерди туура коюу. Ошондой эле биз бул көмөкчү тапшырманы үч кадам менен чечебиз – көрүп тургандай, алар көп деңгээлде кайталанат.
Келгиле, биринчи кадамды кененирээк карап көрөлү: программа кандай маселени чечет. Бул жерде биз көбүнчө программаны кандайдыр бир киргизүүнү алып, бир аз чыгарууну берген функция катары моделдейбиз. Математикада функция адатта жуптардын иреттелген жыйындысы катары сүрөттөлөт. Мисалы, натурал сандар үчүн квадраттоо функциясы {<0,0>, <1,1>, <2,4>, <3,9>, …} көптүгү катары сүрөттөлөт. Мындай функциянын аныктама областы ар бир жуптун биринчи элементтеринин жыйындысы, башкача айтканда натурал сандар. Функцияны аныктоо үчүн анын доменин жана формуласын көрсөтүшүбүз керек.
Бирок математикадагы функциялар программалоо тилдериндеги функциялар менен бирдей эмес. Математика алда канча жөнөкөй. Татаал мисалдарга убактым жок болгондуктан, жөнөкөйсүн карап көрөлү: C тилиндеги функцияны же Javaдагы эки бүтүн сандын эң чоң жалпы бөлүүчүсүн кайтарган статикалык методду. Бул ыкманын спецификациясында биз жазабыз: эсептейт GCD(M,N) аргументтер үчүн M и Nкайда GCD(M,N) - функция, анын домени бүтүн сандардын жуптарынын жыйындысы, ал эми кайтарылган мааниси төмөнкүгө бөлүнгөн эң чоң бүтүн сан болуп саналат. M и N. Бул модель менен реалдуулук кандайча салыштырылат? Модель бүтүн сандар менен иштейт жана C же Java тилдеринде бизде 32-бит бар int. Бул модель алгоритмдин туура экендигин чечүүгө мүмкүнчүлүк берет GCD, бирок бул ашыкча каталардын алдын албайт. Бул үчүн убакыт жок, бир кыйла татаал моделди талап кылат.
Модел катары функциянын чектөөлөрү жөнүндө сүйлөшөлү. Кээ бир программалар (мисалы, операциялык системалар) белгилүү бир аргументтер үчүн белгилүү бир маанини гана кайтарып бербейт, алар тынымсыз иштей алышат. Мындан тышкары, модель катары функция экинчи кадамга начар ылайыктуу: маселени кантип чечүүнү пландаштыруу. Quicksort жана көбүктүү сорттоо бир эле функцияны эсептешет, бирок алар такыр башка алгоритмдер. Ошондуктан, программанын максатына жетүү жолун сүрөттөө үчүн мен башка моделди колдоном, аны стандарттык жүрүм-турум модели деп атайлы. Программа анда бардык жарактуу жүрүм-турумдардын жыйындысы катары көрсөтүлөт, алардын ар бири өз кезегинде абалдардын ырааттуулугу, ал эми абал өзгөрмөлөргө маанилердин ыйгарылышы болуп саналат.
Келгиле, Евклиддик алгоритмдин экинчи кадамы кандай болорун карап көрөлү. Биз эсептешибиз керек 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? Нөл бардык сандарга бөлүнөт, ошондуктан бул учурда эң чоң бөлүүчү жок. Бул жагдайда, биз биринчи кадамга кайтып барып, суроо керек: биз чындап эле оң эмес сандар үчүн GCD эсептөө керекпи? Бул зарыл эмес болсо, анда жөн гана спецификацияны өзгөртүү керек.
Бул жерде өндүрүмдүүлүккө кыскача токтоло кетели. Ал көп учурда күнүнө жазылган код саптарынын саны менен ченелет. Бирок сизде мүчүлүштүктөр үчүн орун аз болгондуктан, белгилүү бир сандагы саптардан арылсаңыз, ишиңиз алда канча пайдалуу. Ал эми коддон кутулуунун эң оңой жолу - биринчи кадамда. Сиз ишке ашырууга аракет кылып жаткан бардык коңгуроолордун жана ышкырыктардын кереги жок болушу мүмкүн. Программаны жөнөкөйлөштүрүүнүн жана убакытты үнөмдөөнүн эң тез жолу – бул кылбаш керек болгон нерселерди кылбоо. Экинчи кадам убакытты үнөмдөө боюнча экинчи этапка ээ. Эгерде сиз өндүрүмдүүлүктү жазылган саптар менен өлчөгөн болсоңуз, анда тапшырманы кантип бүтүрүү жөнүндө ойлоносуз аз өндүрүмдүү, анткени сиз бир эле маселени азыраак код менен чече аласыз. Мен бул жерде так статистиканы бере албайм, анткени мен спецификацияга, башкача айтканда, биринчи жана экинчи кадамдарга кеткен убакыттан улам жазбаган саптардын санын санай албайм. Жана биз бул жерде да эксперимент жасай албайбыз, анткени экспериментте биринчи кадамды бүтүрүүгө укугубуз жок, тапшырма алдын ала аныкталат.
Расмий эмес мүнөздөмөлөрдөгү көптөгөн кыйынчылыктарга көз жумуп коюу оңой. Функциялар үчүн катуу спецификацияларды жазууда кыйын эч нерсе жок, мен муну талкуулабайм. Анын ордуна, биз стандарттуу жүрүм-турум үчүн күчтүү спецификацияларды жазуу жөнүндө сүйлөшөбүз. Коопсуздук касиетин колдонуу менен жүрүм-турумдун ар кандай жыйындысын сүрөттөөгө болот деген теорема бар (коопсуздук) жана аман калуу касиеттери (жандуу). Коопсуздук эч кандай жаман нерсе болбойт дегенди билдирет, программа туура эмес жооп бербейт. Аман калуу эртеби-кечпи жакшы нерсе болоорун билдирет, б.а. программа эртеби-кечпи туура жооп берет. Эреже катары, коопсуздук маанилүү көрсөткүч болуп саналат, каталар көбүнчө бул жерде пайда болот. Ошондуктан, убакытты үнөмдөө үчүн, мен аман калуу жөнүндө сөз кылбайм, бирок бул, албетте, маанилүү.
Биз коопсуздукка адегенде мүмкүн болгон баштапкы абалдардын топтомун көрсөтүү менен жетишебиз. Экинчиден, ар бир мамлекет үчүн бардык мүмкүн болгон кийинки мамлекеттер менен мамилелер. Келгиле, окумуштуулардай болуп, абалдарды математикалык түрдө аныктайлы. Баштапкы абалдардын жыйындысы формула менен сүрөттөлөт, мисалы, Евклиддик алгоритмде: (x = M) ∧ (y = N). Кээ бир баалуулуктар үчүн M и N бир гана баштапкы абал бар. Кийинки абал менен болгон байланыш формула менен сүрөттөлөт, анда кийинки абалдын өзгөрмөлөрү жай сан менен, ал эми учурдагы абалдын өзгөрмөлөрү жайсыз жазылат. Евклиддик алгоритмде биз эки формуланын дизъюнкциясы менен алектенебиз, алардын биринде x эң чоң маани, ал эми экинчисинде - y:
Биринчи учурда у-нун жаңы мааниси у-нун мурунку маанисине барабар болот жана биз чоңураак өзгөрмөнүн кичинесинен кемитүү менен х-тын жаңы маанисин алабыз. Экинчи учурда биз тескерисин жасайбыз.
Евклиддик алгоритмге кайрылып көрөлү. Дагы ушундай дейли 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] туюнтумдун эки бөлүгү тең жалган болот, ошондуктан анын кийинки абалы болбойт. Ошентип, бизде экинчи кадамдын толук спецификациясы бар - көрүп тургандай, бул инженерлер менен илимпоздор сыяктуу жөнөкөй математика жана информатикадагыдай таң калыштуу эмес.
Бул эки формуланы убактылуу логиканын бир формуласына бириктирсе болот. Бул жарашыктуу жана түшүндүрүү оңой, бирок ага азыр убакыт жок. Бизге убактылуу логика жашоонун касиети үчүн гана керек болушу мүмкүн, ал эми коопсуздук үчүн бул керек эмес. Мага убактылуу логика жакпайт, бул жөнөкөй математика эмес, бирок тирүүлүк үчүн бул зарыл жамандык.
Ар бир маани үчүн Евклиддик алгоритмде x и y уникалдуу баалуулуктар бар x' и y', бул кийинки абал менен болгон мамилени туура кылат. Башка сөз менен айтканда, Евклиддик алгоритм детерминистикалык болуп саналат. Детерминисттик эмес алгоритмди моделдөө үчүн, учурдагы абал бир нече мүмкүн болуучу келечектеги абалга ээ болушу керек, ал эми башталбаган өзгөрмөнүн ар бир мааниси кийинки абалга болгон мамиле чын болушу үчүн, баштапкы өзгөрмөнүн бир нече маанилерине ээ болушу керек. Бул кыйын эмес, бирок мен азыр мисал келтирбейм.
Жумушчу куралды жасоо үчүн сизге формалдуу математика керек. Кантип спецификацияны расмий кылуу керек? Бул үчүн бизге расмий тил керек болот, мис. . Бул тилде Евклид алгоритминин спецификациясы төмөнкүдөй болот:
Үч бурчтук менен бирдей белгинин символу белгинин сол тарабындагы маани белгинин оң жагындагы мааниге барабар экендигин аныктайт. Негизи спецификация бул аныктама, биздин учурда эки аныктама. TLA+ спецификациясына жогорудагы слайддагыдай эле декларацияларды жана кээ бир синтаксистерди кошуу керек. ASCIIде бул төмөнкүдөй болот:
Көрүнүп тургандай, татаал эч нерсе жок. TLA+ боюнча спецификацияны текшерүүгө болот, б.а., кичинекей моделдеги бардык мүмкүн болгон жүрүм-турумду айланып өтүүгө болот. Биздин учурда, бул модель белгилүү бир баалуулуктар болот M и N. Бул толугу менен автоматтык түрдө өтө натыйжалуу жана жөнөкөй текшерүү ыкмасы болуп саналат. Мындан тышкары, чындыктын расмий далилдерин жазып, аларды механикалык түрдө текшерүүгө болот, бирок бул көп убакытты талап кылат, андыктан муну дээрлик эч ким жасабайт.
TLA+тин негизги кемчилиги – бул математика, ал эми программисттер жана компьютердик илимпоздор математикадан коркушат. Бир караганда бул тамаша сыяктуу сезилет, бирок, тилекке каршы, мен муну олуттуу түрдө айтып жатам. Менин бир кесиптешим бир нече иштеп чыгуучуларга TLA+ кантип түшүндүрүүгө аракет кылганын айтып берди. Экранда формулалар пайда болоору менен көздөрү дароо айнектей болуп калды. Демек, TLA+ коркунучтуу болсо, колдоно аласыз , оюнчук программалоо тилинин бир түрү. PlusCalдагы туюнтма ар кандай TLA+ туюнтмасы болушу мүмкүн, башкача айтканда, ар кандай математикалык туюнтма. Кошумча, PlusCal детерминисттик эмес алгоритмдердин синтаксисине ээ. PlusCal каалаган TLA+ туюнтмаларын жаза алгандыктан, ал ар кандай реалдуу программалоо тилине караганда бир кыйла экспрессивдүү. Андан кийин, PlusCal окууга оңой TLA+ спецификациясына түзүлөт. Бул, албетте, татаал PlusCal спецификациясы TLA+ боюнча жөнөкөй спецификацияга айланат дегенди билдирбейт - жөн гана алардын ортосундагы кат алышуу ачык болсо, эч кандай кошумча татаалдык пайда болбойт. Акыр-аягы, бул спецификацияны TLA+ куралдары менен текшерсе болот. Жалпысынан алганда, PlusCal математика фобиясын жеңүүгө жардам берет; аны программисттер жана компьютер илимпоздору үчүн да түшүнүү оңой. Мен буга чейин бир нече убакытка (болжол менен 10 жыл) алгоритмдерди жарыяладым.
Балким, кимдир бирөө TLA+ жана PlusCal математика экенине каршы чыгар, ал эми математика ойдон чыгарылган мисалдар менен гана иштейт. Практикада түрлөрү, процедуралары, объекттери жана башкалар бар чыныгы тил керек. Бул андай эмес. Бул жерде Amazonда иштеген Крис Ньюкомб мындай деп жазат: «Биз TLA+ти он ири долбоордо колдондук жана ар бир учурда аны колдонуу өнүгүүгө олуттуу өзгөрүү жаратты, анткени биз коркунучтуу мүчүлүштүктөрдү өндүрүшкө чыга электе кармап алдык жана ал бизге агрессивдүү болуу үчүн керектүү түшүнүк жана ишенимди берди. программанын чындыгына таасир этпестен аткарууну оптималдаштыруу". Сиз көп уга аласыз формалдуу ыкмаларды колдонууда биз натыйжасыз кодду алабыз - иш жүзүндө баары тескерисинче. Мындан тышкары, программисттер алардын пайдалуулугуна ынанган күндө да, формалдуу методдордун зарылдыгына менеджерлерди ынандыра албайт деген түшүнүк бар. Жана Ньюкомб мындай деп жазат: "Менеджерлер азыр TLA+ спецификацияларын жазуу үчүн бардык мүмкүн болгон аракеттерди жасап жатышат жана бул үчүн атайын убакыт бөлүп жатышат". Ошентип, менеджерлер TLA+ иштеп жатканын көргөндө, алар аны кабыл алышат. Крис Ньюкомб муну алты ай мурун (2014-жылдын октябрында) жазган, бирок азыр менин билишимче, TLA+ 14 эмес, 10 долбоордо колдонулат. Дагы бир мисал XBox 360 дизайнына тиешелүү. Чарльз Такерге интерн келип, эс тутумунун спецификациясын жазган. Бул спецификациянын аркасында ката табылды, ал антпесе табылбай кала турган жана ар бир XBox 360 төрт сааттык колдонуудан кийин кыйроого алып келет. IBM инженерлери алардын тесттери бул мүчүлүштүктөрдү аныктай албастыгын ырасташты.
Сиз Интернеттен TLA+ жөнүндө көбүрөөк окуй аласыз, бирок азыр расмий эмес мүнөздөмөлөр жөнүндө сүйлөшөлү. Эң аз жалпы бөлүүчүнү жана ушул сыяктууларды эсептеген программаларды сейрек жазууга туура келет. Биз көбүнчө мен 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 жөнүндө көбүрөөк маалыматты атайын веб-сайттан окуй аласыз, менин үй баракчамдан ал жакка барсаңыз болот . Мунун баары мен үчүн, көңүл бурганыңыз үчүн рахмат.
Бул котормо экенин унутпаңыз. Комментарий жазганда автор окубай турганын унутпаңыз. Эгер сиз чындап эле автор менен баарлашууну кааласаңыз, ал 2019-жылдын 11-12-июлунда Санкт-Петербург шаарында өтө турган Hydra 2019 конференциясында болот. Билеттерди сатып алса болот .
Source: www.habr.com