منبع: بنیاد طراحی تعامل (IxDF) · بازنویسی آزاد: سپنتا پویا · ترجمه: ۶ شهریور ۱۴۰۵ · زمان مطالعه: حدود ۱۰ دقیقه

روش‌های صوری (Formal Methods) چیست؟

💡 این متن «بازنویسی آزاد» است: ایده‌ها و مفاهیم مطلب اصلی با نگارش کاملاً مستقل فارسی و مثال‌های تازه بازگو شده‌اند و ترجمهٔ کلمه‌به‌کلمه نیست. بخش‌های افزودهٔ مترجم در جعبهٔ منبع مشخص شده‌اند.

«بعد از سه بار ورود ناموفق، حساب قفل می‌شود.» این جمله روشن به‌نظر می‌رسد و نیست.

سه بار پشت سر هم یا سه بار در کل؟ شمارنده کِی صفر می‌شود؟ ورود موفق میان دو شکست چه اثری دارد؟ قفل تا کِی؟

روش‌های صوری برای همین ساخته شده‌اند: نوشتن مشخصات به زبانی که این پرسش‌ها را نمی‌شود در آن بی‌جواب گذاشت.

تعریف

روش‌های صوری تکنیک‌هایی هستند که سیستم‌های پیچیده را به‌عنوان موجودیت‌های ریاضی مدل می‌کنند.

یعنی به‌جای توصیف رفتار سیستم با جملهٔ فارسی یا انگلیسی، آن را با نحو و معنای ریاضی می‌نویسید.

و آلن دیکس، استاد رایانش در دانشگاه لنکستر، از مرجع‌های این حوزه در تعامل انسان و رایانه است.

سه چیزی که مدل می‌شود

در تعامل انسان و رایانه، سه دستهٔ چیز را می‌شود صوری کرد.

• - کاربر. تعامل‌ها در سطح کاربر — با سیستم‌های مدل‌سازی وظیفه.
• - سیستم. فرایندهای پشت صحنه و رفتاری که دیده نمی‌شود.
• - جهان. بافت فیزیکی و عامل‌های محیطی.

و دستهٔ سوم آنی است که معمولاً فراموش می‌شود. بیشتر مشخصات فقط سیستم را توصیف می‌کنند، انگار در خلأ اجرا می‌شود.

و پیامدش را همه دیده‌ایم. مشخصاتی که می‌گوید «کاربر کد را وارد می‌کند» فرض کرده کاربر پیامک را می‌بیند، گوشی‌اش شارژ دارد، آنتن دارد، و در همان لحظه کار دیگری نمی‌کند.

هیچ‌کدام از این‌ها در سند نیامده‌اند و همه‌شان می‌توانند نقض شوند. و وقتی نقض می‌شوند، سیستم از نظر خودش درست کار کرده — فقط کاربر نتوانسته کارش را تمام کند.

و همین است که مدل‌کردن «جهان» را از یک تشریفات دانشگاهی به یک ابزار عملی تبدیل می‌کند: بیشتر شکست‌های واقعی، نقض فرض‌های نانوشته دربارهٔ محیط‌اند، نه باگ در منطق.

چهار فایده

• - وارسی رفتار سیستم با اثبات ریاضی.
• - رفع ابهام از مشخصات و آشکارکردن فرض‌های ضمنی.
• - کشف نقص پیش از پیاده‌سازی، که جلوی خطای پرهزینه را می‌گیرد.
• - امکان وارسی مستقل از سوی همکار دیگر.

و فایدهٔ دوم بیشترین ارزش را برای طراح دارد، حتی اگر هیچ اثباتی ننویسید.

چون فرض ضمنی وقتی آشکار می‌شود که مجبور شوید صریح بنویسیدش. همان مثال قفل حساب: تا وقتی جمله را فارسی می‌نویسید، «سه بار» ابهامش را پنهان می‌کند.

و این را می‌شود در یک تمرین کوچک تجربه کرد. همان جملهٔ قفل حساب را بردارید و سعی کنید بدون هیچ ابهامی بازنویسی‌اش کنید.

و خیلی زود می‌بینید که باید چند تصمیم بگیرید:

• - شمارنده کجا نگه‌داری می‌شود؟
• - با ورود موفق صفر می‌شود یا نه؟
• - پس از چه مدتی خودش صفر می‌شود؟
• - قفل چقدر طول می‌کشد؟
• - و در طول قفل، تلاش تازه شمارنده را دوباره پر می‌کند؟

و هیچ‌کدام از این تصمیم‌ها تا لحظه‌ای که مجبور به نوشتنشان نشده بودید، وجود نداشتند. آن‌ها را کسی حذف نکرده بود؛ اصلاً گرفته نشده بودند.

و در عمل، همین تصمیم‌ها بعداً در کد گرفته می‌شوند — از سوی کسی که سریع‌ترین راه را انتخاب می‌کند، و بی آنکه بداند دارد یک تصمیم محصولی می‌گیرد.

محدودیت

منبع صریح است: روش‌های صوری نمی‌توانند به‌طور کامل جایگزین روش‌های متعارف تضمین کیفیت شوند. این‌ها مکمل‌اند، نه جانشین.

و سه محدودیت عملی هم دارند که ارزش گفتن دارد.

• - هزینهٔ یادگیری. نوشتن مشخصات صوری مهارتی است که تیم‌های محصول معمولاً ندارند.
• - مدل، واقعیت نیست. اثبات می‌کند مدل درست است، نه اینکه مدل درست را ساخته‌اید.
• - بخش انسانی مدل نمی‌شود. می‌توانید ثابت کنید سیستم هرگز حالت نامعتبر نمی‌گیرد و نمی‌توانید ثابت کنید کاربر می‌فهمد چه خبر است.

نسخهٔ سبکش، که به کار طراح می‌آید

این بخش افزودهٔ من است، چون بیشتر تیم‌های محصول هرگز مشخصات ریاضی نخواهند نوشت — و باز می‌توانند بیشتر فایده را بگیرند.

هستهٔ روش‌های صوری یک ایده است: هر حالت ممکن را نام ببرید و برای هر رویداد بگویید از هر حالت به کدام حالت می‌رود.

و همین را می‌شود با یک جدول ساده انجام داد. سطرها حالت‌ها، ستون‌ها رویدادها، و هر خانه حالت بعدی.

و خانه‌های خالی همان چیزی هستند که دنبالش بودید: ترکیب‌هایی که هیچ‌کس به آن‌ها فکر نکرده.

مثالش را همه دیده‌ایم. کاربر در حالت «در انتظار پرداخت» دکمهٔ بازگشت مرورگر را می‌زند. این خانه در هیچ سندی پر نشده، و در محصول واقعی به دو بار کسر وجه ختم می‌شود.

همان‌طور که در فلوچارت نوشتم، شاخهٔ کشیده‌نشده همان جایی است که کاربر گیر می‌کند. جدول حالت، همان آزمون را روی رفتار سیستم اجرا می‌کند.

و پرکردن این جدول یک فایدهٔ جانبی هم دارد که اغلب بزرگ‌تر از فایدهٔ اصلی است: مجبورتان می‌کند حالت‌ها را نام‌گذاری کنید.

در بیشتر محصول‌ها، حالت‌ها نام ندارند. تیم می‌گوید «وقتی کاربر پرداخت کرده ولی هنوز تأیید نشده» — یک توصیف نه‌کلمه‌ای که هر بار کمی فرق می‌کند. و همان ابهام کوچک، در سه تیم متفاوت به سه پیاده‌سازی متفاوت ختم می‌شود.

وقتی همان حالت را «در انتظار تأیید درگاه» بنامید، چیز تازه‌ای ساخته‌اید. یک واژه که همه می‌توانند دربارهٔ آن دقیق حرف بزنند — در جلسه، در تیکت، در لاگ، و در پیام خطایی که کاربر می‌بیند.

کِی ارزشش را دارد

صوری‌کردن هزینه دارد، پس همه‌جا موجه نیست. سه نشانه هست که ارزشش را دارد:

• - خطا برگشت‌ناپذیر است. پول، دارو، هویت، حذف داده.
• - حالت‌ها زیادند و در هم می‌روند. اشتراک و مهلت و تخفیف و لغو و بازگشت وجه، همه با هم.
• - چند تیم باید یک فهم مشترک داشته باشند. مشخصات مبهم اینجا دو پیاده‌سازی متفاوت می‌سازد.

و اگر هیچ‌کدام برقرار نیست، همان جدول حالت ساده کافی است.

و در طرف مقابل، سه نشانه هم هست که می‌گوید سراغش نروید.

هنوز نمی‌دانید چه می‌سازید. صوری‌کردن یک ایدهٔ متزلزل، فقط ابهام را با دقت بیشتری می‌نویسد. اینجا نمونهٔ اولیه ارزان‌تر از سند است.

محصول کوچک است و یک نفر همه‌اش را در سر دارد. هزینهٔ نوشتن اینجا واقعی است و فایده‌اش صفر — تا روزی که نفر دوم اضافه شود.

و قاعده‌ها هفته‌به‌هفته عوض می‌شوند. سندی که با هر تغییر بی‌اعتبار می‌شود، خیلی زود کسی به‌روزش نمی‌کند — و سند به‌روزنشده بدتر از نبودِ سند است، چون آدم‌ها به آن اعتماد می‌کنند.

کجا سراغ حالت‌ها برویم

و اگر می‌خواهید از یک جای مشخص شروع کنید، چهار جا در هر محصولی هست که تقریباً همیشه حالت‌های نام‌نگرفته دارند.

پول. پرداخت، بازگشت وجه، پرداخت ناقص، پرداخت دوباره، مبلغ نادرست. اینجا هر حالت جاافتاده مستقیم به پول واقعی وصل است.

هویت. ثبت‌نام نیمه‌کاره، شمارهٔ تکراری، حساب تأییدنشده، حسابی که کاربر دیگر به شماره‌اش دسترسی ندارد. این آخری در هیچ سندی نیست و در پشتیبانی هر محصولی هست.

زمان. مهلت، انقضا، تمدید، دورهٔ آزمایشی. حالت‌های زمانی به این دلیل جا می‌افتند که هیچ کاربری آن‌ها را «انجام» نمی‌دهد — خودشان اتفاق می‌افتند.

و هم‌زمانی. دو دستگاه، دو زبانه، دو کاربر روی یک سفارش. این دسته سخت‌ترین است، چون در آزمون دستی تقریباً هرگز بروز نمی‌کند و در محصول واقعی هر روز.

و یک قاعدهٔ کلی هم پشت هر چهارتاست: حالت‌هایی جا می‌افتند که کاربر آن‌ها را انتخاب نمی‌کند. هر چیزی که «اتفاق می‌افتد» — مهلت تمام می‌شود، شبکه قطع می‌شود، سرویس دیگری دیر جواب می‌دهد — کمتر از چیزی که کاربر روی آن کلیک می‌کند در سند دیده می‌شود.

در بافت فارسی

یک: مشخصات اینجا اغلب شفاهی است. بسیاری از تصمیم‌ها در جلسه گرفته می‌شوند و جایی نوشته نمی‌شوند.

پس پیش از هر صوری‌سازی، یک قدم ساده‌تر لازم است: نوشتنِ اصلاً. بیشتر ابهام‌های ما از پیچیدگی نمی‌آید؛ از نبودِ سند می‌آید.

دو: قاعده‌های بیرونی مدام عوض می‌شوند. سقف تراکنش، الزام احراز هویت، قاعدهٔ درگاه پرداخت. چیزی که امروز صوری کرده‌اید، شش ماه دیگر معتبر نیست.

و نتیجه‌اش این نیست که کار بی‌فایده است. یعنی قاعده‌های متغیر را از منطق ثابت جدا نگه دارید — عددها در یک جا، رفتار در جای دیگر.

سه: تاریخ و تقویم، منبع خطای صوری واقعی است. «سی روز» در تقویم شمسی با ماه شمسی یکی نیست، و ماه‌های اول سال ۳۱ روزه‌اند.

پس هر جا مهلت و اشتراک و دورهٔ آزمایشی دارید، مشخص کنید واحد «روز» است یا «ماه» — و اگر ماه است، کدام تقویم. این دقیقاً همان ابهامی است که روش صوری برای گرفتنش ساخته شده.

چهار: چند سامانهٔ بیرونی، حالت‌های اضافه می‌سازند. درگاه پرداخت، سرویس پیامک، استعلام هویت. هر کدام می‌توانند کند باشند، خطا بدهند، یا جواب مبهم برگردانند.

و همان‌طور که در خطای انسانی نوشتم، بیشتر خرابی‌های واقعی در همین مرزها اتفاق می‌افتند. حالت «نمی‌دانم» را هم یک حالت رسمی بشمارید، نه یک استثنا.

و «نمی‌دانم» را جدی‌گرفتن یک پیامد طراحی هم دارد، نه فقط پیامد فنی.

سیستمی که فقط دو حالت «موفق» و «ناموفق» دارد، در لحظهٔ بلاتکلیفی مجبور است یکی از این دو را دروغ بگوید. و هر دو دروغ گران‌اند: «ناموفق» کاربر را وامی‌دارد دوباره پرداخت کند، و «موفق» تعهدی می‌سازد که ممکن است پشتش پولی نباشد.

و پاسخ درست، حالت سومی است که هم در سیستم و هم در رابط وجود داشته باشد: «در حال بررسی — تا چند دقیقهٔ دیگر نتیجه را می‌گوییم.»

و نوشتن همین یک حالت در سند، معمولاً بیشتر از هر اثبات ریاضی‌ای از کاربر محافظت می‌کند.

جمع‌بندی

• - روش‌های صوری سیستم‌های پیچیده را به‌عنوان موجودیت ریاضی مدل می‌کنند · با نحو و معنای ریاضی به‌جای جملهٔ زبان طبیعی
• - سه چیز مدل می‌شود: کاربر با مدل‌سازی وظیفه · سیستم و رفتار پشت صحنه · و جهان یعنی بافت فیزیکی و محیط، که معمولاً فراموش می‌شود
• - چهار فایده: وارسی با اثبات · رفع ابهام و آشکارکردن فرض ضمنی · کشف نقص پیش از پیاده‌سازی · و وارسی مستقل
• - فایدهٔ دوم حتی بی هیچ اثباتی ارزش دارد · فرض ضمنی وقتی آشکار می‌شود که مجبور شوید صریح بنویسیدش
• - جایگزین تضمین کیفیت متعارف نیستند · و سه محدودیت دارند: هزینهٔ یادگیری · مدل واقعیت نیست · و بخش انسانی مدل نمی‌شود
• - نسخهٔ سبکش: جدول حالت‌ها و رویدادها · و خانه‌های خالی همان ترکیب‌هایی‌اند که کسی به آن‌ها فکر نکرده
• - ارزشش را دارد وقتی خطا برگشت‌ناپذیر است · حالت‌ها در هم می‌روند · یا چند تیم باید فهم مشترک داشته باشند
• - و در فارسی: اول اصلاً بنویسید · قاعده‌های متغیر را از منطق ثابت جدا کنید · واحد مهلت و تقویمش را مشخص کنید · و «نمی‌دانم» را یک حالت رسمی بشمارید