End labels

[fl]

I think we can't write like that something in PCAL:

 

begin algorithm ....

   ....

 

iflbl:

if FEOF(x) = EOF

then

  ret := 0;

  goto endlbl;

end if

endiflbl:

ret := 1

endlbl: <---- Here is the problem

 

end algorithm

 

 

 

Obviously we can replace "endlbl:" by "endlbl: ret := ret" or another innocent step but it is less good.

 

(I know that in this case I might use an "else" but the point is the possibility to have a label with no

expression behind to jump to the end of an algorithm when we want to modelize a multi return

routine.)

 

--

FL

[Stephan Merz]

In Pluscal, labels are attached to (sequences of) statements: they identify units of atomic execution. The fact that they can also serve as targets of goto statements is rather secondary. Typically, code snippets like the one that you show will appear in a procedure, and you can use a return statement to terminate a procedure prematurely.

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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[fl]

> In Pluscal, labels are attached to (sequences of) statements: they identify units of atomic execution. The fact that they

> can also serve as targets of goto statements is rather secondary. Typically, code snippets like the one that you show will > appear in a procedure, and you can use a return statement to terminate a procedure prematurely.

 

Sure but I don't like using PluCal procedure because you need to manage the stack in your proof then and it is

boring.  I have just come across the Skip expression. I will try if we can use it for the discussed purpose.

 

--

FL

[fl]

> Sure but I don't like using PluCal procedure because you need to manage the stack in your proof then and it is
> boring. I have just come across the Skip expression. I will try if we can use it for the discussed purpose.
 

Yes it works. But it adds an extra state. One might think about a false label called "done:" that would be merged

with the "Done" state. (I say that in case somebody wants to make changes to PlusCal, that's all.)

 

Another clause that I would add to PlusCal is the clause "precondition" because the clause "variable" is not

enough.

 

For instance if we had:

 

--algorithm test

variable v = 0

precondition VALIDPOINTER(p)

etc.

 

we would have the translation:

 

Init ==

  /\ v = 0

  /\ VALIDPOINTER(p)

 

--

FL

[Stephan Merz]

> Another clause that I would add to PlusCal is the clause "precondition" because the clause "variable" is not
> enough.
>
> For instance if we had:
>
> --algorithm test
> variable v = 0
> precondition VALIDPOINTER(p)
> etc.
>
> we would have the translation:
>
> Init ==
> /\ v = 0
> /\ VALIDPOINTER(p)

For such a simple case your proposed condition can equivalently be replaced by a set-valued initialization such as

variable p \in ValidPointer

TLC would not be able to evaluate arbitrary predicates appearing in preconditions.

Regards,
Stephan

[fl]

 

> For such a simple case your proposed condition can equivalently be replaced by a set-valued initialization such as

> variable p \in ValidPointer 
 

It depends what you mean by the predicate VALIDPOINTER. It might be more complex. Or

more generally, it might be a predicate with no meaning declared by a constant and intended

to be used with an opaque data

 

> TLC would not be able to evaluate arbitrary predicates appearing in preconditions.

 

Yes its true. But it is to be used with tlaps. And with tlaps I think it might be very helpful. But

it's true if such a clause were added to PlusCal it should be reported that it doesn't work with

TLC so that users are not misled.

 

--

FL

[Leslie Lamport]

   iflbl:
   if FEOF(x) = EOF
   then
     ret := 0;
     goto endlbl;
   end if
   endiflbl:
   ret := 1
   endlbl: <---- Here is the problem
   end algorithm

You can simply replace "goto endlbl" by "goto Done" and
remove the bogus label "endlbl".

----

      For such a simple case your proposed condition can equivalently be
      replaced by a set-valued initialization such as variable p \in
      ValidPointer
   
   It depends what you mean by the predicate VALIDPOINTER. It might be
   more complex.  Or more generally, it might be a predicate with no
   meaning declared by a constant and intended to be used with an opaque
   data

If VALIDPOINTER is a constant expression, then it makes no sense to
make it a precondition.  It should be asserted in the TLA+ module
with an ASSUME.  If VALIDPOINTER(p) is an arbitrary predicate, for
example,

   VALIDPOINTER(p) == \E S : p = SUBSET S

and you want to write

    variable p ;
    precondition VALIDPOINTER(p)

then I'm sorry, PlusCal is not the language for you; you'll have to
write it in TLA+.  There are many more interesting specs that can be
written in TLA+ and are difficult or practically impossible to write
in PlusCal.  (And, as in this case, can't be checked by TLC.)

On the other hand, if you want to write

    VALIDPOINTER(p) ==
       \E m, n \in Nat : IsPrime(m) /\ IsPrime(n) /\ p = m + n

then, as Stephan pointed out, you can easily write

   variable p \in {i \in Nat : VALIDPOINTER(i)}

[fl]

> You can simply replace "goto endlbl" by "goto Done" and
> remove the bogus label "endlbl".

Thank you. I'll use it tomorrow.

> then I'm sorry, PlusCal is not the language for you; you'll have to
> write it in TLA+. There are many more interesting specs that can be
> written in TLA+ and are difficult or practically impossible to write
> in PlusCal. 

 

Sure but we will no longer be able to benefit from the first-rate work

done by PlusCal as regards states and transitions modelization.

 

But anyway for the moment I only modify by hand the Init macro

when generated. But I need to remember to modify it every time I

generate it again.

 

 

--

FL

 

[fl]

Sure but we will no longer be able to benefit from the first-rate work

done by PlusCal as regards states and transitions modelization.

In fact I like PlusCal. If we consider TLA+ is a universal machine like Turing machine
(I only use the words in an unformal way), PlusCal shows in

[fl]

Sure but we will no longer be able to benefit from the first-rate work

done by PlusCal as regards states and transitions modelization.

In fact I like PlusCal. If we consider TLA+ is a universal machine like Turing machine

(I only use the words in an unformal way), PlusCal shows what a procedural
language is. It just shows what "procedurality" is. And, I would say, in a
very pedagogical way.

Maybe somebody would like to do the same thing for a functional language, a mock-lisp,
just as Plus-Cal is a mock-C. A pure functional language obviously.

It would be called Plus-Func, for instance.

--
FL