object PersonList
    components: Person*;
    description: (*
        A PersonList contains zero or more Person records.
    *);
end PersonList;

object Person
    components: first:Name and last:Name and age:Age;
    description: (*
        A Person has a first name, last name, and age.
    *);
end Person;

object Name = string;
object Age = integer;

operation Add
    inputs: p:Person, pl:PersonList;
    outputs: pl':PersonList;
    precondition: not (p in pl);
    postcondition: p in pl';
    description: (*
        Add a person to a list, if that person is not already in the list.
    *);
end Add;