הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

4.4. שיטת / כללי ההוכחה

כדי להוכיח נכונות של תוכנית בשפת תרשימי הזרימה נציג כללים, שבמידה והם יתקיימו נאמר כי התוכנית נכונה. נתחיל במקרה הפשוט בו בתוכנית אין מעגלים (לולאות). במקרה זה מובטחת עצירה של התוכנית, ולכן נכונות חלקית ונכונות מלאה נובעות זו מזו. לאחר מכן נרחיב את הכללים גם למצב בו התוכניות כוללת לולאה אחת או יותר.

בשלב הראשון: המטרה שלנו בהנתן תרשים זרימה: נרצה להראות שכל חישוב מלא (חסר מעגלים) שמספק את plot:${q_1}\left( {\bar x} \right)$ מספק בסופו את plot:${q_2}\left( {\bar x} \right)$.

תגיות המסמך:

לפרק הקודם4.3. למת ההפרדה
לפרק הבא4.4.1. הגדרות – טרנספורמצית המצבים, תנאי הישיגות
אין תגובות!
שיתוף:
| עוד