MODULE ObxSample;
(**

   project   = "BlackBox"
   organization   = "www.oberon.ch"
   contributors   = "Oberon microsystems"
   version   = "System/Rsrc/About"
   copyright   = "System/Rsrc/About"
   license   = "Docu/BB-License"
   changes   = ""
   issues   = ""

**)

   TYPE

      File* = POINTER TO RECORD
         len: INTEGER   (* hidden instance variable *)
      END;
      Rider* = POINTER TO RECORD

         (* there may be several riders on one file *)
         file-: File;   (* read-only instance variable *)
         eof*: BOOLEAN;   (* fully exported instance variable *)
         pos: INTEGER   (* hidden instance variable *)
            (* Invariant: (pos >= 0) & (pos < file.len) *)
      END;
   PROCEDURE (f: File) GetLength* (OUT length: INTEGER), NEW;

   BEGIN
      length := f.len
   END GetLength;
   PROCEDURE (rd: Rider) SetPos* (pos: INTEGER), NEW;

   BEGIN
      (* assert invariants, so that errors may not be propagated across components *)
      ASSERT(pos >= 0); ASSERT(pos < rd.file.len);
      rd.pos := pos
   END SetPos;
   (* ... *)

END ObxSample.