MACHINE      Rename_fstr_obj(maxobj,maxmem)

CONSTRAINTS  maxobj>0

SEES         Bool_TYPE, Rename_fstr_ctx

VARIABLES    Rename_fstrtok, Rename_fstrstruct, Rename_fstrmem

INVARIANT

  Rename_fstrtok <: Rename_FSTROBJ &
  Rename_fstrstruct: Rename_fstrtok --> seq(0..255) &
  Rename_fstrmem:  NAT

INITIALISATION

  Rename_fstrtok, Rename_fstrstruct, Rename_fstrmem := {},{}, 0

OPERATIONS

/****************** General query functions *******************/

  bb <-- Rename_MEM_FUL_FSTR_OBJ =
  BEGIN
    bb:=bool(Rename_fstrmem=maxmem)
  END;

  bb <-- Rename_OBJ_FUL_FSTR_OBJ =
  BEGIN
    bb:=bool(card(Rename_fstrtok) = maxobj)
  END;

  bb <-- Rename_XST_FSTR_OBJ(pp) =
  PRE
    pp: Rename_FSTROBJ
  THEN
    bb:=bool(pp:Rename_fstrtok)
  END;

  pp <-- Rename_ANY_FSTR_OBJ =
  BEGIN
    pp :: Rename_FSTROBJ
  END;


/*************** Creating and deleting strings ******************/

  Rename_INI_FSTR_OBJ =
  BEGIN
    Rename_fstrtok, Rename_fstrstruct, Rename_fstrmem := {},{}, 0
  END;


  bb,pp <-- Rename_CRE_FSTR_OBJ =
  IF card(Rename_fstrtok) < maxobj THEN
      ANY qq WHERE
        qq: Rename_FSTROBJ - Rename_fstrtok
      THEN
        Rename_fstrstruct(qq):=<> ||
        Rename_fstrtok := Rename_fstrtok \/ {qq} ||
        pp:=qq ||
        bb:= TRUE
      END
  ELSE
      bb:=FALSE
  END;


  bb,pp <-- Rename_NEW_FSTR_OBJ(nn) =
  PRE
     card(Rename_fstrtok) < maxobj &
     nn : seq(0..255) 
     /* Rename_fstrmem + size(nn) <= maxmem */
  THEN 
     IF Rename_fstrmem + size(nn) <= maxmem THEN
       ANY qq WHERE
         qq: Rename_FSTROBJ - Rename_fstrtok
       THEN
         Rename_fstrstruct(qq):=nn ||
         Rename_fstrtok := Rename_fstrtok \/ {qq} ||
         Rename_fstrmem := Rename_fstrmem + size(nn) ||
         pp:=qq ||
         bb:=TRUE
       END
     ELSE
       bb := FALSE ||
       pp :: Rename_FSTROBJ
     END
 END;


  Rename_KIL_FSTR_OBJ(pp) =
  PRE
    pp: Rename_fstrtok
  THEN
    Rename_fstrstruct :=  {pp} <<| Rename_fstrstruct ||
    Rename_fstrtok := Rename_fstrtok - {pp} ||
    Rename_fstrmem := Rename_fstrmem - size(Rename_fstrstruct(pp))
  END;


/*********************** Query operations ***********************/


  vv <-- Rename_VAL_FSTR_OBJ(pp,ii) =
  PRE
    pp:Rename_fstrtok &
    ii:1..size(Rename_fstrstruct(pp))
  THEN 
    vv:=Rename_fstrstruct(pp)(ii)
  END;

  bb <-- Rename_EMP_FSTR_OBJ(pp) =
  PRE
    pp: Rename_fstrtok
  THEN
    bb:=bool(Rename_fstrstruct(pp)=<>)
  END;

  bb <-- Rename_XST_IDX_FSTR_OBJ(pp,ii) =
  PRE
    pp: Rename_fstrtok &
    ii: 1..maxmem
  THEN
    bb:=bool(ii:1..size(Rename_fstrstruct(pp)))
  END;

  nn <-- Rename_LEN_FSTR_OBJ(pp)=
  PRE
    pp: Rename_fstrtok
  THEN
    nn:=size(Rename_fstrstruct(pp))
  END;

  bb <-- Rename_SMR_FSTR_OBJ(ss,tt) =
  PRE
     tt : Rename_fstrtok &
     ss : Rename_fstrtok
  THEN
    bb :: BOOL 
  END;

  bb <-- Rename_EQL_FSTR_OBJ(ss,tt) =
  PRE
     tt : Rename_fstrtok &
     ss : Rename_fstrtok
  THEN
     bb := bool(Rename_fstrstruct(tt) = Rename_fstrstruct(ss))
  END;

  bb <-- Rename_EQL_LIT_FSTR_OBJ(tt,nn) =
  PRE
     tt : Rename_fstrtok &
     nn : seq(0..255)
  THEN
     bb := bool(Rename_fstrstruct(tt) = nn)
  END;


  ss <-- Rename_XTR_FSTR_OBJ(pp) =
  PRE
    pp : Rename_fstrtok
  THEN
    ss := Rename_fstrstruct(pp)
  END;

/**************** String operations **************************/

  Rename_CLR_FSTR_OBJ(pp) =
  PRE
    pp: Rename_fstrtok
  THEN
    Rename_fstrstruct(pp) := <> ||
    Rename_fstrmem := (
     Rename_fstrmem - size(Rename_fstrstruct(pp))
    )
  END;


  bb <-- Rename_PSH_FSTR_OBJ(pp,vv) =
  PRE
    pp:Rename_fstrtok &
    vv: 0..255 
    /* Rename_fstrmem<maxmem */
  THEN
    IF Rename_fstrmemTHEN
      Rename_fstrstruct(pp):=Rename_fstrstruct(pp) <- vv ||
      Rename_fstrmem:=Rename_fstrmem+1 ||
      bb:=TRUE
    ELSE
      bb:=FALSE
    END
  END;

  Rename_KEP_FSTR_OBJ(pp,ii) =
  PRE
    pp:Rename_fstrtok &
    ii:0..size(Rename_fstrstruct(pp))
  THEN
    Rename_fstrstruct(pp):=Rename_fstrstruct(pp) /|\ ii ||
    Rename_fstrmem:= (
     Rename_fstrmem-size(Rename_fstrstruct(pp))+ii
    )
  END;

  Rename_CUT_FSTR_OBJ(pp,ii) =
  PRE
    pp:Rename_fstrtok &
    ii:0..size(Rename_fstrstruct(pp))
  THEN
    Rename_fstrstruct(pp):=Rename_fstrstruct(pp) \|/ ii ||
    Rename_fstrmem:=Rename_fstrmem-ii
  END;

  Rename_REV_FSTR_OBJ(pp) =
  PRE
    pp:Rename_fstrtok
  THEN
    Rename_fstrstruct(pp):=rev(Rename_fstrstruct(pp))
  END;

  Rename_SWP_FSTR_OBJ(pp,ii,jj) =
  PRE
    pp:Rename_fstrtok &
    ii:0..size(Rename_fstrstruct(pp)) &
    jj:0..size(Rename_fstrstruct(pp))
  THEN
    Rename_fstrstruct(pp):= (
     Rename_fstrstruct(pp) <+ (
        {ii |-> Rename_fstrstruct(pp)(jj), jj |-> Rename_fstrstruct(pp)(ii)}
        )
     )

  END;

  Rename_POP_FSTR_OBJ(pp) =
  PRE
    pp:Rename_fstrtok &
    size(Rename_fstrstruct(pp))/=0
  THEN
    Rename_fstrstruct(pp):= front(Rename_fstrstruct(pp)) ||
    Rename_fstrmem:=Rename_fstrmem-1
  END;

  Rename_STO_FSTR_OBJ(pp,ii,vv) =
  PRE
    pp:Rename_fstrtok &
    vv:0..255 &
    ii:1..size(Rename_fstrstruct(pp))
  THEN 
    Rename_fstrstruct(pp)(ii):=vv
  END;

  bb <-- Rename_APP_FSTR_OBJ(pp,qq) =
  PRE
    pp:Rename_fstrtok &
    qq:Rename_fstrtok 
    /* Rename_fstrmem+size(Rename_fstrstruct(qq))<=maxmem */
  THEN
    IF
      Rename_fstrmem+size(Rename_fstrstruct(qq))<=maxmem
   THEN
      Rename_fstrstruct(pp):= ( 
       Rename_fstrstruct(pp)^Rename_fstrstruct(qq) 
      ) ||
      Rename_fstrmem:= (
       Rename_fstrmem+size(Rename_fstrstruct(qq)) 
      )||
      bb:=TRUE
    ELSE
      bb:=FALSE
    END
  END;

  bb <-- Rename_CPY_FSTR_OBJ(pp,qq) =
  PRE
    pp:Rename_fstrtok &
    qq:Rename_fstrtok 
    /* Rename_fstrmem- (
     size(Rename_fstrstruct(qq))+size(Rename_fstrstruct(pp)) 
     ) <=  maxmem */
   
  THEN
    IF Rename_fstrmem- ( 
        size(Rename_fstrstruct(qq))+size(Rename_fstrstruct(pp))
         ) <=  maxmem 
   THEN
      Rename_fstrstruct(qq):=Rename_fstrstruct(pp) ||
      Rename_fstrmem:= ( 
        Rename_fstrmem- (
           size(Rename_fstrstruct(qq))+size(Rename_fstrstruct(pp))
        )
      ) ||
      bb:=TRUE
    ELSE
      bb:=FALSE
    END
  END;


  bb <-- Rename_OVR_FSTR_OBJ(pp,qq) =
  PRE
    pp:Rename_fstrtok &
    qq:Rename_fstrtok 
    /* Rename_fstrmem + (
    size(Rename_fstrstruct(qq))-size(Rename_fstrstruct(pp))
    ) <= maxmem */
  THEN
    IF
      Rename_fstrmem+ (
        size(Rename_fstrstruct(qq))-size(Rename_fstrstruct(pp))
      ) <=  maxmem 
    THEN
      Rename_fstrstruct(pp):= (
        Rename_fstrstruct(pp) <+ Rename_fstrstruct(qq)
      ) ||
      Rename_fstrmem:= (
         Rename_fstrmem+ (
            max({0,(size(Rename_fstrstruct(qq))-size(Rename_fstrstruct(pp)))}) 
         )
      )||
      bb:=TRUE
    ELSE
      bb:=FALSE
    END
  END;

 /******************** Persistent Data facilities ***********************/

/***********  save/restore host byte order ***********/

  Rename_SAV_FSTR_OBJ =
  BEGIN
    skip
  END;

  Rename_RST_FSTR_OBJ =
  ANY
    sstrn,sstro,stotstr
  WHERE
    sstrn <: Rename_FSTROBJ &
    sstro: sstrn --> seq(0..255) &
    stotstr:  NAT 
  THEN
    Rename_fstrstruct := sstro ||
    Rename_fstrtok := sstrn ||
    Rename_fstrmem := stotstr
  END;

  Rename_SAVN_FSTR_OBJ =
  BEGIN
    skip
  END;

/***********  save/restore network byte order ***********/

  Rename_RSTN_FSTR_OBJ =
  ANY
    sstrn,sstro,stotstr
  WHERE
    sstrn <: Rename_FSTROBJ &
    sstro: sstrn --> seq(0..255) &
    stotstr:  NAT 
  THEN
    Rename_fstrstruct := sstro ||
    Rename_fstrtok := sstrn ||
    Rename_fstrmem := stotstr
  END;


/**************************** Browsing ********************************/

  nn,pp <-- Rename_FIRST_FSTR_OBJ =  
  IF not(Rename_fstrtok = {}) THEN
     pp :: Rename_fstrtok || 
     nn := card(Rename_fstrtok) 
  ELSE
     pp :: Rename_FSTROBJ ||
     nn := 0
  END;

  nn,qq <-- Rename_NEXT_FSTR_OBJ(mm,pp) = 
  PRE
    pp : Rename_fstrtok &
    mm : NAT1
  THEN
    nn := mm-1 ||
    qq :: Rename_fstrtok
  END



END

Analysed Constructs

On-line Help

---

Document Last Updated: Wed Aug 25 17:36:46 1999

B-Toolkit Beta 4.55

---