// @(#)$Id: PersonSet.lh,v 1.30 1997/07/31 02:43:26 leavens Exp $
#include "Person.lh"

//@ uses PersonSetTrait(PersonSet for Set[Obj[Person]]);

class PersonSet {
public:
  //@ invariant \A p: Obj[Person] ((p \in (self\any)) => assigned(p, any));

  PersonSet() throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = {};
  //@ }

  virtual ~PersonSet() throw();
  //@ behavior {
  //@   ensures true; // persons in self not deleted
  //@ }

  virtual void add(Person& e) throw();
  //@ behavior {
  //@   requires assigned(e, pre);
  //@   modifies self;
  //@   ensures self' = self^ \U {e};
  //@ }

  virtual void remove(Person& e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = delete(e, self^);
  //@ }

  virtual bool member(Person& e) const throw();
  //@ behavior {
  //@   ensures result = (e \in self^);
  //@ }

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

  virtual void bump_years() throw();
  //@ behavior {
  //@   requires \A p: Obj[Person] ((p \in (self\any)) => assigned(p, pre));
  //@   modifies contained_objects(self, any);
  //@   ensures \A p: Obj[Person]
  //@            ((p \in (self\any))
  //@             => (p'.age' = p^.age^ + 1 /\ p'.name' = p^.name^));
  //@   example \E p1: Obj[Person], p2: Obj[Person]
  //@             (assigned(p1, pre) /\ assigned(p2, pre)
  //@              /\ self^ = {p1} \U {p2} /\ p1^.age^ = 19 /\ p2^.age^ = 27
  //@              /\ self' = {p1} \U {p2} /\ p1'.age' = 20 /\ p2'.age' = 28
  //@              /\ p1'.name' = p1^.name^ /\ p1'.name' = p1^.name^);
  //@ }

  PersonSet& copy() const throw();
  //@ behavior {
  //@   requires \A p: Obj[Person] ((p \in (self\any)) => allocated(p, pre));
  //@   ensures fresh(result, contained_objects(result, post))
  //@           /\ assigned(result, post)
  //@           /\ result'' = self\any\any;
  //@   example \E p1: Obj[Person], p2: Obj[Person],
  //@                   p1new: Obj[Person], p2new: Obj[Person]
  //@             (assigned(p1, pre) /\ assigned(p2, pre)
  //@              /\ self\any = {p1} \U {p2}
  //@              /\ p1\any.age = 19 /\ p1\any.name = A"fred"
  //@              /\ p1\any.age = 27 /\ p1\any.name = A"sue"
  //@              /\ fresh(result, p1new, p2new)
  //@              /\ result' = {p1new} \U {p2new}
  //@              /\ p1new'.age = 19 /\ p1new'.name = A"fred"
  //@              /\ p1new'.age = 27 /\ p1new'.name = A"sue");
  //@ }

  PersonSet& copy1() const throw();
  //@ behavior { // one-level copy
  //@   ensures fresh(result) /\ assigned(result, post)
  //@           /\ result' = self\any;
  //@   example \E p1: Obj[Person], p2: Obj[Person]
  //@             (self\any = {p1} \U {p2}
  //@              /\ fresh(result) /\ result' = {p1} \U {p2});
  //@ }
};

[Index]

HTML generated using lcpp2html.