5.1.4.1. אקסיומותאקסיומת ההצבה - . (תסומן ב-ASS) האקסיומה הראשונה שנציג הינה אקסיומת ההצבה. אקסיומה זו מעט מסובכת להבנה בהתקלות ראשונה, ולכן נסביר אותה בפירוט. דגש ראשון: את אקסיומת ההצבה קוראים מימין לשמאל. הוא התנאי החלש ביותר שמבטיח ש- יתקיים לאחר ביצוע . משמעותו: לקחנו את התוכנית והצבנו בכל מקום במקום את הערך . דוגמא 1: נביט בחלק הימני: - השאלה שאנחנו שואלים הינה: "מה צריך לדרוש כדי שיתקיים אחרי ביצוע של הפעולה ?". התשובה היא , ולכן נכתוב: . מבחינת טכניקה: נוכל לקבל את הצד השמאלי על ידי הצבת בכל מקום שבו מופיע ב-, וכך לייצר את הצד השמאלי. לחילופין, אם נתון רק הצד השמאלי: אנחנו יכולים ליצור את הצד הימני באופן אינטואיטיבי, על ידי הפעלת הפקודה שבתוכנית על החלק השמאלי. ניסוח חלופי לאקסיומת ההצבה: מדוע לא ניסחנו טענה בסגנון ? מכיוון שכאן אין קשר בין המצב ההתחלתי לסופי. ראו לדוגמא: . כאשר אינו תלוי ב- מתקיים כי היא אקסיומה נכונה. למשל:
אקסיומת skip - . האקסיומה תסומן . אקסיומות אריתמטיות: כל טענה מהצורה שהינה אמת לוגית הינה אקסיומה. אקסיומות אלו יסומנו ב-.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |