MACHINE Population (HUMAN) VARIABLES people, age INVARIANT people <: HUMAN & age : people --> NATURAL /* * Exercise : add gender information. */ INITIALISATION people := {} || age := {} OPERATIONS birth (pp) = PRE pp : HUMAN - people THEN people := people \/ {pp} || age := age \/ {pp |-> 0} END ; death (pp) = PRE pp : people THEN people := people - {pp} || age := {pp} <<| age END ; aa <-- get_age (pp) = PRE pp : people THEN aa := age(pp) END ; elapse = ANY new_age WHERE new_age : people --> NATURAL & !pp . (pp : people => (new_age(pp) = age(pp) + 1)) THEN age := new_age END END