A minor correction to Michael's post.--in particular, to this statement
Functions in TLA+ are total, while B supports relations, partial functions, injections, bijections, etc.
I believe a partial function is usually said to be a function that is not necessarily defined on all
elements of its domain. In math, the domain of a function is by definition the set of elements on
which it's defined, so "partial function" is meaningless. In typed languages, a function is defined
to have a domain type, and a partial function is one that is not necessarily defined on all elements
of that type. Since TLA+ is untyped, it adopts the mathematical definition of a function and has
no need for anything like a partial functions.
Mathematically, a relation on a pair S, T of sets is a subset of S X T. By "supporting" relations,
injections, etc., Michael means that B provides a large collection of arrow symbols that express certain
sets (more precisely, types) of relations on pairs of sets. For example S -some-kind-of-arrow-> T
might define the set of all relations R on S, T such that (s1,t) and (s2,t) in R implies s1=s2.
Abrial liked those operators and apparently used them frequently when writing specs.
Operators corresponding to all those arrow symbols are easily defined in TLA+. I occasionally
wrote specs that needed to define a set of relations on some pair of sets, and writing that set of
relations as S -some-kind-of-arrow-> T would have been nice. However, they were not always
the sets of relations defined by the B arrows. I thought about providing a few user-defined
arrow symbols for the purpose in TLA+, but I decided they weren't useful enough. Apparently Abrial
and I wrote different kind of specs. Most of my specs were for concurrent systems; he designed
B for specifying sequential programs. Or perhaps we just had different tastes. I think he
found the use of all those arrows elegant, while I found it confusing.
Leslie