PortSpec: trait
  Ports enumeration of A, B
  introduces
    succ : Ports -> Ports
asserts
  succ(A) = B;
  succ(B) = A