Энэ бол орчуулгын нийтлэл юм . Гэхдээ үүнээс өмнө товч танилцуулга байна. Зомби хэрхэн үүсдэг вэ? Хүн бүр найз нөхөд, хамт ажиллагсдаа өөрсдийн түвшинд хүргэхийг хүсч буй нөхцөл байдалд орсон боловч энэ нь бүтдэггүй. Түүгээр ч барахгүй, "энэ нь бүтэхгүй" нь таны хувьд биш, харин түүний хувьд: жингийн нэг талд ердийн цалин, даалгавар гэх мэт, нөгөө талд нь бодох хэрэгтэй. Бодох нь тааламжгүй, өвдөлттэй байдаг. Тэр хурдан бууж өгч, тархиа огт ашиглахгүйгээр код бичсээр байна. Та сурсан арчаагүй байдлын саад бэрхшээлийг даван туулахын тулд хичнээн их хүчин чармайлт гаргадгийг ухаарч, үүнийг хийдэггүй. Ингэж л зомби үүсдэг бөгөөд үүнийг эмчлэх боломжтой мэт боловч хэн ч үүнийг хийхгүй байх шиг байна.
Би үүнийг хараад (Тийм ээ, сурах бичгүүдийн ижил найз) илтгэл биш асуулт хариултын хэлбэрээр явж байгаа тул би бага зэрэг болгоомжилсон. Лесли бол дэлхийд алдартай эрдэмтэн, тархсан тооцооллын чиглэлээр тууштай бүтээл туурвисан хүн бөгөөд та түүнийг 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 болон bubble sort нь ижил функцийг тооцоолох боловч тэдгээр нь огт өөр алгоритмууд юм. Тиймээс, хөтөлбөрийн зорилгод хүрэх арга замыг тодорхойлохын тулд би өөр загварыг ашигладаг, үүнийг стандарт зан үйлийн загвар гэж нэрлэе. Хөтөлбөр нь бүх хүчин төгөлдөр зан үйлийн багц хэлбэрээр илэрхийлэгддэг бөгөөд тэдгээр нь тус бүр нь төлөв байдлын дараалал бөгөөд төлөв нь хувьсагчид утгын хуваарилалт юм.
Евклидийн алгоритмын хоёр дахь алхам ямар байхыг харцгаая. Бид тооцоолох хэрэгтэй 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-ийн шинэ утга нь өмнөх у-ийн утгатай тэнцүү байх ба том хувьсагчаас жижиг хувьсагчийг хасснаар бид 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] илэрхийллийн хоёр хэсэг нь худал байх тул дараагийн төлөв байхгүй. Тиймээс, бид хоёр дахь алхамын бүрэн тодорхойлолттой байна - бидний харж байгаагаар энэ бол инженер, эрдэмтдийн адил энгийн математик бөгөөд компьютерийн шинжлэх ухаан шиг хачирхалтай биш юм.
Эдгээр хоёр томъёог цаг хугацааны логикийн нэг томъёонд нэгтгэж болно. Энэ нь дэгжин бөгөөд тайлбарлахад хялбар боловч одоо үүнийг хийх цаг алга. Бидэнд түр зуурын логик нь зөвхөн амьдралын шинж чанарт хэрэгтэй байж болох ч аюулгүй байдлын хувьд энэ нь шаардлагагүй юм. Би түр зуурын логикт дургүй, энэ нь тийм ч энгийн математик биш, харин амьд байдлын хувьд энэ нь зайлшгүй муу зүйл юм.
Утга бүрийн хувьд Евклидийн алгоритмд 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 оны 14-р сар) бичсэн боловч одоо миний мэдэж байгаагаар TLA+ нь 10 биш 360 төсөлд ашиглагдаж байна. Өөр нэг жишээ нь XBox 360-ийн дизайнтай холбоотой. Дадлагажигч Чарльз Такер дээр ирж, санах ойн системийн тодорхойлолтыг бичсэн. Энэхүү техникийн үзүүлэлтийн ачаар илрүүлдэггүй байсан алдаа олдсон бөгөөд XBox XNUMX бүр дөрвөн цаг ашигласны дараа гацах болно. 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-2019-нд Санкт-Петербургт болох Hydra XNUMX чуулганд оролцох болно. Тасалбар худалдаж авах боломжтой .
Эх сурвалж: www.habr.com