The geometry of distributions in formal methods

The act of distributing and the resulting distribution are notions which lie at the kernel of any distributed system. The basic algebra of such distributions and their use in formal specifications has already been developed in terms of indexed monoids (i.e., function spaces with valuations in monoids) and their morphisms. Complementary to such algebra is a body of emerging geometry/topology of formal specifications, one critical aspect of which is the fibre bundle, and more generally the sheaf. Fibre bundles are used to model the nature and shape of geometrical objects and to associate a field with points in a space. They find particular application in theoretical physics, for example. We demonstrate here that fibre bundles occur naturally in specifications and models associated with formal methods.