Re: Does go have a return value ?

Spiros Bousbouras <spibou@xxxxxxxxx> writes:

Could you sketch your idea of any code at all, that could even notice?
Let's say in one implementation, GO's "return value" is defined to be T.
And in another, GO's "return value" is defined to be NIL.

Please explain how you would ever be able to tell which was which.

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

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?

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.

But I suspect that Lisp is too messy to allow for wide use of
formal methods anyway ; this is more suited to pure functional
languages.

I would think so. You would want to apply formal methods to either a
subset of lisp, or to a domain-specific programming language implemented
in Lisp that has more proof-friendly semantics and restrictions.

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

Relevant Pages

  • Re: Setting FaceID on Custom Button
    ... You can, for example, apply a Tag to your control. ... the same way as you set the caption). ... "MyControl Off". ...
    (microsoft.public.word.docmanagement)
  • Re: Function executed twice
    ... I would also like to say, just in case you don't do it already, that using prefixes for your control ids can make it easier when working in code. ... You do NOT need to add anything to the tag in the *.aspx file ... > code-behid I usually click twice in the link/button and that will ADD the ...
    (microsoft.public.dotnet.framework.aspnet)
  • Re: Does go have a return value ?
    ... If (go tag) ... Does this present any bigger problems than unwind-protect? ... UNWIND-PROTECT very explicitly defines the order of execution of the ... through an abnormally (including a transfer of control). ...
    (comp.lang.lisp)
  • Help needed with AddParsedSubObject() and ControlBuilder()
    ... I've created a test custom control that is declared as follows... ... The AddParsedSubObject code looks like this... ... that tag name as shown in the psuedo code below... ... How can I get to the tag name outside of GetChildControlType()? ...
    (microsoft.public.dotnet.framework.aspnet.buildingcontrols)
  • Formal Methods for Aerospace: 2nd edition
    ... "FMA@CDC: Formal Methods for Aerospace" ... Conference on Decision and Control ... Aerospace applications and formal methods are topics of large interest ... Logics for Stochastic Hybrid Control Systems ...
    (comp.specification.z)