Re: Sets and arrays

Hello Frederic,

I agree that it is natural to describe algorithms at a high level using sets: that's exactly why they are so prominent in TLA+. In your message, I suppose that when you say "algorithms" you are thinking of a description close to a programming language, i.e. an implementation. Both levels have their role: probably you want to prove properties at the abstract level, and the lower level allows you to relate the TLA+ description to a program. If you want to relate the two levels formally, you need a refinement mapping that computes the abstract, set-based representation from the low-level, array-based one. Did you have a look at section 8 of the Hyperbook that introduces this concept and shows how you can use TLC to check refinement (in that case, of a sequence by an array)?

Regards,

Stephan

On Friday, April 17, 2015 at 4:11:53 PM UTC+2, fl 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