این یک مقاله ترجمه است . اما قبل از آن یک مقدمه کوتاه وجود دارد. زامبی ها چگونه تشکیل می شوند؟ همه در موقعیتی قرار گرفته اند که می خواهند دوست یا همکار خود را به سطح خود بیاورند، اما نتیجه نمی دهد. علاوه بر این، "این کار نمی کند" نه برای شما که برای او: در یک طرف مقیاس حقوق عادی، وظایف و غیره وجود دارد، و در طرف دیگر نیاز به فکر کردن است. فکر کردن ناخوشایند و دردناک است. او به سرعت تسلیم می شود و بدون استفاده از مغزش به کدنویسی ادامه می دهد. شما متوجه می شوید که برای غلبه بر سد درماندگی آموخته شده چقدر تلاش لازم است و به سادگی این کار را انجام نمی دهید. اینگونه زامبی ها شکل می گیرند که به نظر می رسد درمان آنها امکان پذیر باشد، اما به نظر می رسد که هیچ کس این کار را انجام نخواهد داد.
وقتی آن را دیدم (بله، همان دوست از کتاب های درسی) و گزارش نمی دهد، بلکه یک جلسه پرسش و پاسخ است، من کمی محتاط بودم. در هر صورت، لزلی یک دانشمند مشهور جهان، نویسنده آثار اساسی در محاسبات توزیع شده است، و همچنین ممکن است او را با حروف La در LaTeX - "Lamport TeX" بشناسید. دومین عامل هشداردهنده، الزام اوست: هرکسی که می آید باید (کاملاً رایگان) چند تا از گزارش های او را از قبل گوش کند، حداقل یک سوال در مورد آنها مطرح کند و فقط بعد بیاید. تصمیم گرفتم ببینم لامپورت چه چیزی را در آنجا پخش می کند - و عالی است! این دقیقاً همان چیزی است، یک قرص پیوند جادویی برای درمان زامبی ها. به شما هشدار می‌دهم: متن ممکن است به شدت کسانی را که عاشق روش‌های فوق‌العاده چابک هستند و دوست ندارند آنچه را که نوشته‌اند آزمایش کنند، بسوزاند.
بعد از حبروکات، ترجمه سمینار در واقع شروع می شود. از خواندن لذت ببرید!
هر کاری که بر عهده می گیرید، همیشه باید سه مرحله را طی کنید:
- تصمیم بگیرید که به چه هدفی می خواهید برسید؛
- تصمیم بگیرید که دقیقا چگونه به هدف خود خواهید رسید.
- به هدفت برس.
این در مورد برنامه نویسی نیز صدق می کند. وقتی کد می نویسیم، نیاز داریم:
- تصمیم بگیرید که برنامه دقیقاً چه کاری باید انجام دهد.
- دقیقاً تعیین کند که چگونه باید وظیفه خود را انجام دهد.
- کد مناسب را بنویسید
مرحله آخر، البته، بسیار مهم است، اما امروز در مورد آن صحبت نمی کنم. در عوض، دو مورد اول را مورد بحث قرار خواهیم داد. هر برنامه نویسی آنها را قبل از شروع به کار انجام می دهد. شما نمی نشینید تا بنویسید مگر اینکه تصمیم بگیرید چه می نویسید: مرورگر یا پایگاه داده. ایده خاصی از هدف باید وجود داشته باشد. و مطمئناً به این فکر می کنید که برنامه دقیقاً چه کاری انجام خواهد داد و آن را به طور تصادفی ننویسید به این امید که خود کد به نوعی به مرورگر تبدیل شود.
این پیش فکر کردن کد دقیقاً چگونه اتفاق می افتد؟ چقدر باید برای این کار تلاش کنیم؟ همه چیز به پیچیدگی مشکلی که ما حل می کنیم بستگی دارد. فرض کنید می خواهیم یک سیستم توزیع شده با تحمل خطا بنویسیم. در این مورد، قبل از اینکه به سراغ کدنویسی بنشینیم، باید به دقت به مسائل فکر کنیم. اگر فقط نیاز داشته باشیم یک متغیر عدد صحیح را 1 افزایش دهیم چه؟ در نگاه اول، همه چیز در اینجا پیش پا افتاده است و نیازی به فکر نیست، اما بعد به یاد می آوریم که یک سرریز ممکن است رخ دهد. بنابراین، حتی برای درک ساده یا پیچیده بودن یک مشکل، ابتدا باید فکر کنید.
اگر از قبل به راه حل های ممکن برای یک مشکل فکر کنید، می توانید از اشتباهات جلوگیری کنید. اما این مستلزم روشن بودن تفکر شماست. برای رسیدن به این هدف، باید افکار خود را یادداشت کنید. من عاشق جمله دیک گیندون هستم: "وقتی می نویسید، طبیعت به شما نشان می دهد که چقدر فکر شما شلخته است." اگر نمی نویسی، فقط فکر می کنی که فکر می کنی. و باید افکار خود را در قالب مشخصات بنویسید.
مشخصات عملکردهای زیادی را انجام می دهند، به خصوص در پروژه های بزرگ. اما من فقط در مورد یکی از آنها صحبت خواهم کرد: آنها به ما کمک می کنند تا به وضوح فکر کنیم. روشن فکر کردن بسیار مهم و بسیار دشوار است، بنابراین ما در اینجا به کمک نیاز داریم. مشخصات را به چه زبانی بنویسیم؟ به طور کلی، این همیشه اولین سوال برای برنامه نویسان است: به چه زبانی بنویسیم؟ هیچ پاسخ درستی وجود ندارد: مشکلاتی که ما حل می کنیم بسیار متنوع هستند. برای برخی افراد، TLA+ یک زبان مشخصاتی است که من توسعه داده ام. برای دیگران، استفاده از چینی راحت تر است. همه چیز به موقعیت بستگی دارد.
سوال مهمتر این است: چگونه می توانیم به تفکر شفاف تری برسیم؟ پاسخ: ما باید مانند دانشمندان فکر کنیم. این یک روش فکری است که در طول 500 سال گذشته به خوبی کار کرده است. در علم ما مدل های ریاضی واقعیت را می سازیم. ستاره شناسی شاید اولین علم به معنای دقیق کلمه بود. در مدل ریاضی مورد استفاده در نجوم، اجرام آسمانی به صورت نقاطی با جرم، موقعیت و تکانه ظاهر می شوند، اگرچه در واقعیت آنها اجرام بسیار پیچیده با کوه ها و اقیانوس ها، جزر و مد هستند. این مدل نیز مانند هر مدل دیگری برای حل مشکلات خاصی ایجاد شده است. اگر می‌خواهید سیاره‌ای پیدا کنید، برای تعیین اینکه تلسکوپ را به کجا بکشید، عالی است. اما اگر بخواهید آب و هوای این سیاره را پیش بینی کنید، این مدل کار نخواهد کرد.
ریاضیات به ما اجازه می دهد تا ویژگی های یک مدل را تعیین کنیم. و علم نشان می دهد که چگونه این ویژگی ها با واقعیت ارتباط دارند. بیایید در مورد علم خود، علم کامپیوتر صحبت کنیم. واقعیتی که ما با آن کار می کنیم انواع سیستم های محاسباتی است: پردازنده ها، کنسول های بازی، رایانه هایی که برنامه ها را اجرا می کنند و غیره. من در مورد اجرای یک برنامه در رایانه صحبت خواهم کرد، اما، به طور کلی، همه این نتایج برای هر سیستم محاسباتی اعمال می شود. ما در علم خود از مدل‌های مختلفی استفاده می‌کنیم: ماشین تورینگ، مجموعه‌هایی از رویدادها و بسیاری موارد دیگر.
برنامه چیه؟ این هر کدی است که می تواند به تنهایی در نظر گرفته شود. فرض کنید باید یک مرورگر بنویسیم. ما سه کار را انجام می دهیم: ارائه برنامه توسط کاربر را طراحی می کنیم، سپس نمودار سطح بالای برنامه را می نویسیم و در نهایت کد را می نویسیم. همانطور که ما کد را می نویسیم، متوجه می شویم که باید یک فرمت کننده متن بنویسیم. در اینجا دوباره باید سه مشکل را حل کنیم: تعیین کنید که این ابزار چه متنی را برگرداند. انتخاب یک الگوریتم برای قالب بندی؛ کد بنویس این کار وظیفه فرعی خود را دارد: قرار دادن خط فاصله در کلمات به درستی. ما همچنین این کار فرعی را در سه مرحله حل می کنیم - همانطور که می بینیم، آنها در سطوح مختلف تکرار می شوند.
بیایید نگاهی دقیق تر به مرحله اول بیندازیم: برنامه چه مشکلی را حل می کند. در اینجا ما اغلب یک برنامه را به عنوان تابعی مدل می کنیم که مقداری ورودی می گیرد و مقداری خروجی می دهد. در ریاضیات، یک تابع معمولاً به عنوان یک مجموعه مرتب شده از جفت ها توصیف می شود. برای مثال، تابع مجذور اعداد طبیعی به صورت مجموعه {<0,0>، <1,1،2,4>، <3,9،XNUMX>، <XNUMX،XNUMX>، …} توصیف می‌شود. دامنه تعریف چنین تابعی مجموعه اولین عناصر هر جفت، یعنی اعداد طبیعی است. برای تعریف تابع باید دامنه و فرمول آن را مشخص کنیم.
اما توابع در ریاضیات با توابع در زبان های برنامه نویسی یکسان نیستند. ریاضی بسیار ساده تر است. از آنجایی که من برای مثال های پیچیده وقت ندارم، بیایید یک مثال ساده را در نظر بگیریم: یک تابع در C یا یک روش استاتیک در جاوا که بزرگترین مقسوم علیه مشترک دو عدد صحیح را برمی گرداند. در مشخصات این روش خواهیم نوشت: محاسبه می کند GCD(M,N) برای استدلال M и Nجایی که GCD(M,N) - تابعی که دامنه آن مجموعه ای از جفت اعداد صحیح است و مقدار بازگشتی آن بزرگترین عدد صحیحی است که تقسیم بر M и N. واقعیت در مقایسه با این مدل چگونه است؟ مدل با اعداد صحیح کار می کند و در C یا جاوا 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 است و با کم کردن متغیر کوچکتر از متغیر بزرگتر، مقدار جدید 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] هر دو قسمت عبارت false خواهد بود، بنابراین حالت بعدی ندارد. بنابراین، ما مشخصات کامل مرحله دوم را داریم - همانطور که می بینیم، این ریاضیات کاملاً معمولی است، مانند ریاضیات مهندسین و دانشمندان، و عجیب نیست، مانند علوم کامپیوتر.
این دو فرمول را می توان در یک فرمول منطق زمانی ترکیب کرد. این ظریف و آسان برای توضیح است، اما در حال حاضر زمانی برای آن وجود ندارد. ما ممکن است فقط برای خاصیت سرزندگی به منطق زمانی نیاز داشته باشیم؛ برای امنیت به آن نیازی نیست. من منطق زمانی را دوست ندارم، ریاضیات کاملاً معمولی نیست، اما در مورد سرزندگی یک شر ضروری است.
در الگوریتم اقلیدسی برای هر مقدار x и y ارزش های منحصر به فردی وجود دارد x' и y'، که رابطه با حالت بعدی را درست می کند. به عبارت دیگر، الگوریتم اقلیدسی قطعی است. برای مدل سازی یک الگوریتم غیر قطعی، وضعیت فعلی باید چندین حالت ممکن آینده داشته باشد، و هر مقدار از متغیر unprimed باید مقادیر متعددی از متغیر اولیه داشته باشد به طوری که رابطه با حالت بعدی درست باشد. انجام این کار دشوار نیست، اما اکنون مثال نمی زنم.
برای ساختن یک ابزار کار، به ریاضیات رسمی نیاز دارید. چگونه یک مشخصات را رسمی کنیم؟ برای انجام این کار به یک زبان رسمی نیاز داریم، به عنوان مثال. . مشخصات الگوریتم اقلیدسی در این زبان به صورت زیر خواهد بود:
علامت مساوی با مثلث به این معنی است که مقدار سمت چپ علامت برابر با مقدار سمت راست علامت تعیین می شود. در اصل، یک مشخصه یک تعریف است، در مورد ما دو تعریف. به مشخصات در TLA+ باید اعلان‌ها و مقداری نحو، مانند اسلاید بالا را اضافه کنید. در ASCII به شکل زیر است:
همانطور که می بینید، هیچ چیز پیچیده ای نیست. مشخصات روی TLA+ را می توان تأیید کرد، به عنوان مثال، امکان دور زدن همه رفتارهای ممکن در یک مدل کوچک وجود دارد. در مورد ما، این مدل مقادیر معینی خواهد بود M и N. این یک روش تأیید بسیار مؤثر و ساده است که کاملاً خودکار است. علاوه بر این، می توان مدارک رسمی صدق را نوشت و آنها را به صورت مکانیکی بررسی کرد، اما این کار زمان زیادی می برد، بنابراین تقریباً هیچ کس این کار را انجام نمی دهد.
عیب اصلی TLA+ ریاضی بودن آن است و برنامه نویسان و دانشمندان کامپیوتر از ریاضیات می ترسند. در نگاه اول این یک شوخی به نظر می رسد، اما، متأسفانه، این را با جدیت کامل می گویم. یکی از همکاران من فقط به من می گفت که چگونه سعی کرد TLA+ را برای چندین توسعه دهنده توضیح دهد. به محض ظاهر شدن فرمول ها روی صفحه، چشمان آنها بلافاصله شیشه ای شد. بنابراین اگر TLA+ ترسناک است، می توانید از آن استفاده کنید ، نوعی زبان برنامه نویسی اسباب بازی است. یک عبارت در PlusCal می تواند هر عبارت TLA+، یعنی اساساً هر عبارت ریاضی باشد. علاوه بر این، PlusCal دارای نحوی برای الگوریتم‌های غیر قطعی است. از آنجایی که PlusCal می تواند هر عبارت TLA+ را بنویسد، به طور قابل توجهی گویاتر از هر زبان برنامه نویسی واقعی است. در مرحله بعد، PlusCal در یک مشخصات TLA+ برای خواندن آسان کامپایل شده است. البته این بدان معنا نیست که مشخصات پیچیده PlusCal در TLA+ به یک ویژگی ساده تبدیل می شود - فقط به این معنی که مطابقت بین آنها واضح است، هیچ پیچیدگی اضافی ظاهر نمی شود. در نهایت، این مشخصات را می توان با استفاده از ابزار TLA+ تأیید کرد. به طور کلی، PlusCal می تواند به غلبه بر فوبیای ریاضیات کمک کند؛ درک آن حتی برای برنامه نویسان و دانشمندان کامپیوتر آسان است. من الگوریتم هایی را برای مدتی (حدود 10 سال) در گذشته بر روی آن منتشر کردم.
شاید کسی اعتراض کند که TLA+ و PlusCal ریاضی هستند و ریاضیات فقط با مثال های ساختگی کار می کند. در عمل شما به یک زبان واقعی با انواع، رویه ها، اشیاء و غیره نیاز دارید. این اشتباه است. در اینجا آنچه کریس نیوکمب، که در آمازون کار می کرد، می نویسد: ما از TLA+ در ده پروژه بزرگ استفاده کرده‌ایم، و در هر مورد استفاده از آن تفاوت قابل‌توجهی در توسعه ایجاد کرد، زیرا توانستیم باگ‌های خطرناک را قبل از شروع تولید پیدا کنیم، و به این دلیل که بینش و اعتماد به نفس لازم برای تهاجمی را به ما داد. بهینه سازی عملکرد بدون تاثیر بر حقیقت برنامه". اغلب می توانید بشنوید که هنگام استفاده از روش های رسمی کد ناکارآمد دریافت می کنیم - در عمل، همه چیز دقیقا برعکس است. علاوه بر این، این تصور وجود دارد که مدیران را نمی‌توان در مورد نیاز به روش‌های رسمی متقاعد کرد، حتی اگر برنامه‌نویسان به مفید بودن آنها متقاعد شوند. و نیوکمب می نویسد: "مدیران اکنون به هر طریق ممکن برای نوشتن مشخصات در TLA+ فشار می آورند و به طور خاص زمان را برای این کار اختصاص می دهند.". بنابراین وقتی مدیران می‌بینند که TLA+ کار می‌کند، آن را در آغوش می‌گیرند. کریس نیوکمب این را حدود شش ماه پیش (اکتبر 2014) نوشت، اما اکنون، تا آنجا که من می دانم، TLA+ در 14 پروژه استفاده می شود، نه 10 پروژه. مثال دیگر مربوط به طراحی XBox 360 است. یک کارآموز به چارلز تاکر آمد و مشخصات سیستم حافظه را نوشت. به لطف این مشخصات، باگی پیدا شد که در غیر این صورت شناسایی نمی شد و باعث می شد هر XBox 360 پس از چهار ساعت استفاده از کار بیفتد. مهندسان IBM تأیید کردند که آزمایشات آنها این باگ را شناسایی نکرده است.
شما می توانید اطلاعات بیشتری در مورد TLA+ در اینترنت بخوانید، اما اکنون اجازه دهید در مورد مشخصات غیر رسمی صحبت کنیم. به ندرت مجبور می شویم برنامه هایی بنویسیم که کمترین مقسوم علیه مشترک و مانند آن را محاسبه کنند. اغلب ما برنامه هایی مانند ابزار چاپگر زیبا که برای TLA+ نوشتم می نویسیم. پس از ساده ترین پردازش، کد TLA+ به شکل زیر خواهد بود:
اما در مثال بالا، کاربر به احتمال زیاد می‌خواست علامت‌های ربط و مساوی در یک راستا قرار گیرند. بنابراین قالب بندی صحیح بیشتر شبیه این خواهد بود:
مثال دیگری را در نظر بگیرید:
در اینجا، برعکس، تراز علائم مساوی، جمع و ضرب در منبع تصادفی بود، بنابراین ساده ترین پردازش کاملاً کافی است. به طور کلی، هیچ تعریف ریاضی دقیقی از قالب بندی صحیح وجود ندارد، زیرا "درست" در این مورد به معنای "آنچه کاربر می خواهد" است و این را نمی توان از نظر ریاضی تعیین کرد.
به نظر می رسد اگر ما تعریفی از صدق نداشته باشیم، آنگاه تصریح بی فایده است. اما این درست نیست. فقط به این دلیل که نمی دانیم یک برنامه باید چه کاری انجام دهد، به این معنی نیست که نیازی به فکر کردن در مورد نحوه عملکرد آن نداریم - برعکس، ما باید تلاش بیشتری را برای آن صرف کنیم. مشخصات در اینجا بسیار مهم است. تعیین برنامه بهینه برای چاپ ساختاریافته غیرممکن است، اما این بدان معنا نیست که اصلاً نباید آن را انجام دهیم و نوشتن کد به عنوان یک جریان آگاهی چنین نیست. من در نهایت به نوشتن مشخصاتی از شش قانون با تعاریف پایان دادم در قالب نظرات در یک فایل جاوا در اینجا مثالی از یکی از قوانین آمده است: a left-comment token is LeftComment aligned with its covering token. این قانون به زبان انگلیسی ریاضی نوشته شده است: LeftComment aligned, left-comment и covering token - اصطلاحات با تعاریف ریاضیدانان ریاضیات را اینگونه توصیف می کنند: آنها تعاریف اصطلاحات را می نویسند و بر اساس آنها قوانینی را ایجاد می کنند. مزیت این مشخصات این است که درک و اشکال زدایی شش قانون بسیار ساده تر از 850 خط کد است. باید بگویم که نوشتن این قوانین آسان نبود؛ رفع اشکال آنها زمان زیادی را صرف کرد. من کدی را به طور خاص برای این منظور نوشتم که به من گفت از کدام قانون استفاده می شود. از آنجایی که من این شش قانون را با چند مثال آزمایش کردم، مجبور نبودم 850 خط کد را اشکال زدایی کنم، و پیدا کردن اشکالات بسیار آسان بود. جاوا ابزارهای بسیار خوبی برای این کار دارد. اگر فقط کد می نوشتم خیلی بیشتر طول می کشید و قالب بندی کیفیت پایین تری داشت.
چرا نمی توان از مشخصات رسمی استفاده کرد؟ از یک طرف، اجرای صحیح در اینجا خیلی مهم نیست. چاپ ساختاریافته برای برخی ناخوشایند است، بنابراین من مجبور نبودم آن را در همه موقعیت‌های غیرعادی به درستی کار کنم. حتی مهمتر این واقعیت است که من ابزار کافی نداشتم. جستجوگر مدل TLA+ در اینجا بی فایده است، بنابراین باید نمونه ها را با دست بنویسم.
مشخصات داده شده دارای ویژگی های مشترک در تمام مشخصات است. سطح آن بالاتر از کد است. می توان آن را به هر زبانی پیاده سازی کرد. هیچ ابزار یا روشی برای نوشتن آن وجود ندارد. هیچ دوره برنامه نویسی به شما در نوشتن این مشخصات کمک نمی کند. و هیچ ابزاری وجود ندارد که بتواند این مشخصات را غیرضروری کند، مگر اینکه در حال نوشتن یک زبان به طور خاص برای نوشتن برنامه های پرینت ساخت یافته در TLA+ هستید. در نهایت، این مشخصات چیزی در مورد نحوه نوشتن کد دقیقاً بیان نمی کند، فقط بیان می کند که کد چه کاری انجام می دهد. ما یک مشخصات می نویسیم تا به ما کمک کند قبل از شروع به فکر کردن درباره کد، مشکل را بررسی کنیم.
اما این مشخصات ویژگی هایی نیز دارد که آن را از سایر مشخصات متمایز می کند. 95% سایر مشخصات بسیار کوتاه تر و ساده تر هستند:
علاوه بر این، این مشخصات مجموعه ای از قوانین است. این معمولاً نشانه ای از مشخصات ضعیف است. درک عواقب مجموعه ای از قوانین بسیار دشوار است، به همین دلیل است که مجبور شدم زمان زیادی را برای رفع اشکال آنها صرف کنم. با این حال، در این مورد من نتوانستم راه بهتری پیدا کنم.
شایان ذکر است که در مورد برنامه هایی که به طور مداوم اجرا می شوند، چند کلمه صحبت کنید. به طور معمول آنها به صورت موازی عمل می کنند، مانند سیستم عامل یا سیستم های توزیع شده. افراد بسیار کمی می توانند آنها را در ذهن یا روی کاغذ درک کنند و من یکی از آنها نیستم، اگرچه زمانی توانستم این کار را انجام دهم. بنابراین، ما به ابزارهایی نیاز داریم که کار ما را بررسی کنند - به عنوان مثال، TLA+ یا PlusCal.
اگر از قبل می دانستم کد باید چه کاری انجام دهد، چرا باید مشخصات بنویسم؟ در واقع، من فقط فکر می کردم که آن را می دانم. علاوه بر این، با وجود یک مشخصات، یک فرد خارجی دیگر نیازی به بررسی کد ندارد تا بفهمد دقیقا چه کاری انجام می دهد. من یک قانون دارم: هیچ قانون کلی نباید وجود داشته باشد. البته یک استثنا برای این قاعده وجود دارد، این تنها قاعده کلی است که من از آن پیروی می‌کنم: مشخصات کاری که کد انجام می‌دهد باید همه چیزهایی را که باید هنگام استفاده از آن کد بدانند به مردم بگوید.
بنابراین برنامه نویسان دقیقاً چه چیزی باید در مورد تفکر بدانند؟ برای شروع، مانند همه: اگر نمی نویسید، فقط به نظر شما می رسد که فکر می کنید. همچنین، شما باید قبل از کدنویسی فکر کنید، به این معنی که قبل از کدنویسی باید بنویسید. مشخصات چیزی است که قبل از شروع کدنویسی می نویسیم. یک مشخصات برای هر کدی که می تواند توسط هر کسی استفاده یا تغییر کند مورد نیاز است. و این "کسی" ممکن است یک ماه پس از نوشتن کد، نویسنده کد باشد. یک مشخصات برای برنامه‌ها و سیستم‌های بزرگ، برای کلاس‌ها، برای متدها و گاهی حتی برای بخش‌های پیچیده یک متد مورد نیاز است. دقیقاً در مورد کد چه چیزی باید بنویسید؟ باید توضیح دهید که چه کاری انجام می دهد، یعنی چیزی که می تواند برای هر کسی که از این کد استفاده می کند مفید باشد. گاهی اوقات نیز ممکن است لازم باشد مشخص شود که کد دقیقا چگونه به هدف خود می رسد. اگر در درس الگوریتم ها از این روش گذشتیم، آن را الگوریتم می نامیم. اگر چیزی تخصصی تر و جدیدتر باشد، آن را طراحی سطح بالا می نامیم. در اینجا هیچ تفاوت رسمی وجود ندارد: هر دو مدل های انتزاعی برنامه هستند.
دقیقاً چگونه باید مشخصات کد بنویسید؟ نکته اصلی: باید یک سطح بالاتر از خود کد باشد. باید حالت ها و رفتارها را توصیف کند. باید به همان اندازه که کار ایجاب می کند سختگیرانه باشد. اگر در حال نوشتن مشخصاتی درباره نحوه اجرای یک کار هستید، می توان آن را با کد شبه یا با استفاده از PlusCal نوشت. شما باید یاد بگیرید که مشخصات را با استفاده از مشخصات رسمی بنویسید. این به شما مهارت های لازم را می دهد که در مورد غیر رسمی نیز کمک خواهد کرد. چگونه می توانید یاد بگیرید که مشخصات رسمی بنویسید؟ وقتی برنامه نویسی را یاد گرفتیم، برنامه ها را می نوشتیم و سپس آنها را دیباگ می کردیم. همین مورد در اینجا: شما باید یک مشخصات بنویسید، آن را با یک مدل بررسی کنید و خطاها را برطرف کنید. TLA+ ممکن است بهترین زبان برای مشخصات رسمی نباشد و زبان دیگری احتمالاً برای نیازهای خاص شما مناسب تر است. نکته مهم در مورد TLA+ این است که کار بسیار خوبی در آموزش تفکر ریاضی انجام می دهد.
چگونه مشخصات و کد را لینک کنیم؟ استفاده از نظراتی که مفاهیم ریاضی و اجرای آنها را به هم مرتبط می کند. اگر با نمودارها کار می کنید، در سطح برنامه، آرایه هایی از گره ها و آرایه هایی از پیوندها خواهید داشت. بنابراین باید بنویسید که چگونه نمودار توسط این ساختارهای برنامه نویسی دقیقا پیاده سازی می شود.
لازم به ذکر است که هیچ یک از موارد فوق در مورد فرآیند نوشتن کد صدق نمی کند. زمانی که کد می نویسید، یعنی مرحله سوم را انجام می دهید، باید به برنامه فکر کنید و فکر کنید. اگر یک کار فرعی پیچیده یا واضح نیست، باید مشخصاتی برای آن بنویسید. اما من در مورد خود کد اینجا صحبت نمی کنم. شما می توانید از هر زبان برنامه نویسی، هر متدولوژی استفاده کنید، این مربوط به آنها نیست. همچنین هیچ یک از موارد فوق نیاز به تست و اشکال زدایی کد شما را برطرف نمی کند. حتی اگر مدل انتزاعی به درستی نوشته شده باشد، ممکن است اشکالاتی در اجرای آن وجود داشته باشد.
نوشتن مشخصات یک مرحله اضافی در فرآیند کدگذاری است. به لطف آن، بسیاری از خطاها را می توان با تلاش کمتر شناسایی کرد - ما این را از تجربه برنامه نویسان آمازون می دانیم. با مشخصات، کیفیت برنامه ها بالاتر می رود. پس چرا ما اغلب بدون آنها می رویم؟ چون نوشتن سخت است. اما نوشتن دشوار است، زیرا برای این کار باید فکر کرد و فکر کردن نیز دشوار است. همیشه راحت تر است وانمود کنید که دارید فکر می کنید. در اینجا می توان یک قیاس با دویدن داشت - هر چه کمتر بدوید، کندتر می دوید. باید عضلات خود را تمرین دهید و نوشتن را تمرین کنید. این نیاز به تمرین دارد.
ممکن است مشخصات نادرست باشد. ممکن است جایی مرتکب اشتباه شده باشید، یا شرایط ممکن است تغییر کرده باشد، یا ممکن است نیاز به بهبود باشد. هر کدی که هر کسی استفاده می کند باید تغییر کند، بنابراین دیر یا زود مشخصات دیگر با برنامه مطابقت نخواهد داشت. در حالت ایده آل، در این مورد، باید مشخصات جدیدی بنویسید و کد را به طور کامل بازنویسی کنید. ما به خوبی می دانیم که هیچ کس این کار را نمی کند. در عمل ما کد را وصله می کنیم و شاید مشخصات را به روز می کنیم. اگر قرار است دیر یا زود این اتفاق بیفتد، پس چرا اصلاً مشخصات بنویسید؟ اولاً، برای شخصی که کد شما را ویرایش می کند، هر کلمه اضافی در مشخصات به ارزش طلا خواهد بود و این شخص ممکن است شما باشید. من اغلب به خودم لگد می زنم که وقتی کدم را ویرایش می کنم به اندازه کافی دقیق نیستم. و بیشتر مشخصات می نویسم تا کد. بنابراین، زمانی که کد را ویرایش می کنید، مشخصات همیشه نیاز به به روز رسانی دارد. ثانیا، با هر ویرایش کد بدتر می شود، خواندن و نگهداری آن دشوارتر می شود. این افزایش آنتروپی است. اما اگر با مشخصاتی شروع نکنید، هر خطی که می نویسید ویرایش خواهد بود و کد از همان ابتدا حجیم و خواندن آن سخت خواهد بود.
همانطور که گفته شد , هیچ نبردی بر اساس نقشه پیروز نشد و هیچ نبردی بدون برنامه پیروز نشد. و او چیزی در مورد نبردها می دانست. نظری وجود دارد که نوشتن مشخصات اتلاف وقت است. گاهی اوقات این درست است، و کار به قدری ساده است که فکر کردن به آن هیچ فایده ای ندارد. اما همیشه باید به یاد داشته باشید که وقتی به شما توصیه می شود مشخصات ننویسید به این معنی است که به شما توصیه می شود فکر نکنید. و هر بار باید به این موضوع فکر کنید. فکر کردن از طریق یک کار تضمین نمی کند که شما اشتباه نکنید. همانطور که می دانیم، هیچ کس عصای جادویی را اختراع نکرد و برنامه نویسی کار دشواری است. اما اگر به کار فکر نکنید، مطمئناً اشتباه خواهید کرد.
می توانید اطلاعات بیشتری در مورد TLA+ و PlusCal در یک وب سایت ویژه بخوانید، می توانید از صفحه اصلی من به آنجا بروید . این همه برای من است، از توجه شما متشکرم.
لطفا به یاد داشته باشید که این یک ترجمه است. هنگام نوشتن نظرات، به یاد داشته باشید که نویسنده آنها را نخواهد خواند. اگر واقعاً می خواهید با نویسنده چت کنید، او در کنفرانس Hydra 2019 خواهد بود که در تاریخ 11-12 ژوئیه 2019 در سن پترزبورگ برگزار می شود. بلیط را می توان خریداری کرد .
منبع: www.habr.com