Other aspects of B
B Method for the specification and fabrication of software and proven critical systems

Regardless of the level of abstraction chosen, to write a formal model, a general process must be applied, including the choice of the mathematical entities best suited to represent what we want to represent, and the statement of the static or dynamic laws that will govern the desired or observed behavior of the system. The more abstract the level, the more delicate the choice of mathematical entities. A formal specification should not, in principle, formalize treatments, but rather properties, if it is to be of significant interest in avoiding high-level errors.