دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Algebraic Semantics of Imperative Programs
دانلود کتاب معناشناسی جبری از برنامههای حاکم بر
مشخصات کتاب
Algebraic Semantics of Imperative Programs
ویرایش: نویسندگان: Joseph A. Goguen, Grant Malcolm سری: Foundations of Computing ISBN (شابک) : 026207172X, 9780262071727 ناشر: The MIT Press سال نشر: 1996 تعداد صفحات: 229 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 26 مگابایت
قیمت کتاب (تومان) : 53,000
در صورت تبدیل فایل کتاب Algebraic Semantics of Imperative Programs به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب معناشناسی جبری از برنامههای حاکم بر نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب معناشناسی جبری از برنامههای حاکم بر
معناشناسی جبری برنامههای امری مقدمه‌ای مستقل و جدید «قابل اجرا» برای استدلال رسمی درباره برنامههای امری ارائه می‌کند. هدف اصلی نویسندگان بهبود توانایی برنامه نویسی با بهبود شهود در مورد معنای برنامه ها و نحوه اجرای آنها است. معنای برنامه های ضروری در یک نماد رسمی و پیاده سازی شده به زبان OBJ مشخص شده است. این امر معناشناسی را بسیار دقیق و در عین حال ساده می کند و برای تأیید مکانیکی ویژگی های برنامه پشتیبانی می کند. OBJ برای معناشناسی جبری طراحی شده است. اعلان‌های آن نمادهایی را برای مرتب‌سازی و توابع معرفی می‌کنند، عبارات آن معادلات هستند، و محاسبات آن اثبات‌های معادله‌ای هستند. بنابراین، یک \"برنامه\" OBJ یک نظریه معادله است و هر محاسبات OBJ یک قضیه را در مورد چنین نظریه ای اثبات می کند. این بدان معناست که یک برنامه OBJ که برای تعریف معنایی یک برنامه استفاده می شود، از قبل دارای یک معنای ریاضی دقیق است. علاوه بر این، تکنیک‌های استاندارد برای مکانیزه کردن استدلال معادله را می‌توان برای تأیید بدیهیات که تأثیر برنامههای امری را بر ماشین‌های انتزاعی توصیف می‌کنند، استفاده کرد. سپس می‌توان از این بدیهیات در اثبات مکانیکی ویژگی‌های برنامه‌ها استفاده کرد. معناشناسی جبری برنامههای امری که برای دانش‌آموزان پیشرفته یا دانشجویان مقطع کارشناسی ارشد در نظر گرفته شده است، شامل مثال‌ها و تمرین‌های بسیاری در راستی‌آزمایی برنامه است که همه آنها را می‌توان در OBJ انجام داد.
توضیحاتی درمورد کتاب به خارجی
Algebraic Semantics of Imperative Programs presents a self-contained and novel "executable" introduction to formal reasoning about imperative programs. The authors' primary goal is to improve programming ability by improving intuition about what programs mean and how they run.The semantics of imperative programs is specified in a formal, implemented notation, the language OBJ; this makes the semantics highly rigorous yet simple, and provides support for the mechanical verification of program properties.OBJ was designed for algebraic semantics; its declarations introduce symbols for sorts and functions, its statements are equations, and its computations are equational proofs. Thus, an OBJ "program" is an equational theory, and every OBJ computation proves some theorem about such a theory. This means that an OBJ program used for defining the semantics of a program already has a precise mathematical meaning. Moreover, standard techniques for mechanizing equational reasoning can be used for verifying axioms that describe the effect of imperative programs on abstract machines. These axioms can then be used in mechanical proofs of properties of programs.Intended for advanced undergraduates or beginning graduate students, Algebraic Semantics of Imperative Programs contains many examples and exercises in program verification, all of which can be done in OBJ.
