Re: Does go have a return value ?

Spiros Bousbouras <spibou@xxxxxxxxx> writes:

On 30 Nov 2009 14:37:41 -0800
tar@xxxxxxxxxxxxx (Thomas A. Russ) wrote:
Spiros Bousbouras <spibou@xxxxxxxxx> writes:


(let ((a 0))
(tagbody
tag
....
(when (= a 0)
(setq a (go tag)))
...))

Lisp could have worked in such a way that a gets modified. If (go tag)
returned something other than 0 (it might return the name of the tag it
jumped to) then you could use the technique to make sure that you jump
backwards at most once. I'm not saying it would be an improvement if
things worked this way but they might and it wouldn't derail the
semantics of go any more than unwind-protect does.

Um, I still don't see it. The fundamental problem is that you have to
evaluate the argument "(go tag)" to SETQ before you have a value to use
to set the variable. But the act of evaulation GO is to transfer
control to the TAG. So, before you have a value you can use, you have
already moved the execution of the program to another point.

Does this present any bigger problems than unwind-protect ?

Immensely.

UNWIND-PROTECT very explicitly defines the order of execution of the
forms. It guarantees that certain forms WILL be executed in order
regardless of whether the protected statement terminates normally or
through an abnormally (including a transfer of control). So that just
involves specifically saying what happens.

Now, if you want to look into it more deeply, you could consider what
happens when one of the clean-up forms in UNWIND-PROTECT also transfers
control. There is an example in the hyperspec where the consequences
are undefined because of the interaction of control transfer between the
protected clause and the clean-up forms.


You can't realistically have any other result for GO. I mean, what are
the semantics supposed to be? The GO form returns a value, then has to
wait for some other function to finish execution, and THEN transfer
control? How would you know exactly where in this process of argument
evaluation and function application to stop an insert the jump?

What about code like:

(let ((v nil)
(result 0))
(tagbody
tryagain
(setq v (get-value-from-user "Enter number: "))
(setq result (/ 128 (if (zerop v) (go tryagain) v))))
result)

At what point does the upward percolation of values stop and the
transfer of control begin?

Good question and I don't know the answer. Your example shows that it
would be messy to define precise semantics and if you did it would
complicate the use of go so things are probably better as they are.

Well, this is why it is difficult, perhaps impossible to actually write
something that could be implemented. At least with UNWIND-PROTECT, you
have specifically stated what forms will get executed and in what
order. Without some syntactic marker to indicate what gets unwound, you
really don't have anything you can do.

Then there is the whole issue of what you would want to do with any
value returned by GO in the first place. If you look at other control
transfer operators, like THROW, they don't return values either. It is
the CATCH that returns a value, even if that value was specified by the
THROW.

But when I first asked the question I was thinking more around the
lines that if you want to use formal methods to prove things about a
programme it would probably make things easier if every form returned a
value.

Well, if it makes you feel better, you can pretend that GO returns any
value you like. You still have to deal with the problem of the transfer
of control. Now, I haven't looked at formal program proof methods in
decades, but it seems to me that having any sort of control transfer of
this nature will greatly complicate any proofs you might construct.

So you're saying that the transfer of control would present greater
problems for formal proofs than whether go returns a value or not ,
yes ?

Sure.

The value it returns is completely irrelevant, because nothing ever gets
to use that value. So it really doesn't matter. The problem for a
formal proof is that you have now to consider how to model and track
this non-local transfer of control or execution flow.

BTW, that's also why GOTO statements have been largely elminated from
most modern programming languages. There was a whole series of articles
debating this in the 1970s or 1980s.


--
Thomas A. Russ, USC/Information Sciences Institute
























.

Relevant Pages

  • Re: Three questions about UNWIND-PROTECT
    ... and then the transfer of control to the tag ... if dummy-function is called first and then the cleanup ... What else can UNWIND-PROTECT do? ... flow of execution will return inside the unwind-protect ...
    (comp.lang.lisp)
  • RealNetworks RealGames StubbyUtil.ShellCtl.1 ActiveX Control (InstallerDlg.dll v2.6.0.445) Multiple
    ... RealNetworks RealGames StubbyUtil.ShellCtl.1 ActiveX Control ... Multiple Remote Commands Execution ... CreateShortcut-> allows to create arbitrary executable files inside the automatic ... ProductName: InstallerDlg Module ...
    (Bugtraq)
  • Re: Debugging Challenge - no source available
    ... transparent backgrounds - I previously noticed some bizarre behavior when I ... tried to set a control's background to a transparent bitmap (the transparent ... I've decided to derive my own control from the label control I'm ... >> In both cases, the debugger catches execution at the same point, just ...
    (microsoft.public.dotnet.general)
  • Re: how to turn off NX bit in assembly?
    ... code using the faults to stop execution in an additional controlled ... Instead of unmapping and flush a page upon a page fault and loading another ... one could terminate the program at that point. ... they could interrupt on flow control. ...
    (alt.lang.asm)
  • Re: how to turn off NX bit in assembly?
    ... code using the faults to stop execution in an additional controlled ... one could terminate the program at that point. ... probably look at the debug registers to see what control of code they ... the ACPI doesn't distinguish apps ...
    (alt.lang.asm)