// @(#)$Id: IntVar.lh,v 1.14 1997/07/31 03:10:16 leavens Exp $

#include "AbstractString.lh"

//@ uses cpp_const_char_string;

class IntVar {
public:
  int var;
  //@ spec String<char> its_name;
  //@ constraint its_name^ = its_name';  // the name can't be changed

  IntVar(const char vname[] = "unnamed", int initial_value = 0) throw();
  //@ behavior {
  //@   requires nullTerminated(vname, any);
  //@   constructs var, its_name;
  //@   ensures its_name' = throughNull(vname, any)
  //@        /\ var' = initial_value;
  //@ }

  const char * name() const throw();
  //@ behavior {
  //@   ensures nullTerminated(result, post)
  //@           /\ throughNull(result, post) = its_name\any;
  //@ }
};

[Index]

HTML generated using lcpp2html.