// @(#)$Id: Person2.lh,v 1.14 1998/08/27 22:42:09 leavens Exp $

#include "AbstractString.lh"

//@ uses cpp_string;

class Person2 {
public:
  //@ spec int age;             // age interpreted as number of years old
  //@ spec String<char> name;

  //@ invariant len(name\any) > 0 /\ age\any >= 0;

  //@ constraint age^ <= age';  // age can only increase
  //@ constraint name^ = name' /\ age^ = age'
  //@    for virtual char * name() const,
  //@        virtual int years_old() const;
  //@ constraint age' = age^
  //@    for virtual void change_name(const char *);
  //@ constraint name' = name^
  //@    for virtual void make_year_older();

  Person2(const char *moniker, int years) throw();
  //@ behavior {
  //@   requires nullTerminated(moniker,pre) /\ lengthToNull(moniker,pre) > 0
  //@            /\ years >= 0;
  //@   modifies name, age;
  //@   ensures name' = uptoNull(moniker,pre) /\ age' = years;
  //@ }

  virtual ~Person2() throw();
  //@ behavior {
  //@   ensures true;
  //@ }

  virtual void Change_Name(const char *moniker) throw();
  //@ behavior {
  //@   requires nullTerminated(moniker,pre) /\ lengthToNull(moniker,pre) > 0;
  //@   modifies name;
  //@   ensures name' = uptoNull(moniker,pre);
  //@   ensures redundantly len(name') > 0;
  //@ }

  virtual char * Name() const throw();
  //@ behavior {
  //@   ensures nullTerminated(result,post)
  //@           /\ fresh(objectsToNull(result,post))
  //@           /\ uptoNull(result,post) = name\any;
  //@ }

  virtual void Make_Year_Older() throw();
  //@ behavior {
  //@   requires age^ < INT_MAX;
  //@   modifies age;
  //@   ensures age' = age^ + 1;
  //@   example age^ = 29 /\ age' = 30;
  //@ }

  virtual int Years_Old() const throw();
  //@ behavior {
  //@   ensures result = age\any;
  //@ }
};

[Index]

HTML generated using lcpp2html.