تفسیر انتزاعی

در علوم کامپیوتر تفسیر انتزاعی یک تیوری تقریب صدا از معنای بزنامه‌های کامپیوتر بر مبنای توابع یکنواخت بر روی مجموعه‌های مرتب به ویژه شبکه‌ها می‌باشد که می‌تواند به صورت یک بخش اجرایی از یک برنامه کامپیوتری که اطلاعات معنایی (مثل کنترل معلق یا داده معلق و ..)را بدون انجام همه محاسبات جمع‌آوری می‌کند باشد.

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

تفسیر انتزاعی توسط دو شریک علوم کامپیوتر فرانسوی، پاتریک کوسوت و رادیا کوسوت در اواخر دهه ۱۹۷۰ رسمیت یافت.

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

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

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

اگر ما فقط به برخی از اطلاعات خاص نیاز داشته باشیم، مثلاً در پرسش "آیا شخصی با سن n در اتاق وجود داشته‌است؟"، نگه داشتن لیستی از همه اسامی و تاریخ تولدها ضروری نیست. ما می‌توانیم بدون از دست دادن دقت، به نگه داشتن لیستی از سن شرکت کنندگان اکتفا کنیم. اگر این کار هم زیاد است، کافی است فقط سن جوانترین و پیرترین فرد را نگه داریم. اگر سؤال در مورد سنی است که به‌طور متوسط کمتر از m یا بالاتر از M است، بنابراین با اطمینان می‌توانیم پاسخ دهیم که هیچ شرکت کننده ای حضور نداشته‌است. در غیر این صورت، ما فقط می‌توانیم بگوییم که نمی‌دانیم.

در مورد محاسبات دقیق که در زمان و حافظه محدود قابل محاسبه نیست (به قضیه رایس و مشکل متوقف کردن مراجعه کنید) از انتزاع استفاده می‌شود تا پاسخ‌های تعمیم یافته مثل شاید را برای سوالاتی که جواب قطعی بله یا قطعاً خیر را نمی‌دانیم به عنوان "بله یا خیر "بسازیم. وقتی که الگوریتم تفسیر انتزاعی نمی‌تواند جواب دقیق را با قطعیت محاسبه کند این روش مشکلات را ساده‌تر می‌کند و برای آنها راه حل‌های خودکار می‌سازد. یک شرط اساسی برای ساختن جواب مبهم این است که بتواند مشکلات را کنترل کند و در عین حال دقت کافی را برای پاسخ به سؤالات مهم حفظ کند (مانند "ممکن است برنامه خراب باشد؟")

 تفسیر انتزاعی از برنامه‌های رایانه ای 
در یک زبان برنامه‌نویسی مشخص، تفسیر انتزاعی شامل ارائه چندین رابطه معناشناسی مرتبط با روابط انتزاعی می‌باشد. معناشناسی یک توصیف ریاضی از یک رفتار احتمالی برنامه است. دقیق‌ترین معناشناسی، که اجرای برنامه را بسیار دقیق توصیف می‌کند، معناشناسی دقیق نامیده می‌شود. مثلاً، معناشناسی دقیق یک زبان برنامه‌نویسی ضروری برای هر برنامه شامل خروجی‌هایی می‌شود که هر برنامه تولید می‌کند. خروجی‌ها معمولاً از اجرای متوالی برنامه در حالات محتلف بدست می‌آید. معمولاً از مقدار پیشخوان برنامه و مکان‌های حافظه (گلوبال‌ها، پشته‌ها و صف‌ها) تشکیل شده‌است. معانی انتزاعی بیشتر بدست می‌آید. مثلاً، ممکن است فقط یک دسته از حالت‌های قابل دستیابی در اجراهاها در نظر گرفته شود (که در نظر گرفتن آخرین حالت‌ها در آثار محدود) است.

هدف ما از تحلیل ایستا استخراح یک سری محاسبات معنایی در برخی نقاط می‌باشد. بمثلا، ممکن است برای تغییر متغیرهای عددی تنها با نگه داری علائم متغیرها (+، یا ۰) وضعیتشان را دستکاری کند. برای برخی از عملیات ابتدایی، مانند ضرب، چنین انتزاعی هیچ دقتی را از دست نمی‌دهد: برای به دست آوردن علامت یک محصول، شناختن علامت عملوندها کافی است. برای برخی از عملیات‌های دیگر ، انتزاع ممکن است دقت را از دست بدهد: برای مثال، نمی‌توان از علامت مبلغی که عملکرد آن‌ها به ترتیب مثبت و منفی باشند، ناممکن است.

در بعضی مواقع برای دست یابی به یک تفسیر معنایی تصمیم پذیر لازم است دقت را کاهش دهیم (نگاه کنید به قضیه رایس، مشکل متوقف کردن). به‌طور کلی، بین دقت آنالیز و تعیین پذیری آن (محاسبه) یا قابلیت تراکم پذیری (هزینه محاسباتی) باید سازش ایجاد شود.

در عمل انتزاعات باید متناسب با هر دو هدف یک برنامه کامپیوتری یعنی تحزیه و تحلیل و مجموعه ای هدفمند بون باشد. اولین تجزیه خودکار مقیاس بزرگ برنامه‌های  کامپیوتری به وسیله تفسیر انتزاعی را می‌توان یک اتفاق تصادفی دانست که منجر به تخریب اولین پرواز موشک Ariane 5 در سال ۱۹۹۶ شد.

 رسمیت 
بندانگشتی| مثال: انتزاع مجموعه‌های عدد صحیح (قرمز) برای امضای مجموعه‌ها (سبز)
L یک مجموعه مرتب است و، یک مجموعه دقیق نامیده شود همجنین L ′ یک مجموعه مرتب دیگر باشد، به نام یک مجموعه انتزاعی. این دو مجموعه L و L' با تعریف توابع کل که عناصر توابع را از یکی به دیگری ترسیم می‌کند، به یکدیگر مرتبط می‌شوند.

تابع α یک تابع انتزاع است اگر عنصر x را از مجموعهٔ دقیق L به عنصر (x)α را در مجموعه L ′ تصویر کند. عنصر α (x) در L ′ x در L است.

تابع γ d یک تابع دقیق گفته می‌شوداگر عنصر x ′ در مجموعه انتزاعی L ′ به یک عنصر γ (x ′) در مجموعه دقیق L ترسیم شود .. یعنی عنصر γ (x ′) L یک ترسیم دقیق x ′ در L ′ می‌باشد.

مجموعه‌های L 1، L 2، L ′ 1 و L ′ 2 را در نظر بگیرید. معناشناسی دقیق f یک تابع یکنواخت از L 1 تا L 2 است. تابع f ′ L ′ تا ′ 2 انتزاع معتبر از f نامیده می‌شود اگر برای هر x ′ L ′ (f ∘ γ)(x′) ≤ (γ ∘ f′)(x′)

معناشناسی برنامه را به‌طور کلی می‌توان به وسیله نقاط ثابت در حضور حلقه‌ها یا روش‌های بازگشتی توصیف کرد. فرض کنید که L یک شبکه کامل است و f یک تابع یکنواخت از L به L می‌باشد. پس هر x' بطوریکه f(x′) ≤ x′ باشد یک انتزاع از نقطه ثابت از f،است، قضیه Knaster-تارسکی.

اکنون می‌خواهیم 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 که ثابت در نظر گرفته می‌شود. سپس می‌توانیم y′) را برابر f′(x′n) در نظر بگیریم.

در برخی موارد، می‌توان انتزاعات را با استفاده از اتصالات Galois (α، γ) تعریف کرد که α در آن از L به L ′ و γ از L ′ به L است. این کار را با فرض وجود بهترین انتزاع انجام می‌دهد که لزوماً نمی‌توان تضمین کرد که بهترینی وجود داشته باشد. مثلاً اگر مجموعه ای از زوج‌های (x , y) از اعداد حقیقی را با محصور کردن چند ضلعی محدب انتزاعی کنیم، هیچ انتزاع بهینه ای نسبت به نسبت به x 2 + y 2 =۱ موجد نیست.

 نمونه‌هایی از دامنه‌های انتزاعی 
به هر متغیر x موجود در یک برنامه، فاصله زمانی [L x ، H x] را اختصاص می‌دهیم. فرض کنیمبرای هر ٓ در برنامه v(x) را به x برای این فواصل  [L x ، H x] اختصاص داشته باشیم، از فواصل [L x ، H x] و [L y ، H y] برای متغیرهای x و y، می‌توان به راحتی فواصل x+y ([Lx+Ly, Hx+Hy] و برای x−y ([Lx−Hy, Hx−Ly]) را اختصاص می‌دهیم. این‌ها انتزاعات دقیق هستند چون مجموعه نتایج احتمالی مثلاً x + y دقیقاً بازه ([L x + L y ، H x + H y]) است. به همین ترتیب می‌توان روابط پیچیده تری را برای ضرب، تقسیم و غیره بدست آورد و به اصطلاح حسابی بازه ای انجام داد.

 اکنون اجازه دهید برنامه بسیار ساده زیر را در نظر بگیریم: y = x;
z = x - y;
بندانگشتی| ترکیبی از حسابی فاصله () و تعدیل تعدیل ۲ در اعداد صحیح () به عنوان دامنه انتزاعی برای تجزیه و تحلیل یک قطعه ساده از کد C (: مجموعه‌های بتونی از مقادیر ممکن در زمان اجرا). با استفاده از اطلاعات هماهنگی ( = حتی،  = عجیب و غریب)، یک تقسیم صفر می‌تواند حذف شود. (از آنجا که فقط یک متغیر درگیر است، مسئله رابطه در مقابل دامنه‌های غیر مرتبط در اینجا مسئله ای نیست)
بندانگشتی| یک چند ضلعی به عنوان مثال محدب ۳ بعدی که مقادیر احتمالی ۳ متغیر را در برخی از برنامه‌ها توصیف می‌کند. هر یک از متغیرها ممکن است صفر باشد، اما هر سه به‌طور همزمان نمی‌توانند صفر باشند. ویژگی دوم را نمی‌توان در حوزه حسابی با فاصله توصیف کرد.
با انواع حسابی معقول، نتیجهٔ  باید صفر باشد. اما اگر محاسبه ای را از  در بازه [۰ ، ۱] شروع کنیم، یکی از ها در بازه [-۱ ، +۱] می‌شود. این مثال نشان می‌دهد با این که هر عملیات به صورت جداگانه  انتزاعی بود، ترکیب آنها انتزاعی نیست.

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

چند نمونه از دامنه‌های  انتزاعی عددی رابطه ای عبارتند از:
 روابط کنگره ای در اعداد صحیح
 چند ضلعی محدب (عکس چپ) - با برخی هزینه‌های محاسباتی بالا
 ماتریس‌های با اختلاف جزئی
 «هشت ضلعی‌ها»
 برابری‌های خطی

و ترکیبات آن (مانند محصول کاسته شده، به عنوان تصویر درست).

وقتی شخصی دامنه انتزاعی را انتخاب می‌کند باید تعادل بین حفظ روابط مختلف و هزینه‌های بالای محاسباتی را برقرار کند.

 ابزارها 
 ابزارهای صوتی 
ابزارهای صوتی تضمین می‌کنند که که آلارم آنها دقیق و درست است و هرگز اشتباهاً منفی ارایه نمی‌دهند اما با عدم اطمینان ممکن است آلارم‌های اشتباهاً مثبت تولید کنند که سیگنال خطای احتمالی را نمایش می دهدا (زیرا تجزیه و تحلیل ایستا به اندازه کافی دقیق نیست تا خطای احتمالی را از بین ببرد).
 آنالایزر پیشرفته مطلقAbsInt Advanced Analyzer
 آستر
 CodeContracts چک کننده استاتیکCodeContracts static checker (cccheck)
 CodePeer
 CPAchecker
 فرار
 نوسان
 تجزیه و تحلیل ارزش Frama-C
 IKOSIKOS
 آنالایزر جولیا استاتیک برای کدهای جاوا، اندروید و جاوا
 پنجیلی
 Polyspace
 درندهpredator
 وراسکوVerasco

 ابزارهای غیر صوتی 
ابزارهای غیر صوتی تضمین نمی‌کنند که آلارم آنها دقیق و درست باشد. این ابزارها می‌توانند آلارم اشتباهاً مثبت یا اشتباهاً منفی صادر کنند و خطایی را که برای یک اجرای برنامه رخ می‌دهد را ثبت نمی‌کند، زیرا تجزیه و تحلیل ایستایی که انجام می‌دهند نادرست است (یعنی در بررسی برخی از اجراهای احتمالی دچار اشتباه می‌شوند). در نتیجه می‌توانند اشتباهاً ادعا کنند که یک برنامه ناامن کاملاً بی خطر است.
 کدونار
 از پوشش جلوگیری می‌کند
 بینش Klocwork 
 تست C / C ++ Parasoft 
 پاراتفت جتست 
 مارمولک قرمز Goanna 

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

 منابع 

 پیوند به بیرون 
 یک صفحه وب در مورد تفسیر چکیده توسط پاتریک کاسوت
 مقاله روبرتو بانگارا که نشان می‌دهد چگونه می‌توان آنالیزور استاتیک مبتنی بر تفسیر انتزاعی را برای یک زبان برنامه‌نویسی C مانند
 Symposia Analysis Static , دادرسی که در سریال Springer LNCS ظاهر می‌شود
 کنفرانس تأیید، بررسی مدل و تفسیر چکیده (VMCAI)، وابسته در کنفرانس POPL , رویه‌هایی که در مجموعه Springer LNCS ظاهر می‌شوند

 یادداشت‌های سخنرانی
 تفسیر چکیده پاتریک کاسوت. MIT
 یادداشتهای سخنرانی دیوید اشمیت در مورد تفسیر انتزاعی 
 یادداشت‌های سخنرانی مولر و شوارتزاک در مورد تحلیل برنامه استاتیک
 یادداشت‌های سخنرانی آگوستینو کورتسی در مورد تجزیه و تحلیل برنامه و تأیید صحت
 اسلایدها توسط Grégoire Sutre در هر مرحله از تفسیر انتزاعی با مثالهای بسیاری - همچنین معرفی اتصالات Galois
رده:تفسیر انتزاعی
رده:تحلیل برنامه