[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: [tlaplus] TLA+, Event B comparison

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/30ac153e-9b49-411c-bacf-c76d1b8b4050%40googlegroups.com.