مشاهده مشخصات مقاله
ترکيب روش SL با ترتيب KBO براي اثبات خودکار پايان‌پذيري سيستم بازنويسي ترم
|
نویسنده (ها) |
|
|
مربوط به کنفرانس |
هفدهمین کنفرانس ملی سالانه انجمن کامپیوتر ایران |
|
چکیده |
سيستم¬ بازنويسي ترم (TRS) مدلي انتزاعي از زبان¬هاي تابعي ارائه مي¬دهد.اثبات پايان¬پذيرييکTRSبراي تاييد درستي عملکرد زبانهاي تابعيضروري است.روش برچسب¬گذاري معنايي(SL) روشي کامل براي اثبات پايان¬پذيري به شمار مي¬رود. بخش معنايياين روش توسط يک شبه-مدلاز تفسير تابع¬نشانه¬ها ايجاد مي¬شود. بيشتر توان روش SLبه استفاده از مدل¬هاي نامتناهي مربوط مي¬شود کهارائه آنها در ابزارهاي آزمون خودکار پايان¬پذيري دشوار است. در اين مقاله روش SL با دامنه تفسيراعداد طبيعي به شکلي با ترتيب کُنت-بنديکس (KBO) ترکيب شده تا بتوان اثبات پايان¬پذيري با مدل¬هاي نامتناهي را به طور خودکار انجام داد. ابتدا تعميمي از KBO به نام ترتيب کُنت-بنديکس برچسب¬گذاري(ℓKBO) ارائه، سپس توانايي آن را در اثبات پايان-پذيري TRS نشان داده¬ايم. الگوريتم جستجوي خودکار يک ℓKBO براي يک TRSمعرفيشده و عملکرد آن روي کتابخانه TPDB 3.1 با موفقيت مورد آزمون قرار گرفته است. |
|
قیمت |
-
برای اعضای سایت : ۱٠٠,٠٠٠ ریال
-
برای دانشجویان عضو انجمن : ۲٠,٠٠٠ ریال
-
برای اعضای عادی انجمن : ۴٠,٠٠٠ ریال
|
خرید مقاله
|
|
.gif){kind=icon}