// @(#)$Id: exercise.txt,v 1.4 1997/06/03 23:06:55 leavens Exp $

Larch/C++ provides several traits that help you specify functions that
use C++ with character strings.  See the following traits
in the Larch/C++ trait library (which if you're reading this in a Unix
file under the Larch/C++ release, are in the directory ../../lib and have
file names ending in ``.lsl'').
	cpp_char_string
	cpp_const_char_string

As an example of using these traits, consider the following specification.

	//@ uses cpp_const_char_string;

	int strlen(const char *s) throw();
	//@ behavior {
	//@   requires nullTerminated(s, pre);
        //@   ensures result = lengthToNull(s, pre);
        //@ }

The uses clause says that the trait cpp_const_char_string is to be
used to give meaning to the trait functions used in the specification.
(This trait includes the trait cpp_char_string.)
The trait function nullTerminated is passed the pointer, s, and a state, pre.
(The state named ``any'' could have also been used.)
The trait function nullTerminated checks that the pointer is valid
and that in the pre-state it points to objects that eventually contain
a null character.  Similarly, ``lengthToNull(s, pre)'' is the (abstract) int
that is the number of characters up to, but not includng,
the null character in the characters pointed to by s in the pre-state.

For another example, see the specification of the string copy function "strcpy"
in the Larch/C++ reference manual.

For this exercise you are to specify the C++ function strdup, which
takes a string, s, and returns a new copy of it.  Assuming that "strcpy"
and "strlen" work as specified, and that the C++ "new" operator works,
what you are to specify is the C++ function given by the following code.

	char* strdup(const char *s) throw()
        {
	  return *t = new char[strlen(s)+1];
          strcpy(t,s);
          return (t);  
        }