// @(#)$Id: Person_defaults.lh,v 1.7 1999/03/03 19:11:51 leavens Exp $

#include "Person.lh"

//@ refine Person by
//@ class Person {
//@ public:     // implicit specifications added to class Person

  //@ spec Person(const Person& arg) throw();
  //@ behavior {
  //@   requires assigned(arg, any) /\ assigned(arg\any, any);
  //@   requires redundantly assigned(arg\any.name, any)
  //@                       /\ assigned(arg\any.age);
  //@   constructs self;
  //@   ensures self'' = arg\any\any;
  //@   ensures redundantly name' = arg\any.name\any
  //@                    /\ age' = arg\any.age\any;
  //@ }
  
  //@ spec Person& operator = (const Person& from) throw();
  //@ behavior {
  //@   requires assigned(from, any) /\ assigned(from\any, any);
  //@   requires redundantly assigned(from\any.name, any)
  //@                        /\ assigned(from\any.age);
  //@   modifies self;
  //@   ensures result = self /\ self'' = from\any\any;
  //@   ensures redundantly name' = arg\any.name\any
  //@                       /\ age' = arg\any.age\any;
  //@ }
//@ };

[Index]

HTML generated using lcpp2html.