موضوع مقاله: تفسیر انتزاعی | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # تفسیر انتزاعی | مقدمه: در علوم کامپیوتر تفسیر انتزاعی یک تیوری تقریب صدا از معنای بزنامه‌های کامپیوتر بر مبنای توابع یکنواخت بر روی مجموعه‌های مرتب به ویژه شبکه‌ها می‌باشد که می‌تواند به صورت یک بخش اجرایی از یک برنامه کامپیوتری که اطلاعات معنایی (مثل کنترل معلق یا داده معلق و ..)را بدون انجام همه محاسبات جمع‌آوری می‌کند باشد. | ## بخش 1: تفسیر انتزاعی | هدف اصلی برنامه آنالیز استاتیک رسمی، یک نمایش خودکار اطلاعات از خروجی‌های احتمالی برنامه‌های کامپیوتری است. این تحلیل‌ها دو کاربرد اساسی دارند: در داخل کامپایلرها، برای تجزیه و تحلیل برنامه‌ها که تصمیم بگیرید آیا بعضی بهینه‌سازی‌ها یا تحولات مناسب هستند یا خیر. تفسیر انتزاعی توسط دو شریک علوم کامپیوتر فرانسوی، پاتریک کوسوت و رادیا کوسوت در اواخر دهه ۱۹۷۰ رسمیت یافت. بینش این بخش تفسیر انتزاعی را به وسیله رویدادهای دنیای واقعی بدون مثال‌های محاسباتی نمایش می‌دهد. یک شناسه منحصر به فرد برای هر شخص در اتاق، مانند شماره تأمین اجتماعی در ایالات متحده، در نظر بگیرید. از آنجا که دو نفر مختلف نمی‌توانند یکسان باشند، می‌توان به سادگی با جستجوی شماره هر شرکت کننده، حضور یک شرکت کننده را اثبات یا رد کرد. فرض کنید فقط نام شرکت کنندگان ثبت شده باشد اگر نام شخص در لیست نباشد، با اطمینان می‌توان گفت که آن شخص حضور نداشته. اما به دلیل احتمال مشابهت نام‌ها (به عنوان مثال، دو نفر به نام جان اسمیت) نمی‌توانیم بدون تحقیق بیشتر حضور افراد را نتیجه بگیریم. این اطلاعات نادقیق هنوز برای بیشتر هدف‌ها کافیست، جون مشابهت اسم احتمال کمی دارد. با این وجود تنها چیزی که می‌توانیم بگوییم این است که فرد احتمالاً این‌جا حضور داشته‌است. اگر ما فقط به برخی از اطلاعات خاص نیاز داشته باشیم، مثلاً در پرسش "آیا شخصی با سن n در اتاق وجود داشته‌است؟"، نگه داشتن لیستی از همه اسامی و تاریخ تولدها ضروری نیست. ما می‌توانیم بدون از دست دادن دقت، به نگه داشتن لیستی از سن شرکت کنندگان اکتفا کنیم. اگر سؤال در مورد سنی است که به‌طور متوسط کمتر از m یا بالاتر از M است، بنابراین با اطمینان می‌توانیم پاسخ دهیم که هیچ شرکت کننده ای حضور نداشته‌است. در مورد محاسبات دقیق که در زمان و حافظه محدود قابل محاسبه نیست (به قضیه رایس و مشکل متوقف کردن مراجعه کنید) از انتزاع استفاده می‌شود تا پاسخ‌های تعمیم یافته مثل شاید را برای سوالاتی که جواب قطعی بله یا قطعاً خیر را نمی‌دانیم به عنوان "بله یا خیر "بسازیم. وقتی که الگوریتم تفسیر انتزاعی نمی‌تواند جواب دقیق را با قطعیت محاسبه کند این روش مشکلات را ساده‌تر می‌کند و برای آنها راه حل‌های خودکار می‌سازد. | ## بخش 2: تفسیر انتزاعی | یک شرط اساسی برای ساختن جواب مبهم این است که بتواند مشکلات را کنترل کند و در عین حال دقت کافی را برای پاسخ به سؤالات مهم حفظ کند (مانند "ممکن است برنامه خراب باشد؟") تفسیر انتزاعی از برنامه‌های رایانه ای در یک زبان برنامه‌نویسی مشخص، تفسیر انتزاعی شامل ارائه چندین رابطه معناشناسی مرتبط با روابط انتزاعی می‌باشد. دقیق‌ترین معناشناسی، که اجرای برنامه را بسیار دقیق توصیف می‌کند، معناشناسی دقیق نامیده می‌شود. مثلاً، معناشناسی دقیق یک زبان برنامه‌نویسی ضروری برای هر برنامه شامل خروجی‌هایی می‌شود که هر برنامه تولید می‌کند. معمولاً از مقدار پیشخوان برنامه و مکان‌های حافظه (گلوبال‌ها، پشته‌ها و صف‌ها) تشکیل شده‌است. مثلاً، ممکن است فقط یک دسته از حالت‌های قابل دستیابی در اجراهاها در نظر گرفته شود (که در نظر گرفتن آخرین حالت‌ها در آثار محدود) است. بمثلا، ممکن است برای تغییر متغیرهای عددی تنها با نگه داری علائم متغیرها (+، یا ۰) وضعیتشان را دستکاری کند. برای برخی از عملیات ابتدایی، مانند ضرب، چنین انتزاعی هیچ دقتی را از دست نمی‌دهد: برای به دست آوردن علامت یک محصول، شناختن علامت عملوندها کافی است. برای برخی از عملیات‌های دیگر ، انتزاع ممکن است دقت را از دست بدهد: برای مثال، نمی‌توان از علامت مبلغی که عملکرد آن‌ها به ترتیب مثبت و منفی باشند، ناممکن است. در بعضی مواقع برای دست یابی به یک تفسیر معنایی تصمیم پذیر لازم است دقت را کاهش دهیم (نگاه کنید به قضیه رایس، مشکل متوقف کردن). به‌طور کلی، بین دقت آنالیز و تعیین پذیری آن (محاسبه) یا قابلیت تراکم پذیری (هزینه محاسباتی) باید سازش ایجاد شود. در عمل انتزاعات باید متناسب با هر دو هدف یک برنامه کامپیوتری یعنی تحزیه و تحلیل و مجموعه ای هدفمند بون باشد. اولین تجزیه خودکار مقیاس بزرگ برنامه‌های کامپیوتری به وسیله تفسیر انتزاعی را می‌توان یک اتفاق تصادفی دانست که منجر به تخریب اولین پرواز موشک Ariane 5 در سال ۱۹۹۶ شد. این دو مجموعه L و L' با تعریف توابع کل که عناصر توابع را از یکی به دیگری ترسیم می‌کند، به یکدیگر مرتبط می‌شوند. تابع α یک تابع انتزاع است اگر عنصر x را از مجموعهٔ دقیق L به عنصر (x)α را در مجموعه L ′ تصویر کند. تابع γ d یک تابع دقیق گفته می‌شوداگر عنصر x ′ در مجموعه انتزاعی L ′ به یک عنصر γ (x ′) در مجموعه دقیق L ترسیم شود .. | ## بخش 3: تفسیر انتزاعی | تابع f ′ L ′ تا ′ 2 انتزاع معتبر از f نامیده می‌شود اگر برای هر x ′ L ′ (f ∘ γ x′) ≤ (γ ∘ f′ x′) معناشناسی برنامه را به‌طور کلی می‌توان به وسیله نقاط ثابت در حضور حلقه‌ها یا روش‌های بازگشتی توصیف کرد. اگر L ′ از ارتفاع محدود، یا حداقل تأیید شرایط زنجیره صعودی (تمام دنباله صعودی در نهایت ثابت هستند)، در این صورت مقداری به عنوان حد ثابت از دنباله صعودی دست آمده به نام x' بصرت زیر وجود دارد: x ′ 0 = ⊥ (کمترین عنصرL ′)n) و x′n+1=f′(x′n). در موارد دیگر یافتن این x ′ از طریق اپراتور گسترده‌ای ممکن است ∇: برای همه x و y , x y باید بزرگتر مساوی x و y باشد و برای هر رشته y ′ n، دنباله ای است که توسط x ′ 0 = و x ′ n +1 = x ′ n ∇ y ′ n که ثابت در نظر گرفته می‌شود. این کار را با فرض وجود بهترین انتزاع انجام می‌دهد که لزوماً نمی‌توان تضمین کرد که بهترینی وجود داشته باشد. مثلاً اگر مجموعه ای از زوج‌های (x , y) از اعداد حقیقی را با محصور کردن چند ضلعی محدب انتزاعی کنیم، هیچ انتزاع بهینه ای نسبت به نسبت به x 2 + y 2 =۱ موجد نیست. نمونه‌هایی از دامنه‌های انتزاعی به هر متغیر x موجود در یک برنامه، فاصله زمانی [L x ، H x] را اختصاص می‌دهیم. به همین ترتیب می‌توان روابط پیچیده تری را برای ضرب، تقسیم و غیره بدست آورد و به اصطلاح حسابی بازه ای انجام داد. با استفاده از اطلاعات هماهنگی ( = حتی، = عجیب و غریب)، یک تقسیم صفر می‌تواند حذف شود. هر یک از متغیرها ممکن است صفر باشد، اما هر سه به‌طور همزمان نمی‌توانند صفر باشند. اما اگر محاسبه ای را از در بازه [۰ ، ۱] شروع کنیم، یکی از ها در بازه [-۱ ، +۱] می‌شود. این مثال نشان می‌دهد با این که هر عملیات به صورت جداگانه انتزاعی بود، ترکیب آنها انتزاعی نیست. در اصل، این دامنه از فاصله‌ها رابطه بین متغیرها را در نظر نمی‌گیرد پس یک دامنه غیر رابطه ای می‌باشد. چند نمونه از دامنه‌های انتزاعی عددی رابطه ای عبارتند از: روابط کنگره ای در اعداد صحیح چند ضلعی محدب (عکس چپ) - با برخی هزینه‌های محاسباتی بالا ماتریس‌های با اختلاف جزئی «هشت ضلعی‌ها» برابری‌های خطی و ترکیبات آن (مانند محصول کاسته شده، به عنوان تصویر درست). وقتی شخصی دامنه انتزاعی را انتخاب می‌کند باید تعادل بین حفظ روابط مختلف و هزینه‌های بالای محاسباتی را برقرار کند. ابزارها ابزارهای صوتی ابزارهای صوتی تضمین می‌کنند که که آلارم آنها دقیق و درست است و هرگز اشتباهاً منفی ارایه نمی‌دهند اما با عدم اطمینان ممکن است آلارم‌های اشتباهاً مثبت تولید کنند که سیگنال خطای احتمالی را نمایش می دهدا (زیرا تجزیه و تحلیل ایستا به اندازه کافی دقیق نیست تا خطای احتمالی را از بین ببرد). | ## جمع‌بندی | این ابزارها می‌توانند آلارم اشتباهاً مثبت یا اشتباهاً منفی صادر کنند و خطایی را که برای یک اجرای برنامه رخ می‌دهد را ثبت نمی‌کند، زیرا تجزیه و تحلیل ایستایی که انجام می‌دهند نادرست است (یعنی در بررسی برخی از اجراهای احتمالی دچار اشتباه می‌شوند).