The
NModel framework supports instance fields with a special class that implements
field maps in the background. This class is called LabeledInstance
. You must
use this class (or a subclass) to program with objects in NModel. Here is an
example:
namespace Payroll2
{
class Employee : LabeledInstance
{
int salary;
Advanced Topics 249
public override void Initialize() { this.salary = 0; }
// ...
}
}
Model program Payroll1 and Payroll2 behave similarly. In the case of objectoriented
Payroll2, the NModel framework will create the field map for salary
automatically. The field map will record the associated value of each reachable
instance of class Employee. An object is reachable if it occurs within a global state
variable, or if it occurs within an instance field of a reachable object. Reachability
will be discussed in more detail in Section 15.2.
When inherited by type T the LabeledInstance class provides the following
features:
??? An implicit field map for instance fields of T, as explained above.
??? A serialized term label for each instance of T. For example, the first instance of
class Employee may appear as the term Employee(1) inside of an action argument.
The role of the term label in composition is discussed in Section 15.3. The role
of the term label in test harnessing is discussed in Section 15.4.
??? A parameter generator for type T named new.
Pages:
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331