Procedure in PlusCal

[fl]

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

[7532...@gmail.com]

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 ...