After reading the introductory paper:
"UML-B and Event-B: an integration of languages and tools"
I understand that the UML-B "package diagram" is actually an overview of
the whole project.
My initial question was actually about the existence of a correspondent of
a Package language element.
My guess is that it is not existing at the moment.
Is that correct ?
Would it make sense to introduce such a concept in a future version of
I also couldn't find a namespace concept in Event-B (that is, for
structuring concepts inside one Machine).
Is that because models requiring that kind of feature would be already
impractical to specify and prove with Event-B ?