Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte
"Model-Based Software Testing and Analysis with C#"
EmptySet;
static Map
salary = Map.EmptyMap;
static Set NextEmployee()
{
return new Set(new Employee(nextId));
}
[Action]
static void CreateEmployee([Domain("NextEmployee")] Employee emp)
{
nextId = nextId + 1;
allEmployees = allEmployees.Add(emp);
salary = salary.Add(emp, 0); // default salary
}
[Action]
static void DeleteEmployee([Domain("allEmployees")] Employee emp)
{
allEmployees = allEmployees.Remove(emp);
salary = salary.RemoveKey(emp);
}
[Action]
static void SetSalary([Domain("allEmployees")] Employee emp, int x)
{
salary = salary.Override(emp, x);
}
}
}
Advanced Topics 251
This example shows the basics of maintaining a field map. There is an action
CreateEmployee that instantiates new objects. The action DeleteEmployee removes
a previously created employee from the state. The SetSalary action changes the
salary of a given employee (Override is a method on Map).
Trace 1 Trace 2
CreateEmployee(Employee(1)) CreateEmployee(Employee(1))
SetSalary(Employee(1), 200) CreateEmployee(Employee(2))
CreateEmployee(Employee(2)) DeleteEmployee(Employee(1))
SetSalary(Employee(2), 400) SetSalary(Employee(2), 400)
DeleteEmployee(Employee(1))
Trace 1 and Trace 2 produce the same end state. In this state the values of the
state variables are
nextId = 3
allEmployees = Set(Employee(2))
salary = Map(Employee(2), 400)
This example shows that you can model instances using only the features introduced
in the previous chapters.
Pages:
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333