// @(#)$Id: charPointer.lh,v 1.17 1997/06/03 21:37:27 leavens Exp $

// Interface specification of for the C++ type pointer to char.
// You can get the specification for a similar C++ type by changing "char"
// in what follows to the appropriate C++ type for the elements.

// The preconditions below don't attempt to capture everything
// about legal C++ pointer arithmetic; use a class to be safer.

// The following uses clause is implicit in Larch/C++.
// You don't have to write it; it's included as an example of the Larch/C++
// implicit use of traits for C++ built-in types.
/*
   uses char, MutableObj(char), Pointer(Obj, char), int;
*/


// ********************************************************
// dereference operator *, address-of operator &
// ********************************************************

// note that the following returns a char object (by reference)
char& operator * (char * p);
//@ behavior {
//@   requires isValid(p);
//@   ensures liberally returns => result = *p;
//@ }

char * operator & (char& c);
//@ behavior {
  // the following says that if c is already in an array, we use that array,
  // otherwise model it with a 1 element array for the pointer.
//@   ensures returns =>
//@      (if (\E a:Arr[Obj[char]], i: int
//@                  (legalIndex(a, i) /\ a[i] = c /\ allocated(a[i], pre)))
//@       then (\E a:Arr[Obj[char]], i: int
//@                   (legalIndex(a, i) /\ a[i] = c /\ allocated(a[i], pre)
//@                    /\ result = [i,a]))
//@ 	  else (result = [0, assign(create(1),0,c)]));
//@ }

// ********************************************************
// arithmetic operations: +, -
// ********************************************************

char * operator + (char * p, int i);
//@ behavior {
//@   requires notNull(p);
//@   ensures returns => result = p + i;
//@ }

char * operator - (char * p, int i);
//@ behavior {
//@   requires notNull(p);
//@   ensures returns => result = p - i;
//@ }


// ********************************************************
// increment/decrement operators: ++ and --
// ********************************************************

// prefix ++, returns a char* object, by reference
char *& operator ++ (char *& p);
//@ behavior {
//@   requires assigned(p, pre);
//@   modifies p;
//@   ensures returns => result = p /\ (p' = p^ + 1);
//@ }

// postfix ++
char * operator ++ (char *& p, int);
//@ behavior {
//@   requires assigned(p, pre);
//@   modifies p;
//@   ensures returns => result' = p^ /\ (p' = p^ + 1);
//@ }

// prefix --, returns a char * object, by reference
char *& operator -- (char *& p);
//@ behavior {
//@   requires assigned(p, pre);
//@   modifies p;
//@   ensures returns => result = p /\ (p' = p^ - 1);
//@ }

// postfix --
char * operator -- (char *& p, int);
//@ behavior {
//@   requires assigned(p, pre);
//@   modifies p;
//@   ensures returns => result' = p^ /\ (p' = p^ - 1);
//@ }

// ********************************************************
// equality operators: == and  !=
// ********************************************************

bool operator == (char * p1, char * p2);
//@ behavior {
//@     ensures returns => (p1 = p2);
//@ }

bool operator != (char * p1, char * p2);
//@ behavior {
//@     ensures returns => (p1 ~= p2);
//@ }


// ********************************************************
// relational operators: <, >, <=, and >= 
// ********************************************************

bool operator < (char * p1, char * p2);
//@ behavior {
//@     requires (isNull(p1) /\ isNull(p2)) \/ locs(p1) = locs(p2);
//@     ensures returns => result = (p1 < p2);
//@ }

bool operator > (char * p1, char * p2);
//@ behavior {
//@     requires (isNull(p1) /\ isNull(p2)) \/ locs(p1) = locs(p2);
//@     ensures returns => result = (p1 > p2);
//@ }

bool operator <= (char * p1, char * p2);
//@ behavior {
//@     requires (isNull(p1) /\ isNull(p2)) \/ locs(p1) = locs(p2);
//@     ensures returns => result = (p1 <= p2);
//@ }

bool operator >= (char * p1, char * p2);
//@ behavior {
//@     requires (isNull(p1) /\ isNull(p2)) \/ locs(p1) = locs(p2);
//@     ensures returns => result = (p1 >= p2);
//@ }


// ********************************************************
// assignment operators: =, +=, -=
// ********************************************************
char * operator = (char *& p1, char *p2);
//@ behavior {
//@     modifies p1;
//@     ensures returns => (assigned(p1, post) /\ result = p1' /\ p1' = p2^);
//@ }    

char * operator += (char *& p, int i);
//@ behavior {
//@     requires assigned(p, pre);
//@     modifies p;
//@     ensures  returns => result = p' /\ p' = p^ + i;
//@ }

char * operator -= (char *& p, int i);
//@ behavior {
//@     requires assigned(p, pre);
//@     modifies p;
//@     ensures  returns => result = p' /\ p' = p^ - i;
//@ }

[Index]

HTML generated using lcpp2html.