---

 
Machine

file : M1.mch
/*
  Example of Operation Refinement
  C. Attiogbe
  Univ-Nantes.fr
*/
MODEL
   M1
SETS
   STATUS = {Ok, Error}
OPERATIONS
res, status <-- chek_xx(xx) =
  /* returns x-1 if x /= 0 otherwise raise an error */ 
  PRE
        xx : INT
  &     MININT <= xx - 1
  THEN
        res :: INT
  ||    status :: STATUS
  END
END

---

Refinement

file : M1R1.ref
/*
  Example of Operation Refinement
  C. Attiogbe
  Univ-Nantes.fr
*/
REFINEMENT
   M1R1
REFINES
   M1
OPERATIONS
   res, status <-- chek_xx(xx) =
/* returns x-1 if x /= 0 otherwise raise an error */
  PRE
        xx : INT
  &     MININT <= xx-1
  THEN

  CHOICE
        res := xx-1
  ||    status := Ok
  OR
        res := -1
  ||    status := Error
  END
  END
END

---

Implementation

file : M1I1.imp
/*
  Example of Operation Refinement
  C. Attiogbe
  Univ-Nantes.fr
*/

IMPLEMENTATION
   M1I1
REFINES
   M1R1
OPERATIONS
res, status <-- chek_xx(xx) =
/* returns x-1 if x /= 0 otherwise raise an error */
  BEGIN
  IF xx /= 0
  THEN
        res := xx-1
  ;     status := Ok
  ELSE
        res := -1
  ;     status := Error
  END
  END
END

---

Christian Attiogbé