libm3/src/sequence/Sequence.mg


 Copyright 1993 Digital Equipment Corporation.             
 Distributed only by permission.                           
 See the file COPYRIGHT for a full description.            
                                                           
 Last modified on Thu Sep 22 19:45:14 PDT 1994 by heydon   
      modified on Thu Sep  8 15:15:04 PDT 1994 by kalsow   
      modified on Tue Aug  9 15:58:24 PDT 1994 by detlefs  
      modified on Mon Oct 25 11:00:36 PDT 1993 by mcjones  
      modified on Mon Jun 28 13:20:59 PDT 1993 by gnelson  
<*PRAGMA SPEC, LOOPINV*>

GENERIC MODULE Sequence(Elem, Seq, Rep);
Where Seq = Sequence(Elem) and Rep = SequenceRep(Elem, Seq).

REVEAL Seq.T = Rep.Public BRANDED Seq.Brand OBJECT
  OVERRIDES
    init := Init;
    fromArray := FromArray;
    addhi := Addhi;
    addlo := Addlo;
    remhi := Remhi;
    remlo := Remlo;
    put := Put;
    size := Size;
    gethi := Gethi;
    getlo := Getlo;
    get := Get
  END;

VAR zero: Elem.T;
Modula-3 requires zero to be initialized to a value of type Elem.T. With high probability the references within that value will be NIL. Hence, setting elements of the sequence to zero should avoid storage leaks.

<*SPEC INVARIANT (ALL [t1: Seq.T, t2: Seq.T]
                    t1 # t2 IMPLIES t1.elem # t2.elem) *>

PROCEDURE Init(s: Seq.T; sizeHint: CARDINAL): Seq.T =
  BEGIN
    IF s.elem = NIL OR NUMBER(s.elem^) = 0 THEN
      s.elem := NEW(Rep.RefArray, MAX(sizeHint, 1))
    ELSE
      (* Clear the previous entries to help the GC *)
      FOR i := s.st TO MIN(s.st + s.sz - 1, LAST(s.elem^)) DO
        s.elem[i] := zero;
      END;
      FOR i := 0 TO MAX(-1, s.st + s.sz - 1 - NUMBER(s.elem^)) DO
        s.elem[i] := zero;
      END;
    END (* IF *);
    s.sz := 0; s.st := 0;
    RETURN s
  END Init;

PROCEDURE FromArray(s: Seq.T; READONLY a: ARRAY OF Elem.T): Seq.T =
  <*SPEC LET numA := NUMBER(a)*>
  <*SPEC LET raPre := Rep.RefArray *>
  BEGIN
    s.sz := NUMBER(a);
    s.st := 0;
    s.elem := NEW(Rep.RefArray, MAX(s.sz, 1));
    FOR i := 0 TO s.sz-1 DO
      <*LOOPINV (ALL [j: INTEGER]
                   (0 <= j AND j < i) IMPLIES s.elem^[j] = a[j])
                AND NUMBER(s.elem^) = numA
                AND (ALL [r: Rep.RefArray]
                        Rep.RefArray[r] = raPre[r] OR r = s.elem) *>
      s.elem[i] := a[i]
    END;
    RETURN s
  END FromArray;

PROCEDURE Addhi(s: Seq.T; READONLY x: Elem.T) =
  BEGIN
    IF s.sz = NUMBER(s.elem^) THEN Expand(s) END;
    VAR i := s.st + s.sz; BEGIN
      IF i >= NUMBER(s.elem^) THEN i := i - NUMBER(s.elem^) END;
      s.elem[i] := x
    END;
    INC(s.sz)
  END Addhi;

PROCEDURE Addlo(s: Seq.T; READONLY x: Elem.T) =
  BEGIN
    IF s.sz = NUMBER(s.elem^) THEN Expand(s) END;
    VAR i := s.st; BEGIN
      IF i = 0 THEN i := LAST(s.elem^) ELSE i := i - 1 END;
      s.elem[i] := x;
      s.st := i
    END;
    INC(s.sz)
  END Addlo;

PROCEDURE Expand(s: Seq.T) =
  VAR
    n := NUMBER(s.elem^);
    new := NEW(Rep.RefArray, 2 * n);
    m := n - s.st;
  BEGIN
    SUBARRAY(new^, 0, m) := SUBARRAY(s.elem^, s.st, m);
    SUBARRAY(new^, m, s.st) :=
      SUBARRAY(s.elem^, 0, s.st);
    s.st := 0;
    s.elem := new
   END Expand;

PROCEDURE Remhi(s: Seq.T): Elem.T =
  VAR
    j := s.st + s.sz - 1;
    res: Elem.T;
  BEGIN
    IF j >= NUMBER(s.elem^) THEN j := j - NUMBER(s.elem^) END;
    DEC(s.sz);
    WITH z = s.elem[j] DO  res := z;  z := zero;  END;
    RETURN res;
  END Remhi;

PROCEDURE Remlo(s: Seq.T): Elem.T =
  VAR res: Elem.T;
  BEGIN
    WITH z = s.elem[s.st] DO  res := z;  z := zero;  END;
    DEC(s.sz);
    INC(s.st);
    IF s.st = NUMBER(s.elem^) THEN s.st := 0 END;
    RETURN res
  END Remlo;

PROCEDURE Put(s: Seq.T; i: CARDINAL; READONLY x: Elem.T) =
  VAR j := s.st + i; BEGIN
    <* ASSERT i < s.sz *>
    IF j >= NUMBER(s.elem^) THEN j := j - NUMBER(s.elem^) END;
    s.elem[j] := x
  END Put;

PROCEDURE Get(s: Seq.T; i: CARDINAL): Elem.T =
  VAR j := s.st + i; BEGIN
    <* ASSERT i < s.sz *>
    IF j >= NUMBER(s.elem^) THEN j := j - NUMBER(s.elem^) END;
    RETURN s.elem[j]
  END Get;

PROCEDURE Size(s: Seq.T): CARDINAL =
  BEGIN
    RETURN s.sz
  END Size;

PROCEDURE Gethi(s: Seq.T): Elem.T =
  VAR j := s.st + s.sz - 1; BEGIN
    <* ASSERT s.sz > 0 *>
    IF j >= NUMBER(s.elem^) THEN
      j := j - NUMBER(s.elem^)
    END;
    RETURN s.elem[j]
  END Gethi;

PROCEDURE Getlo(s: Seq.T): Elem.T =
  BEGIN
    <* ASSERT s.sz > 0 *>
    RETURN s.elem[s.st]
  END Getlo;

PROCEDURE Cat(s, t: T): T =
  VAR u := NEW(Seq.T);
      <*SPEC LET raPre := Rep.RefArray *>
      <*SPEC LET dPreS := Data[s] *>
      <*SPEC LET dPreT := Data[t] *>
  BEGIN
    u.sz := s.sz + t.sz;
    u.elem := NEW(Rep.RefArray, MAX(u.sz, 1));
    FOR i := 0 TO s.sz-1 DO
      <*LOOPINV NUMBER(u.elem^) = MAX(u.sz, 1)
            AND (ALL [x: Rep.RefArray]
                     Rep.RefArray[x] = raPre[x] OR x = u.elem)
            AND (ALL [j: INTEGER] (0 <= j AND j < i) IMPLIES
                   u.elem^[j] = Rep.Abs(raPre[s.elem], s.st, s.sz)[j]) *>
      u.elem[i] := s.get(i)
    END;
    FOR i := 0 TO t.sz-1 DO
      <*LOOPINV NUMBER(u.elem^) = MAX(u.sz, 1)
            AND (ALL [x: Rep.RefArray]
                     Rep.RefArray[x] = raPre[x] OR x = u.elem)
            AND (ALL [j: INTEGER] (0 <= j AND j < s.sz) IMPLIES
                   u.elem^[j] = dPreS[j])
                AND
                (ALL [j: INTEGER] (0 <= j AND j < i) IMPLIES
                   u.elem^[j + s.sz] = dPreT[j]) *>
      u.elem[i + s.sz] := t.get(i)
    END;
    RETURN u
  END Cat;

PROCEDURE Sub(s: T; start: CARDINAL;
    length: CARDINAL := LAST(CARDINAL)): T =
  VAR u := NEW(Seq.T);
      <*SPEC LET raPre := Rep.RefArray *>
      <*SPEC LET dPreS := Data[s] *>
  BEGIN
    IF start >= s.sz OR length = 0 THEN
      u.sz := 0
    ELSE
      u.sz := MIN(length, s.sz - start)
    END;
    u.elem := NEW(Rep.RefArray, MAX(u.sz, 1));
    FOR i := 0 TO u.sz-1 DO
      <*LOOPINV NUMBER(u.elem^) = MAX(u.sz, 1)
            AND (ALL [x: Rep.RefArray]
                     Rep.RefArray[x] = raPre[x] OR x = u.elem)
            AND (ALL [j: INTEGER] (0 <= j AND j < i) IMPLIES
                   u.elem^[j] = dPreS[start + j]) *>
      u.elem[i] := s.get(start + i)
    END;
    RETURN u
  END Sub;
ESC specs...
<*SPEC Init(s, sizeHint)
       MODIFIES Valid[s], Data[s]
       REQUIRES s # NIL
       ENSURES RES = s AND Valid'[s] AND NUMBER(Data'[s]) = 0
*>

<*SPEC FromArray(s, a)
       MODIFIES Valid[s], Data[s]
       REQUIRES s # NIL
       ENSURES RES = s AND Valid'[s] AND NUMBER(Data'[s]) = NUMBER(a)
           AND (ALL [i: INTEGER] (0 <= i AND i < NUMBER(a)) IMPLIES
                                 Data'[s][i] = a[i])
*>

<*SPEC Addhi(s, x)
       MODIFIES Valid[s], Data[s]
       REQUIRES Valid[s] AND s # NIL
       ENSURES Valid'[s]
           AND NUMBER(Data'[s]) = NUMBER(Data[s])+1
           AND (ALL [i: INTEGER] 0 <= i AND i < NUMBER(Data[s]) IMPLIES
                  Data'[s][i] = Data[s][i])
           AND Data'[s][NUMBER(Data[s])] = x
*>

<*SPEC Addlo(s, x)
       MODIFIES Valid[s], Data[s]
       REQUIRES Valid[s] AND s # NIL
       ENSURES Valid'[s]
           AND NUMBER(Data'[s]) = NUMBER(Data[s])+1
           AND Data'[s][0] = x
           AND (ALL [i: CARDINAL]
                 (0 <= i AND i < NUMBER(Data[s])) IMPLIES
                    Data'[s][i+1] = Data[s][i])
*>

<*SPEC Expand(s)
       MODIFIES Valid[s], Data[s]
       REQUIRES Valid[s]
       ENSURES Valid'[s]
           AND s.st' = 0 AND s.sz' = s.sz
           AND NUMBER(s.elem'^') > NUMBER(s.elem^)
           AND (ALL [i: INTEGER] (0 <= i AND i < NUMBER(Data[s])) IMPLIES
                  Data'[s][i] = Data[s][i])
           AND FRESH(s.elem')
*>

<*SPEC Remhi(s)
       MODIFIES Valid[s], Data[s]
       REQUIRES s # NIL AND Valid[s] AND NUMBER(Data[s]) > 0
       ENSURES Valid'[s] AND NUMBER(Data'[s]) = NUMBER(Data[s])-1
           AND (ALL [i: INTEGER] (0 <= i AND i < NUMBER(Data'[s])) IMPLIES
                  Data'[s][i] = Data[s][i])
*>

<*SPEC Remlo(s)
       MODIFIES Valid[s], Data[s]
       REQUIRES s # NIL AND Valid[s] AND NUMBER(Data[s]) > 0
       ENSURES Valid'[s] AND NUMBER(Data'[s]) = NUMBER(Data[s])-1
           AND (ALL [i: INTEGER] (0 <= i AND i < NUMBER(Data'[s])) IMPLIES
                  Data'[s][i] = Data[s][i+1])
*>

<*SPEC Put(s, i, x)
       MODIFIES Valid[s], Data[s][i]
       REQUIRES s # NIL AND Valid[s] AND i < NUMBER(Data[s])
       ENSURES Valid'[s] AND Data'[s][i] = x
           AND NUMBER(Data'[s]) = NUMBER(Data[s])
*>

<*SPEC Size(s)
       REQUIRES s # NIL AND Valid[s]
       ENSURES RES = NUMBER(Data[s])
*>

<*SPEC Gethi(s)
       REQUIRES s # NIL AND Valid[s] AND NUMBER(Data[s]) > 0
       ENSURES RES = Data[s][NUMBER(Data[s])-1]
*>

<*SPEC Getlo(s)
       REQUIRES s # NIL AND Valid[s] AND NUMBER(Data[s]) > 0
       ENSURES RES = Data[s][0]
*>

<*SPEC Get(s, i)
       REQUIRES s # NIL AND Valid[s] AND i < NUMBER(Data[s])
       ENSURES RES = Data[s][i]
*>

BEGIN
END Sequence.