A simple specification for the problem that you mention can be written as
TwoSum(S, tgt) ==
LET GoodSum(x,y) == x + y = tgt
IN { <<x, y>> \in S \X S : GoodSum(x,y) }
This operator will return all pairs of values in S whose sum equals tgt. (Note that it doesn't make sense to talk of an index of a number in a set, since sets are by definition unordered. Also, you may want to exclude symmetric solutions by requiring x <= y as part of the definition GoodSum. It is an easy exercise to adapt the definition to the case where S is a sequence of numbers and the result is the set of pairs of indexes.)
I presume that you would probably not consider the definition above to be an "algorithm" because it doesn't tell you how to compute the result effectively, let alone efficiently. You can use TLA+ to specify an algorithm that computes the set step by step, then assert that when the algorithm terminates given as input a set of integers S and an integer value tgt, its result agrees with TwoSum(S, tgt).
Stephan
I'm trying to learn TLA+ to solve Leetcode problems?
Is TLA+ for writing algorithms or just specifying algorithms. In other words, do i learn the algorithm first, or can I use TLA+ to create an algorithm?
For example, for the classic 2 sums problem:
Given a set of integers. and a target value. Find the index of every pair of numbers that sum to the target value. Note: the index cannot be the same in the pair.
Thanks so much for the help!
--
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/b167372b-d453-404c-a0c7-e4a2766c6a27n%40googlegroups.com.