5.1.4.1. אקסיומות

אקסיומת ההצבה - plot:$\left\{ {p\left[ {x \leftarrow e} \right]}
 \right\}x: = e\left\{ p \right\}$. (תסומן ב-ASS)

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

plot:$p\left[ {x
 \leftarrow e} \right]$ הוא התנאי החלש ביותר שמבטיח ש-plot:$p$ יתקיים לאחר ביצוע plot:$x: = e$. משמעותו: לקחנו את התוכנית plot:$p$ והצבנו בכל מקום במקום plot:$x$ את הערך plot:$e$.

דוגמא 1: נביט בחלק הימני: plot:$x: = x + 5\left\{ {x < 0} \right\}$ - השאלה שאנחנו שואלים הינה: "מה צריך לדרוש כדי שיתקיים plot:$x < 0$ אחרי ביצוע של הפעולה plot:$x:
 = x + 5$?". התשובה היא plot:$x <  -
 5$, ולכן נכתוב: plot:$\left\{ {x < 
 - 5} \right\}x: = x + 5\left\{ {x < 0} \right\}$. מבחינת טכניקה: נוכל לקבל את הצד השמאלי על ידי הצבת plot:$e$ בכל מקום שבו מופיע plot:$x$ ב-plot:$p$, וכך לייצר את הצד השמאלי.

לחילופין, אם נתון רק הצד השמאלי: plot:$\left\{ p \right\}y: = t\left\{ ? \right\}$ אנחנו יכולים ליצור את הצד הימני באופן אינטואיטיבי, על ידי הפעלת הפקודה שבתוכנית על החלק השמאלי.

ניסוח חלופי לאקסיומת ההצבה: מדוע לא ניסחנו טענה בסגנון plot:$\left\{ {true}
 \right\}x: = e\left\{ {x = e} \right\}$? מכיוון שכאן אין קשר בין המצב ההתחלתי לסופי. ראו לדוגמא: plot:$\left\{ {true} \right\}x: = x + 1\left\{
 {\underbrace {x = x + 1}_{false}} \right\}$. כאשר plot:$e$ אינו תלוי ב-plot:$x$ מתקיים כי plot:$\left\{
 {true} \right\}x: = e\left\{ {x = e} \right\}$ היא אקסיומה נכונה. למשל: plot:$\left\{ {true}
 \right\}x: = 5\left\{ {x = 5} \right\}$



אקסיומת skip - plot:$\left\{
 p \right\}skip\left\{ p \right\}$. האקסיומה תסומן plot:$SKIP$.

אקסיומות אריתמטיות: כל טענה מהצורה plot:$q \to q'$ שהינה אמת לוגית הינה אקסיומה. אקסיומות אלו יסומנו ב-plot:$ARITH$.

אין תגובות!
שיתוף:
| עוד