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

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

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

5.1. הגישה המודולרית של Hoare

בתחילת המסמך הצגנו כי עבור מערכת הוכחה צריך:

  • שפת תכנות עם סמנטיקה פורמלית.
  • שפת מפרט עם סמנטיקה פורמלית.
  • שיטת/כללי הוכחה.

כעת נציג שפת תכנות נוספת שאינה PLF.

  • שפת המפרט: נבחר בשפת מפרט זהה לזו שהשתמשנו בה עד כה.
  • שפת התכנות: שפת התכנות תהיה שפה דמויית C בשם while-program.
  • שיטת / כללי הוכחה:
  • השם "הגישה המודולרית" נובע מכיוון שיהיה ניתן להוכיח טענה על חלקים מהתוכנית, ולאחר מכן לחבר טענות לטענות גדולות יותר.
  • נוכיח את הטענות באמצעות אקסיומות וכללי היסק, ולכן נציג בעצם חישובים שהם "לוגיקה מעל תוכניות". (בניגוד לדוגמאות שהצגנו ב-PLF, בהם הצגנו שיטות להוכחה, אבל לא היתה הוכחה פורמלית מסודרת על שלבי התוכנית).

תגיות המסמך:

לפרק הקודם5. לוגיקה של תוכניות
לפרק הבא5.1.1. שפת תוכניות while
אין תגובות!
שיתוף:
| עוד