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

// One way to write the most plausible answer.

//@ uses cpp_const_char_string;

char* strdup(const char *s) throw();
//@ behavior {
//@   requires nullTerminated(s, pre);
//@   ensures isValid(result)
//@           /\ fresh(contained_objects(result, post))
//@ 	  /\ (maxIndex(result) = lengthToNull(s,pre) + 1)
//@ 	  /\ (sameCharsThroughNull(result, post, s, pre));
//@ }

/*
 One can also replace all mentions of the state ``pre'' with ``any'',
 since the state ``pre'' is only used when refering to s, and s does not
 change.

 Another simple variation is to replace ``isValid(result)'' with
 ``nullTerminated(result)''.  This should be equivalent by the last conjunct
 in the ensures clause.

 Note that no modifies clause is needed, becuase nothing is changed.

 You may have wanted to say something about what happens when the call to
 new returns 0 (i.e., when an error occurs).  We choose to ignore that
 issue here, and leave it to you to work out in extra credit exercises.
*/