Software that doesn't terminate can be modeled with coinductive types, a typical example is a Stream.