[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: 7532yahoo@xxxxxxxxx*Date*: Fri, 8 Mar 2019 16:05:53 -0800 (PST)*References*: <359667f7-f2d8-490f-b3ec-1eb7dffeed5f@googlegroups.com>

On Saturday, July 14, 2018 at 6:46:12 AM UTC-4, fl wrote: > I was working on Knuth's fascicle on backtracking: > > > https://www-cs-faculty.stanford.edu/~knuth/fasc5b.ps.gz > > > > and I was using PLUSCAL to get a version of the algorithm B on which I could do some > experiments, > > > and looking at the exercise 5 that proposes to make the recursive version of the > algorithm, it came to my mind that I was once advised not to use the procedure > facilitiy of PLUSCAL. (see p. 26) > > > https://lamport.azurewebsites.net/tla/c-manual.pdf > > > > but to use the TLAPLUS mathematical constructs instead (sets, mathematical functions etc.) > > > It was a very good piece of advice. It amounts to replacing a procedure by its postcondition. > Mathematically speaking, there is nothing wrong with this way of doing. And practically > speaking this prevents the burden of stacks and labels generated by procedures. (It leads > to program that are less simple to prove.) > > > So the rule is: don't use procedures, work through each algorithm in isolation. > > > However there is one case where procedures are required: recursive algorithms. > I think it is the only legitimate case. > > > And since there is always one way to turn a recursive algorithm into a non-recursive > with old good loops and so on, this legitimate case is of little use. > > > But to work on Knuth's exercise 5, use procedures. > > > -- > FL The quote the OP refers to from pg26 is: "For example, if x is a local variable of procedure P, then a step within the body of P that (recursively) calls P cannot also assign a value to x." For example, in this C snippet if the value of i was 10 at the recursive call, foo would be run with i=11 with i=10 still on return. void foo(int i) { . . . foo(i+1); // recursive call . . . } However, in an equivalent PLUSCAL procedure, i would equal 11. Learned this the hard way ... -- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.

**References**:**Procedure in PlusCal***From:*fl

- Prev by Date:
**[tlaplus] Re: Seeking advice about principles of translating TLA+ spec to real code** - Next by Date:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Previous by thread:
**Procedure in PlusCal** - Next by thread:
**Understanding why specification hits deadlock upon initialization** - Index(es):