[tlaplus] Re: Procedure in PlusCal

[7532yahoo@xxxxxxxxx]

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.