// @(#)$Id: answer2.h,v 1.4 1997/06/03 23:06:54 leavens Exp $

//@ uses cpp_string;

char* strdup(const char *s) throw();
//@ behavior {
//@   requires nullTerminated(s, pre);
//@   ensures isValid(result)
//@           /\ (maxIndex(result) = lengthToNull(s,pre) + 1)
//@ 	  /\ (\forall i:int ((0 <= i /\ i <= maxIndex(result))
//@                             => fresh(*(result+i))))
//@ 	  /\ (sameCharsThroughNull(result, post, s, pre));
//@ }

/*
 The use of the trait cpp_string is okay, as it includes cpp_const_char_string.

 The ``\forall i:int ...'' in the third conjunct does the same thing as
	fresh(contained_objects(result, post))
 which was used in the first specification.
*/