استقراء نوع داده را به صورت زیر تعریف می کنیم

Report
1
‫ادامه فصل چهارم ‪:‬‬
‫معنای نشانه گذاریها‬
‫معنای نشانه گذاری‪،‬یک مدل تابعی برای توصیف معنای زبان برنامه سازی است‪.‬قبل از بحث‬
‫مختصر راجع به معنای نشانه گذاری‪ ،‬ابتدا حساب المبدا را به عنوان یک مدل تابعی ساده تر‬
‫معرفی میکنیم که در دهه ‪ 1930‬مطرح شد تا محاسبات ریاضی را تشریح نماید‪ .‬با استفاده از‬
‫حساب الندا ساختارهای پیچیده تری را می توان ایجاد کرد‪،‬از جمله مفاهیم انواع داده و معنای‬
‫زبان برنامه سازی‪.‬‬
‫‪2‬‬
‫حساب الندا‬
‫احتماال اولین مدل معنای زبان برنامه سازی‪ ،‬حساب الندا (حساب ‪ )λ‬بوده است که در دهه ‪ 1930‬توسط ا‪.‬کورچ‬
‫به عنوان مدل تئوری محاسبات در مقایسه با ماشین تورینگ مطرح شد‪.‬حساب الندا ‪،‬مدل خوبی را برای‬
‫فراخوانی تابع زبان برنامه سازی ارائه کرد‪.‬در واقع‪ ،‬الگول و لیسپ می توانند معنای فراخوانی تابع را با مدل‬
‫حساب ‪λ‬ردیابی کنند‪ .‬جانشینی حساب ‪،λ‬نگاشت مستقیم مکانیزم ارسال پارامتر از طریق نام درالگول‬
‫است‪.‬حساب ‪λ‬توسط اسکات به صورت یک تئوری انواع داده بسط داده شد که امروزه معنای نشانه گذاری نامیده‬
‫می شود‪.‬این نشانه گذاری بر روی طراحی تئوری انواع در ام ال تأثیر داشته است‪.‬عبارات ‪λ‬به طور بازگشتی و‬
‫به صورت زیر تعریف می شوند‪.‬‬
‫‪ .1‬اگر ‪х‬نام متغیر باشد ‪х،‬یک عبارت ‪λ‬است‪.‬‬
‫‪ .2‬اگر ‪М‬یک عبارت ‪λ‬باشد ‪λх.м ،‬یک عبارت ‪λ‬است‪.‬‬
‫‪ .3‬اگر‪F‬و ‪A‬عبارات ‪λ‬باشند ‪ )FA(،‬عبارت ‪λ‬است‪F.‬یک عملگرد و ‪A‬یک عملوند است‪.‬‬
‫عبارت ‪λ‬می توانیم با گرامر مستقل از متن تعریف کنیم‪:‬‬
‫)‪λ-expr indentifier | λidentifier .λ-expr |(λ-expr λ_expr‬‬
‫عبارات زیر با گرامر فوق تولید می شوند‪:‬‬
‫‪X‬‬
‫‪λx.x‬‬
‫‪λx.y‬‬
‫)‪λx.(xy‬‬
‫))‪(λx.(xx)λx.(xx‬‬
‫‪λx.λy.x‬‬
‫‪3‬‬
‫متغیرها ممکن است مقید یا آزاد باشند‪.‬ازنظر شهودی ‪،‬متغیر مقید به طور محلی اعالن‬
‫می شود‪،‬در حالی که متغیر آزاد اعالن نمی شود‪.‬در عبارت الندا ‪ х،х‬آزاد است‪.‬اگر ‪х‬‬
‫در ‪ м‬آزاد باشد‪،‬در‪ λх.м‬مقید است‪ х.‬وقتی در(‪)FA‬آزاد است که در ‪ F‬یا در ‪ A‬آزاد‬
‫باشد‪.‬متغیرهای مقید به عنوان ”پارامترهای ”تابعی است که توسط عبارت ‪ λ‬توصیف‬
‫شده است‪.‬متغیرهای آزاد‪،‬عمومی اند‪.‬این مقایسه نشان می دهد که عبارت ‪ λ‬تقریبی از‬
‫مفهوم زیر برنامه در زبانهای برنامه سازی الگوریتمیک مثل پاسکال‪،C،‬ادا و فرترن‬
‫است‪.‬‬
‫‪4‬‬
‫عملیات در حساب الندا‬
‫عبارات ‪ λ‬فقط یک عملیات کاهش دارد‪.‬اگر (‪ )FA‬یک عبارت ‪ λ‬باشد و ‪F=λх.М‬آنگاه ‪ A‬می‬
‫تواند به جای هر ‪ х‬آزاد در ‪ М‬قرار گیرد‪.‬این موضوع به صورت‪ )λх.М A(  M‬نوشته می‬
‫شود‪.‬این عملیات مثل جانشینی پارامترهای مجازی در فراخوانی تابع است‪.‬مثالهایی از عملیات کاهش‬
‫عبارت ‪ λ‬عبارتند از‪:‬‬
‫)‪(λx.x y‬‬
‫‪y‬‬
‫)‪(λx.(xy) y‬‬
‫)‪(yy‬‬
‫)‪(λx.(xy) λx.x‬‬
‫)‪(λx.x y‬‬
‫‪ y‬‬
‫))‪(λx.(xx) λx.(xx‬‬
‫… ‪(λx.(xx) λ.x(xx) ‬‬
‫عملیات کاهش همیشه منجر به عبارت ‪ λ‬نمی شود که ساده تر از عبارت اصلی باشد‪.‬مثال چهارم که‬
‫در باال آمده است خاتمه نمی یابد‪.‬این خاصیت را خاصیت چورچ‪-‬رویسر گویند‪:‬اگر دو کاهش از‬
‫عبارت ‪λ‬خاتمه یابند‪،‬عضوی از یک دسته از مقادیرند‪.‬به عبارت دیگر‪،‬اگر عبارت الندا ‪М‬دارای‬
‫کاهشهای ‪M→p‬و ‪ MQ‬باشد‪،‬آنگاه یک عبارت الندا ‪ R‬وجود دارد که‪ P→R‬و‪ R.Q→R‬را‬
‫شکل نرمال دسته ای از مقادیر می نامند که با ‪ M‬نمایش داده می شود‪.‬‬
‫‪5‬‬
‫انتقال پارامترها با عبارات ‪ .λ‬در عبارت ‪ λ‬دو روش استاندارد را برای کاهش در نظر بگیرید‪.1:‬اول داخلی‬
‫ترین جمله را کاهش دهید و ‪ .2‬اول خارجی ترین جمله را کاهش دهید‪.‬به عنوان مثال‪،‬در این عبارت الندا‪:‬‬
‫))‪(λy.(yy)(λx.(xx)a‬خارجی ترین جمله‪،‬کل عبارت است‪،‬درحالی که داخلی ترین جمله )‪(λx.(xx)a‬‬
‫است‪.‬دو دنباله از کاهش امکان پذیر است‪:‬‬
‫کاهش خارجی ترین جمله‬
‫کاهش داخلی ترین جمله‬
‫))‪(λy.(yy) (λx.(xx0 a‬‬
‫))‪(λy.(yy) (λx.(xx) a‬‬
‫))‪((λx.(xx) a) (λx.(xx) a‬‬
‫))‪(λy.(yy) (aa‬‬
‫))‪((aa) (aa‬‬
‫))‪ ((aa) (aa‬‬
‫هردو کاهش‪،‬پاسخ یکسانی دارند‪ .‬کاهش خارجی ترین جمله‪،‬تابع )‪(λx.(xx) a‬را به جای ‪y‬قرار داد و این‬
‫تابع را برای هر ‪y‬ارزیابی کرد‪.‬این روش همانند فراخوانی با نام است‪.‬فراخوانی با نام‪،‬نمونه ای از ارزیابی‬
‫تنبل است لذا فقط عباراتی که در راه حل آخر ظاهر می شوند باید ارزیابی شوند‪.‬کاهش داخلی ترین‬
‫جمله‪،‬ثابت )‪(aa‬را قبل از جانشینی برای ‪،y‬ارزیابی می کند‪.‬این روش مانند فراخوانی با مقدار است‪.‬فراخوانی با‬
‫مقدار همیشه آرگومانها را ارزیابی می کند‪،‬لذا آرگومانهای خاتمه پذیر نیز حتی در صورت عدم نیاز‪،‬ارزیابی‬
‫می شوند‪.‬‬
‫‪6‬‬
‫با استفاده از این وضعیت می توانیم مثالهایی از جمالت را ارائه کنیم که از طریق فراخوانی با نام خاتمه‬
‫می یابند ولی از طریق فراخوانی با مقدار خاتمه نمی یابند‪.‬برای این منظور الزم است عبارت ‪λ‬پایان نا‬
‫پذیر را به عنوان آرگومان در نظر بگیریم که اصال به آن مراجعه نمی شود‪.‬می دانیم که )‪(λx.(xx‬‬
‫))‪λx.(xx‬خاتمه نمی یابد و در عبارت ‪،λy.z‬به پارامتر ‪y‬مراجعه نمی شود‪،‬لذا عبارت زیر دارای‬
‫شکل نرمال ‪z‬است که اگر از فراخوانی با نام استفاده شود خاتمه می یابد‪،‬اما اگر فراخوانی با‬
‫مقداراِعمال شود‪،‬یک عبارت ‪ λ‬پایان ناپذیر است‪:‬‬
‫)))‪(λy.z (λx.(xx) λx.(xx‬‬
‫‪7‬‬
‫مدلسازی ریاضی با عبارات الندا‬
‫حساب الندا به عنوان مدل منطقی محاسبات ایجاد شد‪.‬با استفاده ازاین عبارات می توانیم درک خود را از محاسبات‬
‫مدلسازی کنیم‪.‬ابتدا عبارت ‪ λ‬برای مدلسازی حساب محموالت)‪ (predicate calculus‬به کار می روند و سپس با‬
‫استفاده از حساب محموالت می توانیم مقادیر صحیح را مدلسازی کنیم‪.‬‬
‫مقادیر بولین‪ .‬مقادیر بولین را به صورت عبارات ‪ λ‬مدلسازی می کنیم‪true(t) :‬به صورت‪λx. λ y.x‬تعریف‬
‫مشود‪(.‬باتوجه به معنای درستی‪،‬تفسیر این عبارت ساده است‪:‬از جفتی از مقادیر‪،‬اولی را انتخاب کن)‬
‫)‪ false(f‬به صورت ‪λx.λy.y‬تعریف می شود(از جفتی از مقادیر‪،‬دومی را انتخاب کن)باتوجه به تعریف این‬
‫اشیاء‪،‬خواص زیر درست اند‪.‬‬
‫‪((T p) Q) p i.e., ((T p) Q) ))λx.λy.x p) Q) (λy.p Q)  p‬‬
‫‪((F p)Q )Q i.e., ((F p) Q) ((λx.λy.y p) Q)(λy.y Q)Q‬‬
‫باتوجه به تعریف ثوابت ‪T‬و‪،F‬توابع بولین را می توانیم به صورت زیر تعریف کنیم‪:‬‬
‫‪not= λx.((xF)T‬‬
‫)‪And= λx.λy.((xy)F‬‬
‫)‪Or= λx.λy.((xT) y‬‬
‫با این تعاریف‪،‬الزم است نشان دهیم که تفسیر ما از آنها با قواعد منطق محموالت سازگاری دارد‪.‬به عنوان‬
‫مثال‪،‬وقتی ‪ not‬بر روی ‪T‬عمل می کند‪F ،‬حاصل می شود و اگر ‪not‬بر روی ‪F‬عمل کند ‪T ،‬حاصل می شود‪:‬‬
‫‪(not T)=(λx.((x F)T)T)  ((T F)T)F‬‬
‫‪(not F)=(λx.((x F)T)F) ((F F)T) T‬‬
‫‪8‬‬
‫مقادیر صحیح‪ .‬باتوجه به توابع بولین‪،‬می توانیم مقادیر صحیح را تولید کنیم‪:‬‬
‫‪0= λf.λc.c‬‬
‫)‪1=λf.λc.(fc‬‬
‫))‪2=λf.λc.(f(fc‬‬
‫)))‪3=λf.λc.(f(f(fc‬‬
‫‪… ….‬‬
‫‪C‬عنصر“صفر“است و ‪f‬تابع ”بعدی (‪“)successor‬است که به عنصر ‪c‬اعمال می شود(یک واحد اضافه می کند)‪.‬‬
‫))‪(M+N)= λa.λb.(M a) ((N a)b‬‬
‫))‪+ =λM.λN.λa.λb.((M a) ((N a)b‬‬
‫))‪:) M *N)= λa.(M(N a‬ضرب‬
‫)‪:)M^N) =(NM‬توان‬
‫‪9‬‬
‫مدلسازی زبانهای برنامه سازی‬
‫باتوجه به بحثی که در مورد عبارات الندا شد‪،‬می توانیم با بسط عبارات الندا‪،‬انواع داده ها را مدلسازی کنیم و سپس‬
‫آن مدل را بسط دهیم تا معنای زبان برنامه سازی را نیز دربر گیرد‪.‬‬
‫وقتی عملیات کاهش بر روی عباراتی اعمال شود‪،‬عبارت ‪ λ‬به یک مقدار ثابت یا عبارت ‪ λ‬دیگر کاهش می یابد‪،‬لذا‬
‫تمام عبارات ‪ λ‬راه حلهایی برای معادله تابعی زیر هستند‪:‬‬
‫)‪λexpression=constant + (λexpression  λ expression‬‬
‫بدون اینکه به جزئیات معنای نشانه گذاری بپردازیم‪،‬می توان گفت که نوع داده‪،‬راه حلی برای این معادله‬
‫است‪.‬شباهتی بین این مدل از نوع داده و تعریف نوع در اِم اِل وجود دارد‪:‬‬
‫| ‪Datatype Mylist =var of int‬‬
‫;‪Listitem of int * Mylist‬‬
‫این دستور‪،‬لیستی از مقادیر صحیح(سازنده ‪ )Mylist‬را با استفاده از سازنده های ‪var‬و ‪(listitem‬مانند عبارات‬
‫‪ )λ‬تعریف می کند‪.‬‬
‫با استفاده از این مفهوم می توانیم مدل معنایی نشانه گذاری را برای یک زبان برنامه سازی ساده مدلسازی کنیم‪.‬این‬
‫مدل به شکل معنای عملیاتی است‪،‬زیرا اجرای هر نوع دستور را ردیابی می کنیم تا اثر آن را بر مفسر سطح باالتر‬
‫تعیین کنیم‪.‬‬
‫‪10‬‬
‫برنامه را مانند حساب ‪ λ‬به صورت یک تابع در نظر می گیریم‪،‬هر دستور برنامه‪،‬یک تابع خواهد بود و اجرای‬
‫دستورات متوالی را مدل می کنیم‪.‬‬
‫برای هر نوع دستور می توانیم یک معادله ”نوع داده ” بنویسیم‪:‬‬
‫)‪Stmt = (ld *Exp‬‬
‫‪Domain of assignments‬‬
‫) ‪+(Stmt * Stmt‬‬
‫‪Domain of sequences‬‬
‫‪+(Exp * Stmt * Stmt ) Domain of conditionals‬‬
‫) ‪+(Exp * Stmt‬‬
‫‪Domain of iterations‬‬
‫همانند هر مفسر دیگر‪،‬نیازمند درک کامپیوتر مجازی مربوط هستیم‪.‬فرض می کنیم هرشناسه به محل خاصی از حافظه‬
‫اشاره می کند‪.‬نام مستعار‪،‬انتقال پارامتر و اشاره گرها در این مثال قابل استفاده نیستند‪.‬لذا‪،‬برای هر شناسه یک محل‬
‫منحصر بفرد در حافظه وجود دارد که شامل مقدارش است‪.‬‬
‫مفهوم حافظه را می توانیم به صورت تابعی مدلسازی کنیم که برای هر شناسه‪،‬مقدارش را برمی گرداند‪.‬این تابع را‬
‫‪stor‬می نامیم‪.‬‬
‫‪ Store‬شناسه ها را به مقادیر ذخیره شده نقش می کند که امضای آن به صورت ‪ idvalue‬است‪ id.‬مجموعه ای‬
‫از شناسه ها در زبان است‪.‬این امضا را حالت برنامه می گوییم‪.‬‬
‫درتعریف معنای زبان برنامه سازی‪،‬چند تابع را باید مشخص کنیم‪:‬‬
‫‪.1‬نیاز به توصیف برنامه است‪.‬‬
‫‪.2‬نیاز به توصیف دستور در زبا ن است‪.‬‬
‫‪.3‬تابع دستور ‪C‬به مقدار عبارات مختلف بستگی دارد‪،‬لذا باید اثر ارزیابی عبارت در زبان را درک کنیم‪.‬‬
‫امضاهای ارزیابی عبارت به صورت زیر است‪:‬‬
‫] ‪∑ : exp  [state  eval‬‬
‫‪11‬‬
‫مثال‪:‬اگر ‪exp‬عبارت ‪ a+b‬باشد‪،‬تابع ارزیابی عبارت است از‪ξ(a+b):state  eval :‬و اعمال این تابع به حالت ‪s‬‬
‫‪،‬تابع زیر را تولید می کند‪:‬‬
‫)‪ξ (a+b()s) =a(s) + b(s‬‬
‫در تعریف زبان‪،‬برای هرنوع دستور نحوی‪،‬نیاز به تعریف تابعی از نوع ‪state state‬داریم‪.‬برای سهولت از‬
‫ساختار ‪let‬در حساب ‪ λ‬استفاده می کنیم‪.‬جمله زیر را در نظر بگیرید‪:‬‬
‫‪Let x ← a in body‬‬
‫این جمله به معنای )‪((x) : body) (a‬است و همانند عبارت ‪ λ‬زیر است‪:‬‬
‫) ‪(λx. Body a‬‬
‫اگر ‪x‬دامنه نوع ‘‪ DD‬باشد‪،‬عبارت ]‪ x[v\e‬به صورت زیر تعریف می شود‪:‬‬
‫(‪X[v\e] =(D d ) D’: if d =v then e else x)d‬‬
‫معنایش تغییر عنصر ‪v‬از ‪x‬به ‪ e‬است و مدل اصلی ”انتساب“ را نشان می دهد‪.‬‬
‫‪12‬‬
‫معنای دستور‬
‫اکنون تعریف معنای هر دستور از زبان را‪،‬برحسب تبدیالت حالت محاسبه مشخص می کنیم‪begin … end.‬‬
‫دنباله ‪begin … end‬بر حالت داخلی محاسبات اثر ندارد‪،‬لذا یک تابع همانی در فضای حالت است‪:‬‬
‫}}‪C{{begin stmt end }} = c {{stmt‬‬
‫ترکیب‪:‬در این حالت‪،‬می خواهیم حالت نتیجه را پس از اجرای ‪ stmt1‬بر روی ‪stmt2‬اعمال کنیم‪.‬این حالت را به‬
‫صورت ترکیب تابع نمایش می دهیم‪:‬‬
‫))‪C{{stmt1; stmt2}} =(state s)state : c{{stmt2}} (c{{stmt1}} (s‬‬
‫آرگومان }}‪c{{stmt2‬همان حالت نتیجه پس از ارزیابی ‪stmt1‬است‪.‬‬
‫انتساب‪:‬حافظه جدیدی ایجاد می کند که نتیجه ارزیابی ‪ exp‬را در حالت فعلی مشخص می کند‪:‬‬
‫))‪C{{id←exp}} =(state s) state((value v)state : s[id\v] (ξ {{exp}} (s‬‬
‫‪ :if‬تعیین می کند کدامیک از دو تابع باید ارزیابی شوند‪.‬این کار‪ ξ،‬را ارزیابی می کند‪،‬آن را به تابع بولین اعمال می کند‬
‫که ‪stmt1‬یا ‪stmt2‬را ارزیابی می کند‪:‬‬
‫=}}‪C{{if exp then stmt1 else stmt2‬‬
‫‪(state s) state ((bool b) state  state :‬‬
‫)‪(if b then c {{stmt1 }} else c{{stmt2}} (ξ{{exp}} (s)) (s‬‬
‫‪13‬‬
‫‪ While.‬نیاز به تعریف بازگشتی دارد‪،‬زیرا تابع ‪ while‬بخشی از تعریف زیر است‪:‬‬
‫=}} ‪C{{while exp do stmt‬‬
‫‪rec(state s)state : ((bool b) state  state:‬‬
‫)}}‪(if b then c{{stmt}} o c{{while exp do stmt‬‬
‫))’‪else ((state s’)state:s‬‬
‫)‪(ξ{{exp}} (s)) (s‬‬
‫توجه کنید که در تعریف}}‪،c{{while‬از }}‪c{{while‬در تعریفش استفاده کردیم(به عنوان بخشی از دستور ‪.)then‬‬
‫لذا ‪ while‬به صورت زیر است‪:‬‬
‫)}}‪C{{while}}= f(c{{while‬‬
‫‪While‬راه حلی برای معادله ای به شکل زیر است‪:‬‬
‫)‪X= f(x‬‬
‫این راه حل‪،‬نقاط ثابت(‪ )fixed points‬نام دارند و کمترین نقطه ثابت را می خواهیم که این معادله را حل کند‪.‬‬
‫‪14‬‬
‫وارسی برنامه‬
‫در نوشتن برنامه ها‪،‬به صحت و قابلیت اعتماد آنها توجه داریم‪.‬زبانها طوری طراحی می شوند که این ویژگیها را‬
‫اعمال می کنند‪.‬‬
‫صحت برنامه از سه جهت بررسی می شود‪:‬‬
‫‪.1‬معنای صحت برنامه مثل ‪p‬چیست؟یعنی مشخصات آن‪S ،‬چیست؟‬
‫‪.2‬باتوجه به مشخصات ‪،S‬برنامه ‪P‬را طوری بنویسید که آن مشخصات را پیاده سازی کند‪.‬‬
‫‪.3‬مشخصات ‪ S‬و برنامه ‪ P‬باید یک عمل را انجام دهند‪.‬‬
‫مورد اول‪،‬موضوع مدلسازی معنای زبان است‪ .‬مورد دوم یعنی چگونه می توان با استفاده از مشخصات‪،‬برنامه خوبی‬
‫نوشت و مورد سوم به وارسی برنامه مربوط می شود‪.‬درواقع این سه مورد به هم شبیه اند‪.‬‬
‫هر برنامه‪،‬تابعی را محاسبه می کند که برنامه نویس باید بداند این تابع کدام است‪.‬حساب محموالت نوعی نشانه گذاری‬
‫از منطق رسمی است که برای مشخص کردن دقیق توابع پیچیده به کار می روند‪.‬‬
‫این نشانه گذاری به صورت }‪{P} {Q‬استفاده می شود و معنایش این است که اگر محمول ‪ P‬قبل از اجرای دستور ‪S‬‬
‫درست باشد و اگر ‪ S‬اجرا شود و خاتمه یابد‪،‬پس از خاتمه ‪،S‬محمول ‪ Q‬درست خواهد بود‪.‬باقواعد استنتاج می توانیم‬
‫این ساختار را در اثبات حساب محموالت به کار ببریم‪.‬‬
‫اگر مقدم در هر قاعده استنتاج درست باشد‪،‬تالی را به جای آن قرار می دهیم‪.‬بدین ترتیب می توانیم اثبات ساختارهای‬
‫برنامه را در حساب محموالت به کار ببریم‪.‬‬
‫مقدم‬
‫تالی‬
‫}‪{P}S{R‬‬
‫‪15‬‬
‫)‪{p}S{Q},(QR‬‬
‫قاعده استنتاج‬
‫‪consequence‬‬
‫وارسی اصل موضوعی‪:‬با عقبگرد در برنامه امکانپذیر است‪ .‬با دانستن پس شرط هردستور‪،‬مشخص کنید که چه‬
‫پیش شرطی قبل از اجرای آن دستور باید درست باشد‪،‬به عنوان مثال‪،‬اگر پس شرط دستور انتساب ‪X:=Y+Z‬برابر‬
‫با ‪ X>0‬باشد‪،‬با اصل موضوع انتساب زیر‪:‬‬
‫})‪{P{expr}}x :=expr{p(x‬‬
‫که در آن‪،P(x)=X>0،‬خواهیم داشت‪:‬‬
‫}‪{Y+Z > 0} X:=Y +Z {X>0‬‬
‫بنابراین پیش شرط دستور انتساب ‪Y + Z >0‬است‪.‬باادامه این روند می توانیم دنباله ای از دستورات‪،‬شامل‬
‫دستورات انتساب‪ if،‬و ‪while‬را اثبات کنیم‪.‬‬
‫قاعده اثبات برای دستور ‪ while‬ممکن است به صورت زیر بیان می شود‪:‬‬
‫‪If {p Λ B } S {P} then‬‬
‫} ‪{p} while B do s{p Λ¬ B‬‬
‫‪16‬‬
‫مثال ‪ 4_1‬برنامه ‪ MULT‬شکل ‪ 4_4‬را اثبات می کند که ‪Y=A * B‬را محاسبه می نماید‪ .‬با مطالعه برنامه می بینیم‬
‫که در هر بار اجرای حلقه ‪،while‬مقدار ‪a‬به ‪y‬اضافه می شود‪،‬در حالی که ‪ a*b‬به اندازه ‪a‬کاهش می یابد‪،‬زیرا یک‬
‫واحد از ‪b‬کم مشود‪ .‬لذا محمول تغییرناپذیر ‪ y+a*b =A*B Λ b ≥ 0‬به دست می آید‪.‬‬
‫شرط }‪{P}S{Q‬بیان می کند که اگر ‪ S‬خاتمه یابد و ‪P‬قبل از اجرای ‪S‬درست باشد‪Q ،‬پس از خاتمه ‪S‬درست خواهد‬
‫بود‪.‬برای دستورات انتساب و ‪if‬مشکلی وجود ندارد‪.‬فرض می شود که هردو خاتمه می یابند‪.‬باید ثابت شود که حلقه‬
‫‪while‬خاتمه می یابد‪.‬این کار به روش زیر انجام می شود‪:‬‬
‫‪.1‬نشان دهید که تابع صحیح ‪ f‬وجود دارد که هروقت حلقه خاتمه یافت‪ f>0،‬است‪.‬‬
‫‪.2‬اگر ‪ fi‬تابع ‪f‬را در ‪i‬امین اجرای حلقه نشان دهد‪.fi+1<fi،‬‬
‫اگر هر دو شرط درست باشند‪،‬حلقه خاتمه می یابد‪ .‬شکل ‪4.4‬‬
‫}‪{B≥ 0‬‬
‫{ ≡(‪1. MULT)A,B‬‬
‫; ‪2. a:=A‬‬
‫;‪3. b:=B‬‬
‫;‪4. y:=0‬‬
‫‪5. while b > 0 do‬‬
‫‪begin‬‬
‫‪6.‬‬
‫;‪y:=y+a‬‬
‫‪7.‬‬
‫;‪b:=b-1‬‬
‫}‪end‬‬
‫}‪{y=A*B‬‬
‫‪17‬‬
‫انواع داده جبری‬
‫عملیات بازنویسی ترم و اتحاد که قبال بحث شدند‪،‬نقش مهمی در توسعه مدل انواع داده جبری دارند‪.‬اگر رابطه بین‬
‫مجموعه ای از توابع را توصیف کنیم‪،‬هر پیاده سازی که از آن رابطه پیروی می کند‪،‬درست است‪.‬‬
‫به عنوان مثال‪،‬پشته ای از مقادیر صحیح را می توان با عملیات زیر تعریف کرد‪:‬‬
‫‪Push :‬‬
‫‪stack * integer  stack‬‬
‫‪Pop:‬‬
‫‪stack  stack‬‬
‫‪Top:‬‬
‫}‪stack  integer U {undefined‬‬
‫‪Empty:‬‬
‫‪stack  Boolean‬‬
‫‪Size:‬‬
‫‪stack  integer‬‬
‫‪Neestack:‬‬
‫‪ stack‬‬
‫‪ Push‬و ‪ pop‬عملیات آشنایی هستند و ‪top‬عنصر باالی پشته رابر می گرداند ولی آن را حذف نمی کند‪empty .‬‬
‫خالی بودن پشته را تست می کند و ‪ size‬تعداد عناصر پشته است و ‪ newstack‬نمونه ی جدیدی از پشته را ایجاد می‬
‫نماید‪.‬‬
‫‪18‬‬
‫تولید اصل موضوعی جبری‬
‫باتوجه به مجموعه ای از عملیاتی که نوع داده ای را مشخص می کند‪،‬رابطه بین این عملیات را می توانیم مشخص‬
‫کنیم‪.‬این عملیات را به سه دسته تقسیم می کنیم‪ :‬مولدها‪،‬سازنده ها و توابع‪.‬‬
‫برای نوع داده ‪،x‬مولد ‪g‬نمونه جدیدی از این نوع را تولید می کند و امضای آن به صورت زیر است‪:‬‬
‫مولدها‪.‬‬
‫‪g: not_x x‬‬
‫( ‪not_x‬هرنوعی غیر از ‪x‬است) در مثال پشته‪ newstack ،‬مولد است‪.‬‬
‫سازنده ها‪ .‬سازنده ‪C‬نمونه های نوع داده انتزاعی ‪ x‬را اصالح می کند و امضای آن به صورت زیر است‪:‬‬
‫‪c: x x not_x  x‬‬
‫در مثال پشته‪ push ،‬یک سازنده است‪.‬‬
‫توابع‪ .‬بقیه عملیات در نوع انتزاعی ‪، x‬توابع اند‪.‬در مثال پشته‪ size ،pop،top،‬و ‪ empty‬توابع اند‪.‬‬
‫‪19‬‬
‫از نظر شهودی می گوییم که شی ء ‪ y‬از نوع انتزاعی ‪،x‬می تواند با ااجرای مولد وتکرار اجرای سازنده ها ایجاد‬
‫شود‪.‬در مورد پشته ها‪،‬با استفاده از ‪ newstack‬یک پشته خالی ایجاد می شود و سپس ‪ push‬چندین بار اجرا می‬
‫شود تا عناصری در پشته قرار گیرد‪.‬به عنوان مثال‪،‬پشته حاوی ‪5 ،1‬و ‪3‬به صورت زیر ایجاد می شود‪:‬‬
‫)‪Push(push(push(newstack, 1),5),3‬‬
‫با اینکه مدل رسمی برای ایجاد اصل موضوعی جبری وجود ندارد ولی این روش آزمایشی به خوبی عمل می‬
‫کند‪.‬چون پشته دارای سه تابع‪،‬یک سازنده و یک مولد است‪6،‬اصل موضوعی الزم است‪.‬‬
‫به عنوان مثال‪،‬با تابع ‪top‬و سازنده ‪،push‬اصل موضوع به صورت زیر است‪:‬‬
‫…=))‪Top(push(s,l‬‬
‫از نظر شهودی‪،‬می خواهیم باالی پشته همان چیزی باشد که فعال در آن قرار داریم‪،‬بنابراین اصل موضوعی زیر را به‬
‫دست می آوریم‪:‬‬
‫‪Top(push(s,l)=l‬‬
‫‪20‬‬
:‫با ادامه این روند اصول زیر را به دست می آوریم‬
1: pop(newstack) =
newstack
2: pop(pus(S,I) =
S
3: top(newstack) =
undefined
4: top(push(s,l)) =
l
5: empty(newstack)= true
6: empty(push(s,l) = false
7:
size(newstack) =
0
8:
size(push(s,l) =
size(s) + 1
21
‫این اصل موضوعی به عنوان قواعد بازنویسی در نظر گرفته می شوند‪.‬می توانیم یک نمونه از شی ء را گرفته و با‬
‫استفاده از این قواعد‪،‬آن را به روش ساده تری بازنویسی کنیم‪.‬براساس مشخصات‪push ،‬نمونه ای ازپشته را‬
‫برمیگرداند که از نمونه دیگری از پشته و مقادیر صحیح ساخته شده است‪.‬برای مثال‪،‬با فراخوانی ‪newstack‬‬
‫تقاضای دیگری شکل می گیرد‪،‬سپس یک ‪،push‬بازهم یک ‪push‬و سپس یک ‪ pop‬و تابع ‪ empty‬عمل می‬
‫کند‪:‬‬
‫)))‪Empty(pop(push(push(newstack , 42 ), 17‬‬
‫اتحاد این عبارت با اصل موضوعی ‪، 2‬شکل ساده ای از خارجی ترین ترکیب ‪pop‬با ‪push‬را ارائه می کند و می‬
‫توانیم آن جمله را به صورت زیر بازنویسی کنیم‪:‬‬
‫))‪Empty(push(newstack, 42‬‬
‫در این نقطه می توانیم با استفاده از اصل موضوعی ‪، 6‬رشته را به ‪false‬ساده کنیم‪.‬می توانستیم این عبارت را‪،‬قبل از‬
‫اعمال تعریف ‪empty‬و به دست آوردن پاسخ ‪،false‬فقط به مولدها و سازنده ها ساده کنیم‪.‬‬
‫عبارت جبری که فقط از سازنده ها و مولدها استفاده می کند‪،‬به شکل نرمال یا کانونی است‪.‬‬
‫‪22‬‬
‫استقراء نوع داده‬
‫باتوجه به مجموعه ای از اصول موضوعی(یعنی رابطه های)بین مجموعه ای از عملیات در نوع داده جبری‪،‬الزم‬
‫است بررسی شود که بعضی از خواص ارزش درستی دارند‪.‬بدین ترتیب‪،‬این کار برای تمام برنامه هایی که این‬
‫مشخصات را پیاده سازی می کنند ( ‪ c‬یا پاسکال)ضروری است‪.‬‬
‫استقراء نوع داده (‪،)data type induction‬تکنیکی برای بررسی این عملیات است‪.‬‬
‫‪23‬‬
‫فرض کنید )‪ p(y‬محمولی به صورت ‪y‬عضو ‪x‬باشد‪.‬تحت چه شرایطی ‪ p‬برای همه اعضایی از نوع ‪ x‬درست‬
‫است؟همانند استقراء معمولی‪،‬می توانیم نشان دهیم که ‪ p‬برای اشیاء اولیه آن نوع درست و سپس نشان دهیم که وقتی‬
‫این اشیاء اولیه برای ساختن اشیاء جدید از آن نوع به کار می روند‪،‬خاصیت ‪ p‬درست باقی می ماند‪.‬‬
‫‪24‬‬
‫استقراء نوع داده را به صورت زیر تعریف می کنیم‪:‬‬
‫‪ .1‬با توجه به نوع ‪ x‬و توابع مولد ‪،fi‬سازنده های ‪ gi‬و سایر توابع ‪ hi‬و محمول )‪p(y‬برای ‪y‬عضو ‪.x‬‬
‫‪ .2‬نشان دهید که )‪ p(fi‬معتبر است‪ .‬این حالت پایه نشان می دهد که مقدار مولد درست است‪.‬‬
‫‪ .3‬با فرض اینکه )‪ p(y‬درست است‪،‬نشان دهید که ))‪ p(gi((y‬درست است‪.‬بدین ترتیب می توانیم محمول ‪ p‬را به‬
‫تمام اشیاء داده ای بسط دهیم که با استفاده از مولد و سازنده ها به وجود می آیند‪.‬‬
‫‪ .4‬سپس )‪ p(y‬را برای هر ‪ y‬از نوع ‪x‬نتیجه گیری کنید‪.‬‬
‫در مثال پشته‪،‬الزم است )‪ p(newstack‬و ))‪ p(push(x,i‬را نشان دهیم‪.‬با استفاده از استقراء نوع داده‪،‬می توانیم‬
‫نشان دهیم که قرار دادن مقداری در پشته‪،‬اندازه آن را افزایش می دهد‪.‬‬
‫)‪Size(push(s,x)) > size(s‬‬
‫‪25‬‬
‫پایان‬
‫‪26‬‬

similar documents