Re: [tlaplus] Pagination, get N elements from a set

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

your description makes the distinction between the (unsorted) data base and a variant where identifiers have been sorted. So it sounds like you have two sub-problems that you should specify: sorting the data base and then retrieving a batch of elements. For the second part, you should find it easy to extract a batch of given size from a *sequence* (rather than a *set*) of elements. I do not know whether you intend sorting to be part of the regular operation of the system or just an auxiliary function used in the specification of this particular problem.

Hope this helps,

Stephan

On 29 Aug 2018, at 23:32, jakub....@xxxxxxxxx wrote:

Hi,

I am modelling an existing piece of code. The code runs paginated SQL queries that I would like to model. In particular, I model the Database as a set of identifiers that satisfy

  Database \in SUBSET 1..N_IDENTIFIERS

Given page size PAGE_SIZE and page number P, I would like to retrieve elements from the Database that are in range between PAGE_SIZE*P and PAGE_SIZE*(P+1) of the sequence of sorted identifiers. For example, if Database is {1,2,5,6,7,10,11} , PAGE_SIZE=3, then the query for page P=0 should result in {1,2,5}, page P=1 gives {6,7,10} and P=2 gives {11}.

How to model such "query"?

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.