Ин мақолаи тарҷума аст . Аммо пеш аз он, як муқаддимаи кӯтоҳ вуҷуд дорад. Зомбиҳо чӣ гуна ташаккул меёбанд? Ҳар касе худро дар вазъияте пайдо кардааст, ки мехоҳанд дӯст ё ҳамкорашро ба сатҳи худ расонанд, аммо ин натиҷа намедиҳад. Гузашта аз ин, на барои шумо, балки барои ӯ "ин кор намекунад": дар як тарафи тарозу музди муқаррарӣ, вазифаҳо ва ғайра ва аз тарафи дигар зарурати фикр кардан аст. Фикр кардан ногувор ва дардовар аст. Вай зуд таслим мешавад ва бидуни истифодаи майнаи худ ба навиштани код идома медиҳад. Шумо дарк мекунед, ки барои бартараф кардани монеаи нотавонӣ чӣ қадар заҳмат лозим аст ва шумо ин корро намекунед. Ҳамин тавр зомбиҳо ба вуҷуд меоянд, ки табобаташон имконпазир аст, аммо ба назар чунин мерасад, ки ҳеҷ кас ин корро намекунад.
Вакте ки ман инро дидам (бале, ҳамон дӯсти китобҳои дарсӣ) ва маъруза не, балки саволу чавоб медихад, андаке эхтиёт кардам. Дар ҳар сурат, Лесли як олими машҳури ҷаҳонӣ, муаллифи корҳои муҳим дар компютерҳои тақсимшуда аст ва шумо инчунин метавонед ӯро бо ҳарфҳои La дар 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, аммо он хатогиҳои изофаро пешгирӣ намекунад. Ин модели мураккабтареро талаб мекунад, ки барои он вақт нест.
Биёед дар бораи маҳдудиятҳои функсия ҳамчун модел сӯҳбат кунем. Баъзе барномаҳо (масалан, системаҳои оператсионӣ) на танҳо арзиши мушаххасро барои аргументҳои муайян бармегардонанд; онҳо метавонанд пайваста кор кунанд. Илова бар ин, функсия ҳамчун модел барои қадами дуюм: банақшагирии ҳалли мушкилот чандон мувофиқ нест. Сорти зуд ва ҳубобӣ як функсияро ҳисоб мекунанд, аммо онҳо алгоритмҳои тамоман гуногунанд. Аз ин рӯ, барои тавсифи роҳи расидан ба ҳадафи барнома ман модели дигарро истифода мебарам, биёед онро модели рафтори стандартӣ меномем. Барнома дар он ҳамчун маҷмӯи тамоми рафторҳои дуруст муаррифӣ карда мешавад, ки ҳар яки онҳо, дар навбати худ, пайдарпайии ҳолатҳо ва ҳолат таъини арзишҳо ба тағирёбандаҳо мебошад.
Биёед бубинем, ки қадами дуюми алгоритми Евклид чӣ гуна хоҳад буд. Мо бояд ҳисоб кунем 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:
Дар ҳолати аввал, қимати нави y ба қимати пешинаи 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 дар вебсайти махсус хонед, шумо метавонед аз саҳифаи хонагии ман ба он ҷо равед . Ин ҳама барои ман аст, ташаккур барои таваҷҷӯҳатон.
Лутфан дар хотир доред, ки ин тарҷума аст. Ҳангоми навиштани шарҳҳо, дар хотир доред, ки муаллиф онҳоро намехонад. Агар шумо дар ҳақиқат хоҳед, ки бо муаллиф сӯҳбат кунед, ӯ дар конфронси Hydra 2019, ки рӯзҳои 11-12 июли соли 2019 дар Санкт-Петербург баргузор мешавад, хоҳад буд. Билетхоро харидан мумкин аст .
Манбаъ: will.com