hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
198 stars 40 forks source link

Duplication checker: itself self-explanatory, text around it confusing #81

Open keithb-coop opened 6 months ago

keithb-coop commented 6 months ago

Description

The writing specifications page says this of the duplication checker:

  1. Create an empty set seen, then step through the elements of seq.

  2. Every time we see a number, we check if it's already in seen.

    • If it is, we say the list is not unique.
    • Otherwise, we add the element to seen and continue.
  3. If we reach the end and haven't seen any duplicate elements, we say the list is unique.

  4. Our decision should match the operator IsUnique(seq).

In this chapter we'll focus on just writing out the spec, parts (2) and (3). In the next chapter we'll do steps (1) and (4), actually verifying the algorithm.

But the example plainly does do steps 1, 2, 3. Does the segment

In this chapter we'll focus on just writing out the spec, parts (2) and (3). In the next chapter we'll do steps (1) and (4), actually verifying the algorithm.

perhaps refer to an earlier list of activities that the user is to do?

problem statement

Suggest that IsUnique(seq) is a misleading name, and that something like ContainsNoDuplicates(seq) expresses the intent better. Similarly, if we reach the end and haven’t seen any duplicate elements, we might better say the elements of the list is are unique.