פתרון מודל וכשל נשלט

פתרון ראשון

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

פתרון שני

נוסיף לתוכנית ההרצאה את הניסוי הבא בתוך הפונקציה הראשית, לפני החזרה המוצלחת. הוא משתמש בפונקציות ובטיפוס המעטפת שכבר הוגדרו.

let mut writer = FaultWriter { bytes: base.clone(), remaining: 3 };
assert!(append(&mut writer, b"new-data").is_err());
let (_, valid) = recover(&writer.bytes);
writer.remaining = 100;
append(&mut writer, b"later")?;
assert_eq!(recover(&writer.bytes).0, vec![b"old".to_vec()]);
writer.bytes.truncate(valid);
append(&mut writer, b"later")?;
assert_eq!(recover(&writer.bytes).0,
    vec![b"old".to_vec(), b"later".to_vec()]);

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

פתרון שלישי

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

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