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

Re: [tlaplus] Sets and arrays



Hello,

I'd like to just add that sets are very natural in describing algorithms :-)
(but not low-level data structures).  For example, consider graph reachability:

 -- given a set e of edges and a set s of vertices, compute
 -- set r of vertices reachable from vertices in s following edges in e:

    r := s
    while exists v in {v: (u,v) in e, u in r, v not in r}:
      r := r + {v}

 -- same algorithm at a low level,
 -- so it is linear/optimal time by doing each set operation in O(1) time:

    w := s
    r := {}
    while exists x in w:
      for y in e{x}:
        if y not in r and y not in w:
          w := w + {y}
      w := w - {x}
      r := r + {x}

where e{x} is the image of x under map e (as in SETL:-), where a map is 
just a set of pairs), i.e., the set of elements that e maps x to.

Annie

On Fri, Apr 17, 2015 at 10:11 AM, fl <freder...@xxxxxxxxxxx> wrote:
 
I've changed my procedures by their specifications. I just want to report this trouble: when I think about specifications,
I naturally think in terms of sets, when I think about algorithms, I naturallly think in terms of arrays
(and then in terms of finite sequences) and then when I'm juggling with specification on one hand and algorithms
on the other one, I need to transform the formers into the latters.
 
In fact sets are not natural in algorithmics.
 
--
FL