Larch/C++ Reference Manual - A First Class Design (Person)

Go to the first, previous, next, last section, table of contents.

7.1.1 A First Class Design (Person)

The first major hurdle you face as a user of Larch/C++ is how to specify the abstract values of a class.

Consider the specification of a class Person. The first question to ask is: what kind of information should be kept about a Person? To keep things simple, suppose you want to keep track of a person's name and age.

As in programming, the usual thing is to introduce some data members to record this decision. However, since we don't want to require that these particular data members appear in every implementation, we make them "specification" or "ghost" variables. That is we prefix their declarations with the Larch/C++ keyword spec, and put them in annotation comments. This means that these declarations need not appear in an implementation. (See section 9.1 Ghost Variables for more details on spec-decls.) For example, we would write the following as the declaration of a data member that tracks a person's age.

  // spec int age;

To track a person's name, we want some kind of string. If we had a C++ template class defined already for strings, such as String<char>, then we could declare the name as follows.

  // spec String<char> age;

However, suppose we don't already have such a class defined, what can we do? Well, one could go off and specify such a class and all its details in Larch/C++, but that would be overkill, since we don't need to use the class itself, as name is just a specification variable, not something we are (necessarily) manipulating in a C++ program. To avoid all that effort, we just use another spec-decl to declare the template class String, as in the following file.

// @(#)$Id: AbstractString.lh,v 1.1 1997/07/28 21:02:51 leavens Exp $
//@ spec template<class C> class String;
//@ uses AbstractStringTrait;  // defines the sort String[char]
//@ uses NoContainedObjects(String<char>);

The used trait AbstractStringTrait (see section 4.13.5 Abstract String Constants) associates a sort with the name String<char>. (Larch/C++ uses this trait by default in any case, but this makes it clearer.) Since we are associating the abstract values explicitly with the type String<char>, it is necessary to state whether the abstract values have any contained objects, hence the use of the trait NoContainedObjects(String<char>) (see section 7.5 Contained Objects).

Instead of using such abstract strings, you might think to use a C++ pointer to an array of null terminated characters. But this would be a mistake for such a simple specification, as it would make the abstract values much more complicated than they need to be. All that is needed are the characters in the name, details such as that they are contained in an array etc. are irrelevant. See section 5.4.4 Structure and Class Declarations for the comparable, but more complicated, abstract values of the type Entry.)

Note that the abstract values of C++ integers are specified in the Larch/C++ trait int (see section 11.1.5 int Trait for details). The association between the type int and the abstract values in that trait is made, again, by having a sort with the same name int, defined in the trait int.

At this point it is a good idea to think about invariant properties you want to hold for the values in the specification variables. For example, you might want ages to always be positive. There are two ways to handle this. One is to change the type of the specification variable age to some type (like unsigned int) that has only positive integer values. However, if you want to use the type int in the interface to communicate with clients, that may cause difficulty. The second way is to use a Larch/C++ invariant-clause when you get to the point of writing the interface specification. An invariant allows you to state that you will only be using a subset of the potential abstract values.

Once you have decided how to model the information in instances of the type Person, you can proceed to designing and specifying the C++ interface.

For the design, typically you will want some or all of the following kinds of member functions.

Constructors, which have the same name as the name of the class. For the class Person, we will use one constructor named Person. You may have one or more constructors with different types of arguments. The job of a constructor is to initialize an object once C++ has allocated space for it.
A destructor, which has the name of the class prefixed by ~. For the class Person, the destructor would be named ~Person. The job of a destructor is normally to deallocate any dynamically allocated contained objects. Since there are no contained objects in a Person instance, the destructor should do nothing. (This is fine, because it is the C++ operator delete that actually deallocates storage for a Person instance, not the destructor.)
Mutators, which are member functions that change the abstract value of specification variables (or the default argument, *this). For the class Person, we might want something to change a person's name, and to add a year to their age (on their birthday). We call these Change_Name and Make_Year_Older.
Observers, which are member functions that do not change the abstract value of the default argument, but instead return some information about it. For the class Person, we might want a member function to return the person's name and their age. We call these Name and Years_Old.

It is also possible to have a combination mutator and observer, but it is simpler to keep them separate.

Once you have designed the member functions, you can specify their interfaces and behavior in more detail. Things to decide include the following:

What the parameter types are for constructors, mutators, and observers, and what the result type is for each mutator and observer.
Whether some of the member functions are to be virtual, so that they will work with subtyping. Unless you have some efficiency reasons not to make them virtual, it seems best to make all but the constructor virtual, as this gives greater flexibility. (The constructors, of course, cannot be virtual.) Other C++ interface details, such as the use of const, can also be decided here.
What, informally, you want each member function to do. These informal statements can be written as comments in the Larch/C++ formal specification.

Then you should be ready to write a formal specification, such as the following (which is discussed further below).

// @(#)$Id: Person.lh,v 1.26 1998/08/27 22:42:08 leavens Exp $

#include "AbstractString.lh"

//@ uses cpp_string; 

class Person {
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

  Person(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 ~Person() 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;
  //@ }
};

In the specification of the class Person above, the included file, `AbstractString.lh', is the one shown above that specifies the type String<char>. The trait used, cpp_string, defines trait functions, such as nullTerminated and lengthToNull that are useful in dealing with C++ character strings. (See section 11.9 Character Strings for details.)

The invariant specified for the class Person says that a person always has a name that has one or more characters in it, and that the person's age is at least 0 (years). See section 7.3 Class Invariants for more details on invariants.

The constraint specified for the class Person says that a person's age may only increase over time. See section 7.4 History Constraints for more details on such history constraints.

The constructor takes a null-terminated C++ string and an integer and uses them to initialize the specification variables name and age.

Since age and name are data members, they have sorts, Obj[int] and Obj[String[char]], respectively. Hence, to refer to their abstract values in the post-state, one must write name' and age'. (See section 2.8 Objects and Values for an introductory discussion about objects and values. See section 6.2.1 State Functions for details on state functions such as '.) Notice that the constructor's precondition is needed to have a sensible C++ character string, and to establish the invariant in the post-state.

The destructor's specification is standard; it says that the destructor does nothing.

See section 6.9.3 Redundant Ensures Clauses or Claims for details on using a redundant ensures-clause such as the one in change_name.

See section 6.9.1 Examples in Function Specifications for details on using an example such as the one in make_year_older.

It may be of some interest to see the LSL trait that Larch/C++ automatically (in theory) constructs for this specification. The following trait, Person_Trait assumes and then includes some traits relating to the types mentioned in the declaration of Person; then in the last set of includes, it generates the theory of values of Person objects, and then the theory of const Person objects.

% @(#) $Id: Person_Trait.lsl,v 1.5 1997/07/31 21:11:28 leavens Exp $

% This trait would be automatically constructed by Larch/C++

Person_Trait: trait
  assumes AbstractStringTrait, int, cpp_member_function
  includes MutableObj(int), MutableObj(String[char]),
           ConstObj(int), ConstObj(String[char]),
           ConstObj(cpp_member_function)
  includes Person_Pre_Trait(Person, Obj, Val[Person]),
           Person_Pre_Trait(Const[Person], ConstObj, Val[Person])

The trait Person_Pre_Trait that defines the theory of Person and Const[Person] with the various renamings is as follows. Note that the tuples defined for these sorts include all the (non-static) members of the class Person, including the member functions. See section 11.10 Structure and Class Types for details and a similar example.

% @(#) $Id: Person_Pre_Trait.lsl,v 1.1 1997/07/31 17:25:51 leavens Exp $

% This trait would be automatically constructed by Larch/C++

Person_Pre_Trait(Person, Loc, Val): trait

  assumes AbstractStringTrait, int, cpp_member_function,
          TypedObj(Loc, String[char]), TypedObj(Loc, int),
          ConstObj(cpp_member_function),
          contained_objects(Loc[String[char]]), contained_objects(Loc[int])

  includes NoContainedObjects(Val), contained_objects(Person)

  Person tuple of age: Loc[int], name: Loc[String[char]],
                  destructor: ConstObj[cpp_member_function],
                  Change_Name: ConstObj[cpp_member_function],
                  Name: ConstObj[cpp_member_function],
                  Make_Year_Older: ConstObj[cpp_member_function],
                  Years_Old: ConstObj[cpp_member_function]

  Val tuple of age: int, name: String[char], 
                  destructor: cpp_member_function,
                  Change_Name: cpp_member_function,
                  Name: cpp_member_function,
                  Make_Year_Older: cpp_member_function,
                  Years_Old: cpp_member_function

  introduces
    eval: Person, State -> Val
    allocated, assigned: Person, State -> Bool

  asserts
    \forall per: Person, oi: Loc[int], os: Loc[String[char]], 
            odestroy, och_nm, onm, omyo, oyo: ConstObj[cpp_member_function],
            st: State

       contained_objects([oi,os,odestroy,och_nm,onm,omyo,oyo], st)
         == {asTypeTaggedObject(oi)} \U {asTypeTaggedObject(os)}
            \U {asTypeTaggedObject(odestroy)} \U {asTypeTaggedObject(och_nm)}
            \U {asTypeTaggedObject(onm)} \U {asTypeTaggedObject(omyo)}
            \U {asTypeTaggedObject(oyo)};

       eval(per,st)
         == [eval(per.age, st), eval(per.name, st),
             eval(per.destructor, st),  eval(per.Change_Name, st),
             eval(per.Name, st), eval(per.Make_Year_Older, st),
             eval(per.Years_Old, st)];

       allocated(per,st)
         == allocated(per.age, st) /\ allocated(per.name, st)
          /\ allocated(per.destructor, st) /\ allocated(per.Change_Name, st)
          /\ allocated(per.Name, st) /\ allocated(per.Make_Year_Older, st)
          /\ allocated(per.Years_Old, st);

       assigned(per,st)
         == assigned(per.age, st) /\ assigned(per.name, st)
          /\ assigned(per.destructor, st) /\ assigned(per.Change_Name, st)
          /\ assigned(per.Name, st) /\ assigned(per.Make_Year_Older, st)
          /\ assigned(per.Years_Old, st);

  implies
    converts
      contained_objects: Person, State -> Set[TypeTaggedObject],
      eval: Person, State -> Val,
      allocated: Person, State -> Bool, assigned: Person, State -> Bool

Go to the first, previous, next, last section, table of contents.