# [tlaplus] Re: Procedure in PlusCal

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