[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.


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.