دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: نویسندگان: Nielson F., Nielson H.R سری: ISBN (شابک) : 9783030051556 ناشر: Springer سال نشر: 2019 تعداد صفحات: 170 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 1 Mb
در صورت تبدیل فایل کتاب Formal methods. An appetizer به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب روش های رسمی یک پیش غذا نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب درسی مقدمهای بر استفاده از روشهای رسمی است که از معناشناسی سازههای برنامهنویسی کلیدی گرفته تا تکنیکهای تجزیه و تحلیل و تأیید برنامهها را شامل میشود. نویسندگان از نمودارهای برنامه به عنوان مکانیزمی برای نمایش ساختار کنترل برنامه ها استفاده می کنند تا تعادلی بین کلیت و پیچیدگی مفهومی پیدا کنند. فصلهای اولیه نمودارهای برنامه و زبان فرمانهای محافظت شده مقدمه کافی برای اکثر خوانندگان است تا از یک رویکرد plug-and-play برای فصلهای باقیمانده لذت ببرند. اینها روشهای رسمی برای تجزیه و تحلیل رفتار برنامهها را به روشهای مختلف، از تأیید، از طریق تجزیه و تحلیل برنامه و امنیت مبتنی بر زبان، تا بررسی مدل، توضیح میدهند. فصلهای باقیمانده پسوندهای زبان را با رویهها و همزمانی ارائه میکنند و معنای آنها را پوشش میدهند. این کتاب برای دورههای پیشرفته کارشناسی و کارشناسی ارشد در توسعه نرمافزار مناسب است و متن با تمرینهایی با درجههای سختی متفاوت پشتیبانی میشود. نویسندگان یک محیط یادگیری آنلاین ایجاد کردهاند که به دانشآموزان اجازه میدهد تا نمونههایی فراتر از مواردی که در متن اصلی توضیح داده شده است ایجاد کنند، و در پیوستهای کتاب، پروژههای برنامهنویسی را با هدف اجرای بخشهای مرکزی توسعه با استفاده از زبان کاربردی F# ارائه میدهند.
This textbook is an introduction to the use of formal methods ranging from semantics of key programming constructs to techniques for the analysis and verification of programs. The authors use program graphs as the mechanism for representing the control structure of programs in order to find a balance between generality and conceptual complexity. The early chapters on program graphs and the Guarded Commands language are sufficient introduction for most readers to then enjoy a plug-and-play approach to the remaining chapters. These explain formal methods for analysing the behaviour of programs in various ways ranging from verification, via program analysis and language-based security, to model checking. The remaining chapters present language extensions with procedures and concurrency and cover their semantics. The book is suitable for advanced undergraduate and graduate courses in software development, and the text is supported throughout with exercises of varying grades of difficulty. The authors have developed an online learning environment that allows students to create examples beyond those covered in the main text, and in the book appendices they present programming projects aimed at implementing central parts of the development using the functional language F#.
Preface......Page 5
Prologue......Page 8
Contents......Page 13
1.1 Program Graphs......Page 16
1.2 Semantics......Page 18
1.3 The Structure of the Memory......Page 22
1.4 Properties of Program Graphs......Page 24
1.5 Bit-Level Semantics (Bonus Material)......Page 26
2.1 Syntax......Page 30
2.2 Program Graphs......Page 32
2.3 Semantics......Page 36
2.4 Alternative Approaches......Page 39
2.5 More Control Structures (Bonus Material)......Page 41
3.1 Predicates......Page 46
3.2 Predicate Assignments......Page 49
3.3 Partial Predicate Assignments......Page 51
3.4 Guarded Commands with Predicates......Page 55
3.5 Reverse Postorder (Bonus Material)......Page 58
4.1 Abstract Properties......Page 62
4.2 Analysis Assignments......Page 64
4.3 Analysis Functions......Page 66
4.4 Analysis Specification......Page 70
4.5 Computing Solutions (Bonus Material)......Page 73
5.1 Information Flow......Page 76
5.2 Reference-Monitor Semantics......Page 78
5.3 Security Analysis......Page 82
5.4 Multi-Level Security......Page 85
5.5 Non-Interference (Bonus Material)......Page 88
6.1 Transition Systems......Page 92
6.2 Computation Tree Logic – CTL......Page 95
6.3 Syntax and Semantics of CTL......Page 97
6.4 From Program Graphs to Transition Systems......Page 99
6.5 Towards an Algorithm (Bonus Material)......Page 101
7.1 Declarations......Page 106
7.2 Blocks......Page 108
7.3 Procedures with Dynamic Scope......Page 113
7.4 Procedures with Static Scope......Page 119
8.1 Shared Variables......Page 124
8.2 Asynchronous Communication......Page 127
8.3 Synchronous Communication......Page 132
8.4 Broadcast and Gather (Bonus Material)......Page 134
Epilogue......Page 139
Appendix A: The MicroC Language......Page 142
Appendix B: Programming Projects......Page 145
C.1 The Core Development......Page 148
C.2 Program Verification......Page 151
C.3 Program Analysis......Page 153
C.4 Language-Based Security......Page 156
Appendix D: A Learning Environment......Page 159
D.1 The Welcome Screen......Page 160
D.2 Step-Wise Execution......Page 161
D.3 Verification Conditions......Page 162
D.4 Detection of Signs Analysis......Page 163
D.5 Security Analysis......Page 164
Symbols......Page 165
Index......Page 167