ការសរសេរកម្មវិធីគឺច្រើនជាងការសរសេរកូដ

នេះជាអត្ថបទបកប្រែ សិក្ខាសាលា Stanford. ប៉ុន្តែមុននោះមានការណែនាំខ្លីៗ។ តើ zombies ត្រូវបានបង្កើតឡើងយ៉ាងដូចម្តេច? មនុស្សគ្រប់រូបបានរកឃើញខ្លួនឯងនៅក្នុងស្ថានភាពដែលពួកគេចង់នាំមិត្តភ័ក្តិ ឬមិត្តរួមការងាររហូតដល់កម្រិតរបស់ពួកគេ ប៉ុន្តែវាមិនដំណើរការទេ។ លើសពីនេះទៅទៀត "វាមិនដំណើរការទេ" មិនច្រើនសម្រាប់អ្នកទេប៉ុន្តែសម្រាប់គាត់: នៅផ្នែកម្ខាងនៃមាត្រដ្ឋានមានប្រាក់ខែធម្មតាភារកិច្ចនិងអ្វីៗផ្សេងទៀតហើយម្ខាងទៀតគឺត្រូវគិត។ ការគិតគឺជាការមិនសប្បាយចិត្ត និងឈឺចាប់។ គាត់បោះបង់ចោលយ៉ាងឆាប់រហ័ស ហើយបន្តសរសេរកូដដោយមិនប្រើខួរក្បាលទាល់តែសោះ។ អ្នក​ដឹង​ថា​វា​ត្រូវ​ការ​ការ​ខិត​ខំ​ប៉ុន្មាន​ដើម្បី​ជម្នះ​ឧបសគ្គ​នៃ​ភាព​អស់​សង្ឃឹម ហើយ​អ្នក​មិន​ធ្វើ​វា​ទេ។ នេះជារបៀបដែល zombies ត្រូវបានបង្កើតឡើង ដែលហាក់ដូចជាអាចព្យាបាលបាន ប៉ុន្តែវាហាក់ដូចជាគ្មាននរណាម្នាក់នឹងធ្វើបែបនេះទេ។

នៅពេលដែលខ្ញុំបានឃើញនោះ។ Leslie Lamport (បាទ មិត្តដូចគ្នានោះមកពីសៀវភៅសិក្សា) មកដល់ប្រទេសរុស្ស៊ី ហើយ​មិន​បាន​ផ្តល់​របាយការណ៍​ទេ ប៉ុន្តែ​ជា​វគ្គ​សំណួរ​និង​ចម្លើយ ខ្ញុំ​មាន​ការ​ប្រុង​ប្រយ័ត្ន​បន្តិច។ ជាក់ស្តែង Leslie គឺជាអ្នកវិទ្យាសាស្ត្រដ៏ល្បីលើពិភពលោក ដែលជាអ្នកនិពន្ធនៃការងារបង្រៀនក្នុងការគណនាចែកចាយ ហើយអ្នកក៏អាចស្គាល់គាត់តាមរយៈអក្សរ La in LaTeX - "Lamport TeX" ។ កត្តាប្រកាសអាសន្នទីពីរគឺតម្រូវការរបស់គាត់៖ អ្នកគ្រប់គ្នាដែលមកត្រូវតែ (មិនគិតថ្លៃទាំងស្រុង) ស្តាប់របាយការណ៍របស់គាត់ពីរបីជាមុន មកជាមួយសំណួរយ៉ាងហោចណាស់មួយអំពីពួកគេ ហើយបន្ទាប់មកមក។ ខ្ញុំបានសម្រេចចិត្តមើលអ្វីដែល Lamport កំពុងចាក់ផ្សាយនៅទីនោះ ហើយវាពិតជាអស្ចារ្យណាស់! នេះពិតជារឿងនោះ ដែលជាថ្នាំគ្រាប់វេទមន្តសម្រាប់ព្យាបាល zombies ។ ខ្ញុំ​ព្រមាន​អ្នក៖ អត្ថបទ​អាច​នឹង​ឆេះ​ខ្លាំង​ដល់​អ្នក​ដែល​ចូលចិត្ត​វិធីសាស្ត្រ​រហ័សរហួន ហើយ​អ្នក​ដែល​មិន​ចូលចិត្ត​សាកល្បង​អ្វី​ដែល​ពួកគេ​បាន​សរសេរ។

បន្ទាប់ពី habrokat ការបកប្រែនៃសិក្ខាសាលាពិតជាចាប់ផ្តើម។ សូមរីករាយអាន!

មិនថាអ្នកធ្វើកិច្ចការអ្វីក៏ដោយ អ្នកតែងតែត្រូវឆ្លងកាត់បីជំហាន៖

• សម្រេចចិត្តថាតើគោលដៅអ្វីដែលអ្នកចង់សម្រេចបាន;
• សម្រេចចិត្តថាតើអ្នកនឹងសម្រេចបានគោលដៅរបស់អ្នកដោយរបៀបណា?
• ឈានដល់គោលដៅរបស់អ្នក។

នេះក៏អនុវត្តចំពោះការសរសេរកម្មវិធីផងដែរ។ នៅពេលយើងសរសេរកូដ យើងត្រូវការ៖

• សម្រេចចិត្តថាតើកម្មវិធីគួរធ្វើអ្វី
• កំណត់ឱ្យច្បាស់អំពីរបៀបដែលវាគួរតែអនុវត្តភារកិច្ចរបស់ខ្លួន;
• សរសេរកូដសមរម្យ។

ជំហានចុងក្រោយគឺសំខាន់ណាស់ ប៉ុន្តែខ្ញុំនឹងមិននិយាយអំពីវានៅថ្ងៃនេះទេ។ ផ្ទុយទៅវិញ យើងនឹងពិភាក្សាពីរដំបូង។ អ្នកសរសេរកម្មវិធីគ្រប់រូបអនុវត្តវាមុនពេលចាប់ផ្តើមធ្វើការ។ អ្នក​មិន​អង្គុយ​សរសេរ​ទេ លុះត្រាតែ​អ្នក​សម្រេច​ចិត្ត​ថា​អ្នក​កំពុង​សរសេរ​អ្វី៖ កម្មវិធីរុករកតាមអ៊ីនធឺណិត ឬ​មូលដ្ឋានទិន្នន័យ។ គំនិតជាក់លាក់នៃគោលដៅត្រូវតែមានវត្តមាន។ ហើយ​អ្នក​ប្រាកដ​ជា​គិត​អំពី​អ្វី​ដែល​កម្មវិធី​នឹង​ធ្វើ ហើយ​កុំ​សរសេរ​វា​ដោយ​អចេតនា​ដោយ​សង្ឃឹម​ថា​កូដ​ខ្លួន​ឯង​នឹង​ក្លាយ​ទៅ​ជា​កម្មវិធីរុករក​តាម​អ៊ីនធឺណិត។

តើ​ការ​គិត​ទុក​មុន​អំពី​កូដ​នេះ​កើត​ឡើង​យ៉ាង​ណា? តើ​យើង​គួរ​ប្រឹងប្រែង​ប៉ុណ្ណា​ក្នុង​រឿង​នេះ? វាទាំងអស់គឺអាស្រ័យលើថាតើយើងដោះស្រាយបញ្ហាស្មុគស្មាញប៉ុណ្ណា។ ចូរនិយាយថាយើងចង់សរសេរប្រព័ន្ធចែកចាយដែលមានកំហុស។ ក្នុង​ករណី​នេះ យើង​គួរ​គិត​ឲ្យ​បាន​ហ្មត់ចត់ មុន​នឹង​អង្គុយ​សរសេរ​កូដ។ ចុះបើយើងគ្រាន់តែត្រូវការបង្កើនអថេរចំនួនគត់ដោយ 1? នៅ glance ដំបូង អ្វីគ្រប់យ៉ាងនៅទីនេះគឺតូចតាច ហើយមិនចាំបាច់គិតអ្វីទាំងអស់ ប៉ុន្តែបន្ទាប់មកយើងចងចាំថាការហៀរទឹកអាចកើតឡើង។ ដូច្នេះ សូម្បីតែ​ដើម្បី​យល់​ថា​បញ្ហា​សាមញ្ញ​ឬ​ស្មុគស្មាញ​ក៏ដោយ​ដំបូង​អ្នក​ត្រូវ​គិត។

ប្រសិនបើអ្នកគិតតាមរយៈដំណោះស្រាយដែលអាចកើតមានចំពោះបញ្ហាជាមុន អ្នកអាចជៀសវាងកំហុស។ ប៉ុន្តែនេះទាមទារការគិតរបស់អ្នកឱ្យច្បាស់លាស់។ ដើម្បីសម្រេចបាននូវចំណុចនេះ អ្នកត្រូវសរសេរគំនិតរបស់អ្នក។ ខ្ញុំចូលចិត្តសម្រង់សម្តីរបស់ Dick Guindon៖ "នៅពេលអ្នកសរសេរ ធម្មជាតិបង្ហាញអ្នកពីរបៀបដែលការគិតរបស់អ្នកច្របូកច្របល់"។ បើមិនសរសេរទេ គិតតែពីគិត។ ហើយអ្នកត្រូវសរសេរគំនិតរបស់អ្នកក្នុងទម្រង់នៃការបញ្ជាក់។

ការបញ្ជាក់បម្រើមុខងារជាច្រើន ជាពិសេសនៅក្នុងគម្រោងធំៗ។ ប៉ុន្តែខ្ញុំនឹងនិយាយអំពីពួកគេតែមួយប៉ុណ្ណោះ៖ ពួកគេជួយយើងគិតឱ្យបានច្បាស់លាស់។ ការគិតឱ្យច្បាស់គឺមានសារៈសំខាន់ និងពិបាកណាស់ ដូច្នេះយើងត្រូវការជំនួយណាមួយនៅទីនេះ។ តើ​យើង​គួរ​សរសេរ​លក្ខណៈ​ពិសេស​ជា​ភាសា​អ្វី? ជាទូទៅ នេះតែងតែជាសំណួរដំបូងសម្រាប់អ្នកសរសេរកម្មវិធី៖ តើយើងនឹងសរសេរជាភាសាអ្វី? មិនមានចម្លើយត្រឹមត្រូវមួយទេ៖ បញ្ហាដែលយើងដោះស្រាយមានភាពចម្រុះពេក។ សម្រាប់មនុស្សមួយចំនួន TLA+ មានប្រយោជន៍ - វាជាភាសាជាក់លាក់ដែលខ្ញុំបានបង្កើត។ សម្រាប់អ្នកផ្សេងទៀត វាកាន់តែងាយស្រួលប្រើភាសាចិន។ វាទាំងអស់គឺអាស្រ័យលើស្ថានភាព។

សំណួរ​សំខាន់​ជាង​នេះ​គឺ៖ តើ​យើង​អាច​សម្រេច​បាន​នូវ​ការ​គិត​កាន់​តែ​ច្បាស់​ដោយ​របៀប​ណា? ចម្លើយ៖ យើងត្រូវតែគិតដូចអ្នកវិទ្យាសាស្ត្រ។ នេះ​ជា​វិធី​គិត​ដែល​បាន​ដំណើរការ​ល្អ​ក្នុង​រយៈពេល ៥០០ ឆ្នាំ​ចុង​ក្រោយ​នេះ។ នៅក្នុងវិទ្យាសាស្ត្រ យើងបង្កើតគំរូគណិតវិទ្យានៃការពិត។ តារាវិទ្យាប្រហែលជាវិទ្យាសាស្ត្រដំបូងគេក្នុងន័យតឹងរឹងនៃពាក្យ។ នៅក្នុងគំរូគណិតវិទ្យាដែលប្រើក្នុងវិស័យតារាសាស្ត្រ សាកសពសេឡេស្ទាលលេចឡើងជាចំណុចជាមួយនឹងម៉ាស់ ទីតាំង និងសន្ទុះ ទោះបីជាការពិតពួកវាជាវត្ថុស្មុគស្មាញខ្លាំងជាមួយនឹងភ្នំ និងមហាសមុទ្រ រលក និងលំហូរក៏ដោយ។ គំរូនេះត្រូវបានបង្កើតឡើងដើម្បីដោះស្រាយបញ្ហាជាក់លាក់។ វាល្អណាស់សម្រាប់ការកំណត់កន្លែងដែលត្រូវចង្អុលកែវយឺតប្រសិនបើអ្នកចង់ស្វែងរកភពមួយ។ ប៉ុន្តែប្រសិនបើអ្នកចង់ទស្សន៍ទាយអាកាសធាតុនៅលើភពផែនដីនេះ គំរូនេះនឹងមិនដំណើរការទេ។

គណិតវិទ្យាអនុញ្ញាតឱ្យយើងកំណត់លក្ខណៈសម្បត្តិនៃគំរូមួយ។ ហើយវិទ្យាសាស្រ្តបង្ហាញពីរបៀបដែលលក្ខណៈសម្បត្តិទាំងនេះទាក់ទងនឹងការពិត។ ចូរនិយាយអំពីវិទ្យាសាស្រ្តរបស់យើង វិទ្យាសាស្រ្តកុំព្យូទ័រ។ ការពិតដែលយើងធ្វើការជាមួយគឺប្រព័ន្ធកុំព្យូទ័រនៃប្រភេទផ្សេងៗគ្នាជាច្រើន៖ ខួរក្បាល កុងសូលហ្គេម កុំព្យូទ័រដែលដំណើរការកម្មវិធីជាដើម។ ខ្ញុំ​នឹង​និយាយ​អំពី​ការ​ប្រតិបត្តិ​កម្មវិធី​មួយ​នៅ​លើ​កុំព្យូទ័រ ប៉ុន្តែ​ដោយ​និង​ធំ ការ​សន្និដ្ឋាន​ទាំង​អស់​នេះ​អនុវត្ត​ចំពោះ​ប្រព័ន្ធ​កុំព្យូទ័រ​ណា​មួយ​។ នៅក្នុងវិទ្យាសាស្ត្ររបស់យើង យើងប្រើម៉ូដែលផ្សេងៗគ្នាជាច្រើន៖ ម៉ាស៊ីន Turing សំណុំនៃព្រឹត្តិការណ៍ដែលបានបញ្ជាដោយផ្នែក និងផ្សេងទៀតជាច្រើន។

តើកម្មវិធីអ្វី? នេះគឺជាកូដណាមួយដែលអាចពិចារណាដោយខ្លួនឯងបាន។ ឧបមាថាយើងត្រូវសរសេរកម្មវិធីរុករក។ យើងអនុវត្តកិច្ចការបី៖ រចនាបទបង្ហាញរបស់អ្នកប្រើប្រាស់នៃកម្មវិធី បន្ទាប់មកសរសេរដ្យាក្រាមកម្រិតខ្ពស់នៃកម្មវិធី ហើយចុងក្រោយសរសេរកូដ។ នៅពេលយើងសរសេរកូដ យើងដឹងថាយើងត្រូវសរសេរទម្រង់អត្ថបទ។ នៅទីនេះម្តងទៀតយើងត្រូវដោះស្រាយបញ្ហាបី: កំណត់ថាតើអត្ថបទអ្វីដែលឧបករណ៍នេះនឹងត្រលប់មកវិញ។ ជ្រើសរើសក្បួនដោះស្រាយសម្រាប់ការធ្វើទ្រង់ទ្រាយ; សរសេរកូដ។ កិច្ចការនេះមានកិច្ចការរងរបស់វា៖ បញ្ចូលសហសញ្ញាទៅក្នុងពាក្យឱ្យបានត្រឹមត្រូវ។ យើងក៏ដោះស្រាយកិច្ចការរងនេះជាបីជំហានផងដែរ - ដូចដែលយើងឃើញ ពួកវាត្រូវបានធ្វើម្តងទៀតនៅកម្រិតជាច្រើន។

ចូរយើងពិនិត្យមើលឱ្យកាន់តែច្បាស់នៅជំហានដំបូង: តើបញ្ហាអ្វីដែលកម្មវិធីដោះស្រាយ។ នៅទីនេះយើងច្រើនតែយកគំរូតាមកម្មវិធីជាមុខងារដែលយកធាតុចូលខ្លះ និងផ្តល់លទ្ធផលខ្លះ។ នៅក្នុងគណិតវិទ្យា មុខងារមួយត្រូវបានពិពណ៌នាជាធម្មតាថាជាសំណុំនៃគូ។ ឧទាហរណ៍ អនុគមន៍​ការេ​សម្រាប់​លេខ​ធម្មជាតិ​ត្រូវ​បាន​ពិពណ៌នា​ជា​សំណុំ {<0,0>, <1,1>, <2,4>, <3,9>, … }។ ដែននៃនិយមន័យនៃមុខងារបែបនេះ គឺជាសំណុំនៃធាតុទីមួយនៃគូនីមួយៗ ពោលគឺលេខធម្មជាតិ។ ដើម្បីកំណត់មុខងារ យើងត្រូវបញ្ជាក់ដែន និងរូបមន្តរបស់វា។

ប៉ុន្តែមុខងារនៅក្នុងគណិតវិទ្យាមិនដូចគ្នាទៅនឹងមុខងារនៅក្នុងភាសាសរសេរកម្មវិធីនោះទេ។ គណិតវិទ្យាគឺសាមញ្ញជាង។ ដោយសារខ្ញុំមិនមានពេលសម្រាប់ឧទាហរណ៍ស្មុគ្រស្មាញ សូមពិចារណាសាមញ្ញមួយ៖ មុខងារមួយនៅក្នុង C ឬវិធីសាស្ត្រឋិតិវន្តនៅក្នុង Java ដែលត្រឡប់ផ្នែកចែកទូទៅធំបំផុតនៃចំនួនគត់ពីរ។ នៅក្នុងការបញ្ជាក់នៃវិធីសាស្រ្តនេះយើងនឹងសរសេរ: គណនា GCD(M,N) សម្រាប់អាគុយម៉ង់ M и Nដែលជាកន្លែង GCD(M,N) - អនុគមន៍​ដែល​ដែន​ជា​សំណុំ​នៃ​ចំនួន​គត់​គូ ហើយ​តម្លៃ​ត្រឡប់​ជា​ចំនួន​គត់​ធំ​បំផុត​ដែល​ត្រូវ​បាន​បែងចែក​ដោយ M и N. តើការពិតប្រៀបធៀបទៅនឹងគំរូនេះយ៉ាងដូចម្តេច? គំរូដំណើរការជាមួយចំនួនគត់ ហើយនៅក្នុង C ឬ Java យើងមាន 32 ប៊ីត int. គំរូនេះអនុញ្ញាតឱ្យយើងសម្រេចចិត្តថាតើ algorithm ត្រឹមត្រូវឬអត់ GCDប៉ុន្តែវានឹងមិនការពារកំហុសលើសចំណុះទេ។ នេះនឹងតម្រូវឱ្យមានគំរូស្មុគ្រស្មាញជាងនេះ ដែលមិនមានពេលវេលា។

ចូរនិយាយអំពីដែនកំណត់នៃមុខងារជាគំរូ។ កម្មវិធីមួយចំនួន (ដូចជាប្រព័ន្ធប្រតិបត្តិការ) មិនគ្រាន់តែត្រឡប់តម្លៃជាក់លាក់សម្រាប់អាគុយម៉ង់ជាក់លាក់ប៉ុណ្ណោះទេ ពួកគេអាចដំណើរការជាបន្តបន្ទាប់។ លើសពីនេះ មុខងារជាគំរូគឺមិនសូវសមសម្រាប់ជំហានទីពីរ៖ ការធ្វើផែនការរបៀបដោះស្រាយបញ្ហា។ Quicksort និង bubble sort គណនាមុខងារដូចគ្នា ប៉ុន្តែពួកវាជាក្បួនដោះស្រាយខុសគ្នាទាំងស្រុង។ ដូច្នេះដើម្បីពិពណ៌នាអំពីវិធីដើម្បីសម្រេចបាននូវគោលដៅនៃកម្មវិធី ខ្ញុំប្រើគំរូមួយផ្សេងទៀត សូមហៅវាថា គំរូអាកប្បកិរិយាស្តង់ដារ។ កម្មវិធីត្រូវបានតំណាងនៅក្នុងវាជាសំណុំនៃឥរិយាបទត្រឹមត្រូវទាំងអស់ ដែលនីមួយៗជាលំដាប់នៃរដ្ឋ ហើយរដ្ឋមួយគឺជាការចាត់ចែងតម្លៃទៅអថេរ។

តោះមើលថាតើជំហានទីពីរសម្រាប់ក្បួនដោះស្រាយ Euclidean នឹងមើលទៅដូចអ្វី។ យើងត្រូវការគណនា 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 សម្រាប់លេខដែលមិនវិជ្ជមានមែនទេ? ប្រសិនបើនេះមិនចាំបាច់ទេនោះអ្នកគ្រាន់តែត្រូវការផ្លាស់ប្តូរការបញ្ជាក់។

ការវិភាគសង្ខេបអំពីផលិតភាពគឺស្ថិតនៅក្នុងលំដាប់នៅទីនេះ។ ជារឿយៗវាត្រូវបានវាស់ជាចំនួនបន្ទាត់នៃកូដដែលសរសេរក្នុងមួយថ្ងៃ។ ប៉ុន្តែការងាររបស់អ្នកមានប្រយោជន៍ជាងប្រសិនបើអ្នកកម្ចាត់ចំនួនបន្ទាត់ជាក់លាក់មួយ ព្រោះអ្នកមានកន្លែងតិចសម្រាប់កំហុស។ ហើយវិធីងាយស្រួលបំផុតដើម្បីកម្ចាត់កូដគឺនៅក្នុងជំហានដំបូង។ វាអាចទៅរួចដែលអ្នកមិនត្រូវការកណ្តឹង និងហួចទាំងអស់ដែលអ្នកកំពុងព្យាយាមអនុវត្ត។ មធ្យោបាយលឿនបំផុតដើម្បីធ្វើឱ្យកម្មវិធីងាយស្រួល និងសន្សំសំចៃពេលវេលាគឺកុំធ្វើរឿងដែលមិនគួរធ្វើ។ ជំហានទីពីរមានសក្តានុពលសន្សំសំចៃពេលវេលាខ្ពស់បំផុតទីពីរ។ ប្រសិនបើអ្នកវាស់វែងផលិតភាពតាមបន្ទាត់ដែលបានសរសេរនោះ ការគិតអំពីរបៀបបញ្ចប់កិច្ចការនឹងធ្វើឱ្យអ្នក។ ផលិតភាពតិចពីព្រោះអ្នកអាចដោះស្រាយបញ្ហាដូចគ្នាជាមួយនឹងកូដតិច។ ខ្ញុំមិនអាចផ្តល់ស្ថិតិពិតប្រាកដនៅទីនេះបានទេ ព្រោះខ្ញុំគ្មានវិធីរាប់ចំនួនបន្ទាត់ដែលខ្ញុំមិនបានសរសេរដោយសារពេលវេលាដែលខ្ញុំបានចំណាយលើការបញ្ជាក់នោះទេ ពោលគឺនៅជំហានទីមួយ និងទីពីរ។ ហើយ​យើង​ក៏​មិន​អាច​ធ្វើ​ការ​ពិសោធ​នៅ​ទី​នេះ​ដែរ ព្រោះ​នៅ​ក្នុង​ការ​ពិសោធ​មួយ យើង​មិន​មាន​សិទ្ធិ​បញ្ចប់​ជំហាន​ដំបូង​ឡើយ កិច្ចការ​ត្រូវ​បាន​កំណត់​ជាមុន។

វាងាយស្រួលក្នុងការមើលរំលងការលំបាកជាច្រើននៅក្នុងលក្ខណៈបច្ចេកទេសក្រៅផ្លូវការ។ មិនមានអ្វីពិបាកទេក្នុងការសរសេរការកំណត់ជាក់លាក់សម្រាប់មុខងារ ខ្ញុំនឹងមិនពិភាក្សារឿងនេះទេ។ ជំនួសមកវិញ យើងនឹងនិយាយអំពីការសរសេរលក្ខណៈជាក់លាក់ខ្លាំងសម្រាប់ឥរិយាបថស្តង់ដារ។ មានទ្រឹស្តីបទដែលចែងថាសំណុំនៃអាកប្បកិរិយាណាមួយអាចត្រូវបានពិពណ៌នាដោយប្រើទ្រព្យសម្បត្តិសុវត្ថិភាព (សុវត្ថិភាព) និងលក្ខណៈសម្បត្តិនៃការរស់រានមានជីវិត (ភាពរស់រវើក). សុវត្ថិភាពមានន័យថាគ្មានអ្វីអាក្រក់នឹងកើតឡើងទេកម្មវិធីនឹងមិនផ្តល់ចម្លើយខុសទេ។ ការរស់រានមានជីវិត មានន័យថា មិនយូរមិនឆាប់ អ្វីល្អនឹងកើតឡើង ពោលគឺកម្មវិធីនឹងផ្តល់ចម្លើយត្រឹមត្រូវ។ តាមក្បួនមួយ សុវត្ថិភាពគឺជាសូចនាករសំខាន់ជាង កំហុសភាគច្រើនកើតឡើងនៅទីនេះ។ ដូច្នេះហើយ ដើម្បីសន្សំពេលវេលា ខ្ញុំនឹងមិននិយាយអំពីការរស់រានមានជីវិតទេ ទោះបីជាវាជាការពិតក៏សំខាន់ផងដែរ។

យើងសម្រេចបាននូវសុវត្ថិភាពដោយការបញ្ជាក់ជាដំបូងនូវសំណុំនៃស្ថានភាពដំបូងដែលអាចកើតមាន។ ហើយទីពីរ ទំនាក់ទំនងជាមួយរដ្ឋបន្ទាប់ដែលអាចធ្វើទៅបានសម្រាប់រដ្ឋនីមួយៗ។ ចូរយើងប្រព្រឹត្តដូចអ្នកវិទ្យាសាស្ត្រ ហើយកំណត់រដ្ឋតាមគណិតវិទ្យា។ សំណុំនៃរដ្ឋដំបូងត្រូវបានពិពណ៌នាដោយរូបមន្ត ឧទាហរណ៍ ក្នុងករណីនៃក្បួនដោះស្រាយ Euclidean៖ (x = M) ∧ (y = N). សម្រាប់តម្លៃជាក់លាក់ M и N មានរដ្ឋដំបូងតែមួយគត់។ ទំនាក់ទំនងជាមួយរដ្ឋបន្ទាប់ត្រូវបានពិពណ៌នាដោយរូបមន្តដែលអថេរនៃរដ្ឋបន្ទាប់ត្រូវបានសរសេរដោយបឋម ហើយអថេរនៃរដ្ឋបច្ចុប្បន្នត្រូវបានសរសេរដោយគ្មានបឋម។ នៅក្នុងករណីនៃក្បួនដោះស្រាយ Euclidean យើងនឹងដោះស្រាយជាមួយនឹងការបំបែកនៃរូបមន្តពីរដែលក្នុងនោះមួយ x គឺជាតម្លៃធំបំផុត ហើយនៅក្នុងទីពីរ - y:

ក្នុងករណីដំបូង តម្លៃថ្មីនៃ y គឺស្មើនឹងតម្លៃមុនរបស់ y ហើយយើងទទួលបានតម្លៃថ្មីនៃ x ដោយដកអថេរតូចជាងពីធំជាង។ ក្នុងករណីទីពីរយើងធ្វើផ្ទុយ។

ចូរយើងត្រលប់ទៅក្បួនដោះស្រាយ Euclidean ។ ឧបមាថាម្តងទៀត 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] ផ្នែកទាំងពីរនៃកន្សោមនឹងមិនពិត ដូច្នេះវាមិនមានស្ថានភាពបន្ទាប់ទេ។ ដូច្នេះ យើងមានការបញ្ជាក់ពេញលេញនៃជំហានទីពីរ - ដូចដែលយើងឃើញ នេះពិតជាគណិតវិទ្យាធម្មតា ដូចជាវិស្វករ និងអ្នកវិទ្យាសាស្ត្រ ហើយមិនចម្លែកទេ ដូចជានៅក្នុងវិទ្យាសាស្ត្រកុំព្យូទ័រ។

រូបមន្តទាំងពីរនេះអាចបញ្ចូលគ្នាទៅជារូបមន្តមួយនៃតក្កវិជ្ជាបណ្ដោះអាសន្ន។ វាមានភាពឆើតឆាយ និងងាយស្រួលពន្យល់ ប៉ុន្តែមិនមានពេលសម្រាប់វាឥឡូវនេះទេ។ យើងប្រហែលជាត្រូវការតក្កវិជ្ជាបណ្ដោះអាសន្នសម្រាប់តែទ្រព្យសម្បត្តិនៃភាពរស់រវើកប៉ុណ្ណោះ សម្រាប់សុវត្ថិភាពវាមិនចាំបាច់ទេ។ ខ្ញុំ​មិន​ចូល​ចិត្ត​តក្កវិជ្ជា​បណ្ដោះ​អាសន្ន​បែប​នេះ​ទេ វា​មិន​មែន​ជា​គណិតវិទ្យា​ធម្មតា​ទេ ប៉ុន្តែ​ក្នុង​ករណី​ភាព​រស់​រវើក​វា​ជា​អំពើ​អាក្រក់​ចាំបាច់។

នៅក្នុងក្បួនដោះស្រាយ Euclidean សម្រាប់តម្លៃនីមួយៗ x и y មានតម្លៃពិសេស x' и y'ដែលធ្វើឱ្យទំនាក់ទំនងជាមួយរដ្ឋបន្ទាប់ជាការពិត។ នៅក្នុងពាក្យផ្សេងទៀត ក្បួនដោះស្រាយ Euclidean គឺជាការកំណត់។ ដើម្បីយកគំរូតាមក្បួនដោះស្រាយ nondeterministic រដ្ឋបច្ចុប្បន្នត្រូវតែមានរដ្ឋនាពេលអនាគតជាច្រើនដែលអាចធ្វើទៅបាន ហើយតម្លៃនីមួយៗនៃអថេរ unprimed ត្រូវតែមានតម្លៃច្រើននៃអថេរបឋម ដែលទំនាក់ទំនងទៅរដ្ឋបន្ទាប់គឺពិត។ នេះ​មិន​ពិបាក​ធ្វើ​ទេ ប៉ុន្តែ​ខ្ញុំ​នឹង​មិន​លើក​ឧទាហរណ៍​ឥឡូវ​នេះ​ទេ។

ដើម្បីបង្កើតឧបករណ៍ធ្វើការ អ្នកត្រូវការគណិតវិទ្យាផ្លូវការ។ តើធ្វើដូចម្តេចដើម្បីធ្វើឱ្យការបញ្ជាក់ជាផ្លូវការ? ដើម្បីធ្វើដូចនេះយើងនឹងត្រូវការភាសាផ្លូវការ ឧ. TLA+. ការបញ្ជាក់នៃក្បួនដោះស្រាយ Euclidean នៅក្នុងភាសានេះនឹងមើលទៅដូចនេះ៖

និមិត្តសញ្ញាសញ្ញាស្មើជាមួយត្រីកោណមានន័យថាតម្លៃនៅខាងឆ្វេងនៃសញ្ញាត្រូវបានកំណត់ថាស្មើនឹងតម្លៃនៅខាងស្តាំនៃសញ្ញា។ នៅក្នុងខ្លឹមសារ ការបញ្ជាក់គឺជានិយមន័យមួយ ក្នុងករណីរបស់យើង និយមន័យពីរ។ ចំពោះការបញ្ជាក់នៅក្នុង TLA+ អ្នកត្រូវបន្ថែមការប្រកាស និងវាក្យសម្ព័ន្ធមួយចំនួន ដូចនៅក្នុងស្លាយខាងលើ។ នៅក្នុង ASCII វានឹងមើលទៅដូចនេះ:

ដូចដែលអ្នកអាចឃើញគ្មានអ្វីស្មុគស្មាញទេ។ ការបញ្ជាក់នៅលើ TLA+ អាចត្រូវបានផ្ទៀងផ្ទាត់ ពោលគឺវាអាចទៅរួចក្នុងការរំលងឥរិយាបថដែលអាចកើតមានទាំងអស់នៅក្នុងគំរូតូចមួយ។ ក្នុងករណីរបស់យើងគំរូនេះនឹងមានតម្លៃជាក់លាក់ M и N. នេះគឺជាវិធីសាស្ត្រផ្ទៀងផ្ទាត់ដ៏មានប្រសិទ្ធភាព និងសាមញ្ញបំផុតដែលដោយស្វ័យប្រវត្តិទាំងស្រុង។ លើសពីនេះ គេអាចសរសេរភស្តុតាងផ្លូវការនៃការពិត និងពិនិត្យមើលវាដោយមេកានិច ប៉ុន្តែត្រូវចំណាយពេលច្រើន ដូច្នេះស្ទើរតែគ្មាននរណាម្នាក់ធ្វើបែបនេះទេ។

គុណវិបត្តិចម្បងនៃ TLA+ គឺថាវាជាគណិតវិទ្យា ហើយអ្នកសរសេរកម្មវិធី និងអ្នកវិទ្យាសាស្ត្រកុំព្យូទ័រខ្លាចគណិតវិទ្យា។ នៅ glance ដំបូង នេះស្តាប់ទៅដូចជារឿងកំប្លែងមួយ ប៉ុន្តែជាអកុសល ខ្ញុំនិយាយរឿងនេះក្នុងន័យធ្ងន់ធ្ងរទាំងអស់។ សហសេវិករបស់ខ្ញុំគ្រាន់តែប្រាប់ខ្ញុំពីរបៀបដែលគាត់ព្យាយាមពន្យល់ TLA+ ទៅកាន់អ្នកអភិវឌ្ឍន៍មួយចំនួន។ ដរាបណារូបមន្តបង្ហាញនៅលើអេក្រង់ ភ្នែករបស់ពួកគេក្លាយជាកញ្ចក់ភ្លាមៗ។ ដូច្នេះប្រសិនបើ TLA+ គួរឱ្យខ្លាច អ្នកអាចប្រើ បូកកាល់ជាប្រភេទភាសាសរសេរកម្មវិធីរបស់ក្មេងលេង។ កន្សោមនៅក្នុង PlusCal អាចជាកន្សោម TLA+ ណាមួយ នោះគឺជាកន្សោមគណិតវិទ្យាជាមូលដ្ឋានណាមួយ។ លើសពីនេះ PlusCal មានវាក្យសម្ព័ន្ធសម្រាប់ក្បួនដោះស្រាយមិនកំណត់។ ដោយសារតែ PlusCal អាចសរសេរកន្សោម TLA+ ណាមួយ វាមានការបញ្ចេញមតិច្រើនជាងភាសាសរសេរកម្មវិធីពិតប្រាកដណាមួយ។ បន្ទាប់មក PlusCal ត្រូវបានចងក្រងទៅជាការបញ្ជាក់ TLA+ ដែលងាយស្រួលអាន។ ជាការពិតណាស់នេះមិនមានន័យថាការបញ្ជាក់របស់ PlusCal ស្មុគស្មាញនឹងប្រែទៅជាសាមញ្ញមួយនៅលើ TLA+ នោះទេ - គ្រាន់តែថាការឆ្លើយឆ្លងរវាងពួកគេគឺជាក់ស្តែង គ្មានភាពស្មុគស្មាញបន្ថែមនឹងលេចឡើងទេ។ ជាចុងក្រោយ ការបញ្ជាក់នេះអាចត្រូវបានផ្ទៀងផ្ទាត់ដោយប្រើឧបករណ៍ TLA+ ។ ជាទូទៅ PlusCal អាចជួយយកឈ្នះលើការភ័យខ្លាចនៃគណិតវិទ្យា វាងាយស្រួលយល់ សូម្បីតែអ្នកសរសេរកម្មវិធី និងអ្នកវិទ្យាសាស្ត្រកុំព្យូទ័រក៏ដោយ។ ខ្ញុំបានបោះពុម្ពក្បួនដោះស្រាយនៅលើវាមួយរយៈ (ប្រហែល 10 ឆ្នាំ) កាលពីអតីតកាល។

ប្រហែលជាមាននរណាម្នាក់នឹងជំទាស់ថា TLA+ និង PlusCal គឺជាគណិតវិទ្យា ហើយគណិតវិទ្យាដំណើរការតែជាមួយឧទាហរណ៍ដែលបង្កើតឡើងប៉ុណ្ណោះ។ នៅក្នុងការអនុវត្ត អ្នកត្រូវការភាសាពិតប្រាកដជាមួយនឹងប្រភេទ នីតិវិធី វត្ថុ និងអ្វីៗផ្សេងទៀត។ នេះ​គឺ​ខុស។ នេះជាអ្វីដែល Chris Newcomb ដែលធ្វើការនៅ Amazon សរសេរថា៖ "យើងបានប្រើប្រាស់ TLA+ លើគម្រោងធំៗចំនួនដប់ ហើយក្នុងគ្រប់ករណីទាំងអស់ ការប្រើប្រាស់របស់វាធ្វើឱ្យមានភាពខុសប្លែកគ្នាយ៉ាងខ្លាំងចំពោះការអភិវឌ្ឍន៍ ពីព្រោះយើងអាចចាប់កំហុសដែលមានគ្រោះថ្នាក់មុនពេលវាឈានដល់ការផលិត ហើយព្រោះវាផ្តល់ឱ្យយើងនូវការយល់ដឹង និងទំនុកចិត្តដែលយើងត្រូវការដើម្បីធ្វើឱ្យមានភាពឈ្លានពាន។ ការបង្កើនប្រសិទ្ធភាពការអនុវត្តដោយមិនមានឥទ្ធិពលលើការពិតនៃកម្មវិធី". ជាញឹកញាប់អ្នកអាចលឺថានៅពេលប្រើវិធីសាស្រ្តផ្លូវការយើងទទួលបានកូដមិនមានប្រសិទ្ធភាព - នៅក្នុងការអនុវត្តអ្វីគ្រប់យ៉ាងគឺផ្ទុយពីនេះ។ លើសពីនេះ មានការយល់ឃើញមួយថា អ្នកគ្រប់គ្រងមិនអាចជឿជាក់លើតម្រូវការសម្រាប់វិធីសាស្រ្តផ្លូវការនោះទេ ទោះបីជាអ្នកសរសេរកម្មវិធីជឿជាក់លើអត្ថប្រយោជន៍របស់ពួកគេក៏ដោយ។ ហើយ Newcomb សរសេរថា៖ "ឥឡូវនេះអ្នកគ្រប់គ្រងកំពុងជំរុញគ្រប់មធ្យោបាយដែលអាចធ្វើទៅបានដើម្បីសរសេរការបញ្ជាក់នៅក្នុង TLA+ ហើយជាពិសេសកំពុងបែងចែកពេលវេលាសម្រាប់រឿងនេះ". ដូច្នេះនៅពេលដែលអ្នកគ្រប់គ្រងឃើញថា TLA+ ដំណើរការ ពួកគេទទួលយកវា។ Chris Newcomb បានសរសេររឿងនេះប្រហែលប្រាំមួយខែមុន (ខែតុលា 2014) ប៉ុន្តែឥឡូវនេះ តាមដែលខ្ញុំដឹង TLA+ ត្រូវបានប្រើក្នុងគម្រោងចំនួន 14 មិនមែន 10 ទេ។ ឧទាហរណ៍មួយទៀតទាក់ទងនឹងការរចនារបស់ XBox 360។ អ្នកហាត់ការម្នាក់បានមកដល់ Charles Thacker ហើយ បានសរសេរបញ្ជាក់សម្រាប់ប្រព័ន្ធអង្គចងចាំ។ សូមអរគុណចំពោះការបញ្ជាក់នេះ កំហុសមួយត្រូវបានរកឃើញដែលនឹងមិនត្រូវបានរកឃើញ ហើយនឹងធ្វើឱ្យរាល់ 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 ។

ហេតុអ្វីខ្ញុំត្រូវសរសេរការបញ្ជាក់ ប្រសិនបើខ្ញុំដឹងរួចហើយថា កូដគួរធ្វើអ្វី? តាមពិតខ្ញុំគ្រាន់តែគិតថាខ្ញុំដឹង។ លើសពីនេះទៀត ជាមួយនឹងការបញ្ជាក់នៅនឹងកន្លែង អ្នកខាងក្រៅលែងត្រូវការរកមើលកូដដើម្បីយល់ពីអ្វីដែលវាធ្វើ។ ខ្ញុំមានច្បាប់៖ មិនគួរមានច្បាប់ទូទៅទេ។ មានការលើកលែងចំពោះច្បាប់នេះ ជាការពិតនេះគឺជាច្បាប់ទូទៅតែមួយគត់ដែលខ្ញុំធ្វើតាម៖ លក្ខណៈជាក់លាក់នៃអ្វីដែលកូដធ្វើគួរតែប្រាប់មនុស្សទាំងអស់ដែលពួកគេត្រូវដឹងនៅពេលប្រើកូដនោះ។

ដូច្នេះតើអ្នកសរសេរកម្មវិធីត្រូវដឹងអ្វីខ្លះអំពីការគិត? ដើម្បីចាប់ផ្តើម ដូចគ្នានឹងមនុស្សគ្រប់គ្នាដែរ៖ ប្រសិនបើអ្នកមិនសរសេរទេ វាគ្រាន់តែជាអ្នកដែលអ្នកកំពុងគិតប៉ុណ្ណោះ។ ដូចគ្នានេះផងដែរ អ្នកត្រូវគិតមុនពេលអ្នកសរសេរកូដ ដែលមានន័យថាអ្នកត្រូវសរសេរមុនពេលអ្នកសរសេរកូដ។ ការបញ្ជាក់គឺជាអ្វីដែលយើងសរសេរមុនពេលយើងចាប់ផ្តើមសរសេរកូដ។ ការបញ្ជាក់គឺត្រូវការសម្រាប់លេខកូដដែលអាចប្រើ ឬផ្លាស់ប្តូរដោយនរណាម្នាក់។ ហើយ "នរណាម្នាក់" នេះអាចក្លាយជាអ្នកនិពន្ធនៃកូដមួយខែបន្ទាប់ពីវាត្រូវបានសរសេរ។ ការបញ្ជាក់គឺត្រូវការសម្រាប់កម្មវិធី និងប្រព័ន្ធធំៗ សម្រាប់ថ្នាក់ សម្រាប់វិធីសាស្រ្ត និងពេលខ្លះសូម្បីតែសម្រាប់ផ្នែកស្មុគស្មាញនៃវិធីសាស្ត្រតែមួយ។ តើអ្នកគួរសរសេរអ្វីពិតប្រាកដអំពីកូដ? អ្នកត្រូវពណ៌នាអំពីអ្វីដែលវាធ្វើ នោះគឺជាអ្វីមួយដែលអាចមានប្រយោជន៍សម្រាប់អ្នកដែលប្រើកូដនេះ។ ពេលខ្លះវាក៏អាចចាំបាច់ផងដែរក្នុងការបញ្ជាក់ថាតើលេខកូដសម្រេចបានគោលដៅរបស់វាយ៉ាងដូចម្តេច។ ប្រសិនបើយើងបានឆ្លងកាត់វិធីសាស្រ្តនេះនៅក្នុងវគ្គសិក្សា algorithms នោះយើងហៅវាថា algorithm ។ ប្រសិនបើវាជាអ្វីដែលពិសេស និងថ្មីជាងនេះ យើងហៅវាថាការរចនាកម្រិតខ្ពស់។ មិនមានភាពខុសគ្នាជាផ្លូវការនៅទីនេះទេ៖ ទាំងពីរគឺជាគំរូអរូបីនៃកម្មវិធី។

តើអ្នកគួរសរសេរកូដជាក់លាក់បែបណា? រឿងចំបង៖ វាគួរតែខ្ពស់ជាងលេខកូដខ្លួនឯង។ វាត្រូវតែពិពណ៌នាអំពីរដ្ឋ និងអាកប្បកិរិយា។ វាគួរតែតឹងរ៉ឹងដូចដែលកិច្ចការទាមទារ។ ប្រសិនបើអ្នកកំពុងសរសេរការបញ្ជាក់អំពីវិធីអនុវត្តភារកិច្ច នោះវាអាចត្រូវបានសរសេរជា pseudocode ឬដោយប្រើ PlusCal ។ អ្នក​ត្រូវ​រៀន​សរសេរ​ការ​បញ្ជាក់​ដោយ​ប្រើ​ការ​បញ្ជាក់​ផ្លូវការ។ នេះនឹងផ្តល់ឱ្យអ្នកនូវជំនាញចាំបាច់ដែលនឹងជួយអ្នកក្រៅផ្លូវការផងដែរ។ តើអ្នកអាចរៀនសរសេរលក្ខណៈផ្លូវការដោយរបៀបណា? ពេល​យើង​រៀន​សរសេរ​កម្មវិធី យើង​បាន​សរសេរ​កម្មវិធី ហើយ​បន្ទាប់​មក​កែ​កំហុស​ពួក​គេ។ រឿងដដែលនេះនៅទីនេះ៖ អ្នកត្រូវសរសេរការបញ្ជាក់ ពិនិត្យវាជាមួយឧបករណ៍ពិនិត្យគំរូ និងជួសជុលកំហុស។ TLA+ ប្រហែលជាមិនមែនជាភាសាដ៏ល្អបំផុតសម្រាប់ការបញ្ជាក់ជាផ្លូវការនោះទេ ហើយភាសាផ្សេងទៀតទំនងជាសាកសមជាងសម្រាប់តម្រូវការជាក់លាក់របស់អ្នក។ រឿងដ៏អស្ចារ្យអំពី TLA+ គឺថាវាធ្វើការងារដ៏អស្ចារ្យក្នុងការបង្រៀនការគិតគណិតវិទ្យា។

របៀបភ្ជាប់ការបញ្ជាក់ និងលេខកូដ? ការប្រើមតិយោបល់ដែលភ្ជាប់គំនិតគណិតវិទ្យា និងការអនុវត្តរបស់ពួកគេ។ ប្រសិនបើអ្នកធ្វើការជាមួយក្រាហ្វបន្ទាប់មកនៅកម្រិតកម្មវិធីអ្នកនឹងមានអារេនៃថ្នាំងនិងអារេនៃតំណភ្ជាប់។ ដូច្នេះអ្នកត្រូវសរសេរថាតើក្រាហ្វត្រូវបានអនុវត្តដោយរចនាសម្ព័ន្ធកម្មវិធីទាំងនេះ។

វាគួរតែត្រូវបានកត់សម្គាល់ថាគ្មានណាមួយខាងលើអនុវត្តចំពោះដំណើរការនៃការសរសេរកូដខ្លួនឯងនោះទេ។ នៅពេលអ្នកសរសេរកូដ នោះគឺអនុវត្តជំហានទីបី អ្នកក៏ត្រូវគិត និងគិតតាមកម្មវិធីផងដែរ។ ប្រសិនបើកិច្ចការរងប្រែទៅជាស្មុគស្មាញ ឬមិនច្បាស់ អ្នកត្រូវសរសេរការបញ្ជាក់សម្រាប់វា។ ប៉ុន្តែខ្ញុំមិននិយាយអំពីកូដខ្លួនឯងនៅទីនេះទេ។ អ្នកអាចប្រើភាសាសរសេរកម្មវិធីណាមួយ វិធីសាស្រ្តណាមួយ នេះមិនមែននិយាយអំពីពួកគេទេ។ ដូចគ្នាដែរ គ្មានចំណុចណាមួយខាងលើអាចលុបបំបាត់តម្រូវការក្នុងការធ្វើតេស្ត និងបំបាត់កំហុសកូដរបស់អ្នកបានទេ។ ទោះបីជាគំរូអរូបីត្រូវបានសរសេរត្រឹមត្រូវក៏ដោយ វាអាចមានកំហុសក្នុងការអនុវត្តរបស់វា។

ការសរសេរជាក់លាក់គឺជាជំហានបន្ថែមនៅក្នុងដំណើរការសរសេរកូដ។ សូមអរគុណចំពោះវា កំហុសជាច្រើនអាចត្រូវបានគេចាប់បានដោយមានការខិតខំប្រឹងប្រែងតិច - យើងដឹងរឿងនេះពីបទពិសោធន៍របស់អ្នកសរសេរកម្មវិធីពី Amazon ។ ជាមួយនឹងលក្ខណៈជាក់លាក់ គុណភាពនៃកម្មវិធីកាន់តែខ្ពស់។ ដូច្នេះ ហេតុអ្វីបានជាយើងច្រើនតែទៅដោយគ្មានពួកគេ? ព្រោះការសរសេរគឺពិបាក។ ប៉ុន្តែ​ការ​សរសេរ​គឺ​ពិបាក​ព្រោះ​សម្រាប់​នេះ​អ្នក​ត្រូវ​គិត ហើយ​ការ​គិត​ក៏​ពិបាក​ដែរ។ វាតែងតែងាយស្រួលក្នុងការធ្វើពុតជាអ្នកគិត។ នៅទីនេះអ្នកអាចគូរភាពស្រដៀងគ្នាជាមួយនឹងការរត់ - អ្នករត់តិច អ្នករត់កាន់តែយឺត។ អ្នកត្រូវហ្វឹកហាត់សាច់ដុំរបស់អ្នក និងអនុវត្តការសរសេរ។ វាត្រូវការការអនុវត្ត។

ការ​បញ្ជាក់​អាច​នឹង​មិន​ត្រឹមត្រូវ។ អ្នកប្រហែលជាមានកំហុសនៅកន្លែងណាមួយ ឬតម្រូវការអាចនឹងមានការផ្លាស់ប្តូរ ឬការកែលម្អអាចនឹងត្រូវធ្វើ។ កូដណាមួយដែលនរណាម្នាក់ប្រើត្រូវតែផ្លាស់ប្តូរ ដូច្នេះមិនយូរមិនឆាប់ ការកំណត់នឹងលែងត្រូវគ្នានឹងកម្មវិធីទៀតហើយ។ តាមឧត្ដមគតិ ក្នុងករណីនេះ អ្នកត្រូវសរសេរការបញ្ជាក់ថ្មី ហើយសរសេរកូដឡើងវិញទាំងស្រុង។ យើងដឹងយ៉ាងច្បាស់ថាគ្មាននរណាម្នាក់ធ្វើបែបនេះទេ។ នៅក្នុងការអនុវត្ត យើងជួសជុលកូដ ហើយប្រហែលជាធ្វើបច្ចុប្បន្នភាពការបញ្ជាក់។ ប្រសិនបើរឿងនេះកើតឡើងឆាប់ៗ ឬយូរជាងនេះ ហេតុអ្វីត្រូវសរសេរបញ្ជាក់? ទីមួយ សម្រាប់អ្នកដែលនឹងកែសម្រួលកូដរបស់អ្នក រាល់ពាក្យបន្ថែមនៅក្នុងការបញ្ជាក់នឹងមានតម្លៃជាមាស ហើយបុគ្គលនេះប្រហែលជាអ្នកផងដែរ។ ខ្ញុំតែងតែទាត់ខ្លួនឯងថាមិនជាក់លាក់គ្រប់គ្រាន់នៅពេលខ្ញុំកែសម្រួលកូដរបស់ខ្ញុំ។ ហើយ​ខ្ញុំ​សរសេរ​បញ្ជាក់​ច្រើន​ជាង​កូដ។ ដូច្នេះហើយ នៅពេលដែលអ្នកកែសម្រួលកូដនោះ ការបញ្ជាក់តែងតែត្រូវធ្វើបច្ចុប្បន្នភាព។ ទីពីរ ជាមួយនឹងការកែសម្រួលនីមួយៗ កូដកាន់តែអាក្រក់ វាកាន់តែពិបាកអាន និងថែទាំ។ នេះគឺជាការកើនឡើងនៃ entropy ។ ប៉ុន្តែប្រសិនបើអ្នកមិនចាប់ផ្តើមជាមួយការបញ្ជាក់ទេនោះ រាល់បន្ទាត់ដែលអ្នកសរសេរនឹងត្រូវបានកែសម្រួល ហើយកូដនឹងមានសំពីងសំពោង និងពិបាកអានតាំងពីដំបូង។

ដូចដែលបាននិយាយ Eisenhower, គ្មាន​ការ​ប្រយុទ្ធ​ណា​មួយ​ត្រូវ​បាន​ឈ្នះ​តាម​ផែនការ​ទេ ហើយ​គ្មាន​ការ​ប្រយុទ្ធ​ណា​បាន​ឈ្នះ​ដោយ​គ្មាន​ផែនការ​នោះ​ទេ។. ហើយគាត់បានដឹងអ្វីមួយអំពីការប្រយុទ្ធ។ មាន​មតិ​មួយ​ថា​ការ​សរសេរ​បញ្ជាក់​គឺ​ជា​ការ​ខ្ជះខ្ជាយ​ពេល​វេលា។ ពេលខ្លះនេះជាការពិត ហើយកិច្ចការគឺសាមញ្ញណាស់ ដែលមិនមានចំណុចណាមួយក្នុងការគិតវា។ ប៉ុន្តែអ្នកគួរចងចាំជានិច្ចថា នៅពេលដែលអ្នកត្រូវបានណែនាំមិនអោយសរសេរជាក់លាក់ វាមានន័យថាអ្នកត្រូវបានណែនាំមិនឱ្យគិត។ ហើយអ្នកគួរគិតអំពីរឿងនេះរាល់ពេល។ ការ​គិត​តាម​កិច្ចការ​មួយ​មិន​ធានា​ថា​អ្នក​នឹង​មិន​ធ្វើ​ខុស​នោះ​ទេ។ ដូចដែលយើងដឹងហើយថាគ្មាននរណាម្នាក់បង្កើត wand វេទមន្តទេហើយការសរសេរកម្មវិធីគឺជាកិច្ចការដ៏លំបាកមួយ។ ប៉ុន្តែ​ប្រសិន​បើ​អ្នក​មិន​គិត​តាម​រយៈ​កិច្ច​ការ​នោះ​ទេ អ្នក​ត្រូវ​បាន​ធានា​ថា​នឹង​មាន​កំហុស។

អ្នកអាចអានបន្ថែមអំពី TLA+ និង PlusCal នៅលើគេហទំព័រពិសេស អ្នកអាចទៅទីនោះពីទំព័រដើមរបស់ខ្ញុំ តំណភ្ជាប់. នោះហើយជាទាំងអស់សម្រាប់ខ្ញុំ អរគុណសម្រាប់ការយកចិត្តទុកដាក់របស់អ្នក។

សូមចងចាំថានេះគឺជាការបកប្រែ។ នៅពេលអ្នកសរសេរយោបល់ សូមចាំថាអ្នកនិពន្ធនឹងមិនអានវាទេ។ ប្រសិនបើអ្នកពិតជាចង់ជជែកជាមួយអ្នកនិពន្ធ គាត់នឹងនៅក្នុងសន្និសីទ Hydra 2019 ដែលនឹងធ្វើឡើងនៅថ្ងៃទី 11-12 ខែកក្កដា ឆ្នាំ 2019 នៅ St. Petersburg។ សំបុត្រអាចទិញបាន។ នៅលើគេហទំព័រផ្លូវការ.

ប្រភព: www.habr.com