| 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
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/0926889F-DAF2-45F1-AEF6-A42B04734B24%40gmail.com. |