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

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

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

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

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

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

تعریف

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

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

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

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

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

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

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

چهار فایده

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

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

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

محدودیت

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

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

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

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

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

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

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

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

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

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

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

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

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

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

در بافت فارسی

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

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

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

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

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

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

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

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

جمع‌بندی

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