آنالیز تخصیص قطعی
آنالیز

موارد زیر بر اساس رسمی‌سازی Fruja در تجزیه و تحلیل تخصیص قطعی درون رویه‌ای (تک روشی) سی شارپ است، که مسئول اطمینان از تخصیص همه متغیرهای محلی قبل از استفاده از آن‌ها است. آن را به طور همزمان تجزیه و تحلیل تخصیص مشخص و انتشار ثابت مقادیر بولین انجام می‌دهد. ما پنج تابع استاتیک را تعریف می کنیم:
| نام | دامنه | توضیح |
| --- | --- | --- |
| قبل | تمام عبارات | متغیرهایی که قبل از ارزیابی عبارت، اختصاص داده شده‌اند. |
| بعد | تمام عبارات | متغیرهایی که قطعاً پس از ارزیابی عبارت، با فرض اینکه به طور معمول کامل شود، اختصاص داده می شوند. |
| vars | تمام عبارات | همه متغیرهای موجود در محدوده‌ی عبارت داده شده. |
| درست | تمام عبارات بولین | متغیرهایی که پس از ارزیابی عبارت داده شده، با فرض درست بودن عبارت، قطعاً اختصاص داده می‌شوند. |
| نادرست | تمام عبارات بولین | متغيرهایی که قطعاً پس از ارزيابي عبارت، با فرض نادرست بودن عبارت، تخصيص داده مي شوند. |
ما معادلات جریان داده را ارائه می کنیم که مقادیر این توابع را در عبارات مختلف بر حسب مقادیر توابع در زیرعبارات نحوی آن‌ها تعریف می‌کند. فرض کنید که هیچ دستوری برای رسیدگی به دستورات goto، break، continue، return یا کنترل استثنا وجود ندارد. چند نمونه از این معادلات به صورت زیر است:
هر عبارت e که بر مجموعه متغیرهایی که به طور قطعی اختصاص داده شده‌اند، تأثیر نمی‌گذارد: after(e) = before(e)
فرض کنید e عبارت تخصیص loc = v باشد. آنگاه before(v) = before(e) و after(e) = after(v) U {loc}.
فرض کنید e عبارت «درست» باشد. آنگاه true(e) = before(e) و false(e) = vars(e). به عبارت دیگر، اگر e مقدار «نادرست» را بگیرد، همه‌ی متغیرها (به صورت خالی) به طور قطعی اختصاص داده می شوند، زیرا e مقدار «نادرست» را نگرفته است.
از آنجایی که آرگومان‌های متد از چپ به راست ارزیابی می شوند، before(argi + 1) = after(argi). پس از تکمیل یک متد، پارامترهای خروجی قطعاً اختصاص داده شده‌اند.
فرض کنید s عبارت شرطی if (e) s1 else s2 باشد. آنگاه before(e) = before(s), before(s1) = true(e), before(s2) = false(e), و after(s) = after(s1) intersect after(s2).
فرض کنید s عبارت حلقه‌ی while (e) s1 باشد. آنگاه before(e) = before(s), before(s1) = true(e), and after(s) = false(e).
و غیره ...
در ابتدای روش، هیچ متغیر محلی به طور قطعی تخصیص داده نمی‌شود. تأیید کننده به طور مکرر روی درخت نحو انتزاعی مرور می‌کند و از معادلات جریان داده برای انتقال اطلاعات بین مجموعه‌ها استفاده می‌کند تا به یک نقطه ثابت برسد. سپس، تأییدکننده مجموعه‌ی «قبل»، از هر عبارتی که از متغیر محلی استفاده می‌کند، بررسی می‌کند تا مطمئن شود که حاوی آن متغیر است.
این الگوریتم با معرفی پرش‌های کنترل جریان مانند goto، break، continue، return و کنترل خطا، پیچیده می شود. هر عبارتی که می‌تواند هدف یکی از این پرش‌ها باشد، باید مجموعه‌ی «قبل» خود را با مجموعه متغیرهای قطعی اختصاص داده شده در منبع پرش، تقاطع بدهد. هنگامی که این‌ها معرفی می شوند، جریان داده‌ی حاصل ممکن است چندین نقطه ثابت داشته باشد، مانند این مثال:
int i = 1;
 L:
 goto L;
از آنجایی که می‌توان به برچسب L دو مکان دسترسی یافت، معادله کنترل جریان برای goto حکم می کند که before(2) = after(1) با before(3) تقاطع دارد. اما before(3) = before(2)، پس before(2) = after(1) با before(2) تقاطع دارد. این دارای دو نقطه ثابت برای before(2), {i} و مجموعه‌ی تهی است. با این حال، می‌توان نشان داد که به دلیل شکل یکنواخت معادلات جریان داده، یک نقطه ثابت ماکسیمال منحصر به فرد (نقطه ثابت با بزرگترین اندازه) وجود دارد که بیشترین اطلاعات ممکن را در مورد متغیرهای قطعی اختصاص داده شده ارائه می‌دهد. چنین ماکسیمال (یا ماکسیمم) نقطه ثابت ممکن است با تکنیک‌های استاندارد محاسبه شود. به تحلیل جریان داده رجوع کنید.

یک مسئله دیگر این است که یک پرش جریان کنترلی ممکن است برخی جریان‌های کنترلی را غیرممکن کند. به عنوان مثال، در این قطعه کد، متغیر i قطعا قبل از استفاده، اختصاص داده شده است:
int i;
 if (j < 0) return; else i = j;
 print(i);
معادله جریان داده برای if می گوید که after(2) = after(return) پس از (i = j) متقاطع می‌شوند. برای اینکه این کار به درستی انجام شود، تعریف می‌کنیم after(e) = vars(e) برای همه‌ی پرش‌های کنترل جریان. این به همان دلیل تایید شده است که معادله false(true) = vars(e) است؛ زیرا امکان ندارد کنترل بلافاصله پس از پرش جریان کنترل، به نقطه‌ای برسد.