Document Last Updated: Wed Aug 25 17:35:45 1999
B-Toolkit Beta 4.55
MACHINE Rename_Client(TOK,inbufsize,outbufsize)
SEES String_TYPE, Bool_TYPE
VARIABLES in,inptr,outptr
INVARIANT
in : 0..inbufsize &
inptr : 0..in &
outptr : 0..outbufsize
INITIALISATION in,inptr,outptr := 0,0,0
OPERATIONS
/*** operation to initialise ipaddress,port and reset pointers ***/
Rename_INIT(ipaddress : STRING & port : NAT) =
BEGIN in,inptr,outptr := 0,0,0 END;
/*** operations on the socket ***/
rep <-- Rename_CONNECT = BEGIN rep :: BOOL END;
rep <-- Rename_WRITE =
CHOICE
rep := TRUE || outptr := 0
OR
rep := FALSE
END;
rep,pp <-- Rename_READ =
ANY bufsize WHERE bufsize : 0..inbufsize THEN
CHOICE
rep := TRUE || pp := bufsize || in := bufsize || inptr := 0
OR
rep := FALSE || pp := 0
END
END;
rep <-- Rename_CLOSE = BEGIN rep :: BOOL END;
/*** operations to read from the input buffer ***/
tok <-- Rename_GET_TOK(toksize : 1..4 ) =
IF inptr+toksize <= in THEN
tok :: TOK || inptr := inptr + toksize
ELSE
tok :: TOK
END;
ss <-- Rename_GET_STR =
IF inptr + 3 <= in THEN
ANY str, newptr WHERE
str : STRING & newptr = inptr + size(str) + 3
THEN
ss := str || inptr := newptr
END
ELSE
ss :: STRING
END;
rep <-- Rename_GET_FIL(filename : STRING) =
CHOICE
ANY newptr WHERE newptr : 0..in & newptr > inptr THEN
inptr := newptr ||
rep := TRUE
END
OR
rep := FALSE
END;
/*** operations to to write the output buffer ***/
Rename_PUT_TOK(tok : TOK & toksize : 1..4 ) =
IF outptr+toksize <= outbufsize THEN
outptr := outptr+toksize
END;
Rename_PUT_STR(ss:STRING) =
IF outptr+size(ss)+3 <= outbufsize THEN
outptr := outptr+size(ss)+3
END;
/*** operations to get and set the input buffer pointer ***/
Rename_SET_IN_PTR(ptr : NAT) = PRE ptr <= inptr THEN inptr := ptr END;
ptr <-- Rename_GET_IN_PTR = BEGIN ptr := inptr END;
/*** operations to get and set the output buffer pointer ***/
Rename_SET_OUT_PTR(ptr : NAT) = PRE ptr <= outptr THEN outptr := ptr END;
ptr <-- Rename_GET_OUT_PTR = BEGIN ptr := outptr END
END