references/addrresses in imperative languages

Kaz Kylheku kkylheku at gmail.com
Tue Jun 21 05:18:09 CEST 2005


Lawrence D’Oliveiro wrote:
> In article <1119220461.626477.56110 at g49g2000cwa.googlegroups.com>,
>  "Xah Lee" <xah at xahlee.org> wrote:
>
> >A[n] easy way to see this, is to ask yourself: how come in mathematics
> >there's no such thing as "addresses/pointers/references".
>
> Yes there are such things in mathematics, though not necessarily under
> that name.
>
> For instance, in graph theory, edges can be considered as "pointers".
> After all, make a change to a node, and that change is visible via all
> edges pointing to that node.

Oh yeah, by the way, note how such destructive changes to a variable
become whole-environment derivations in the discipline of proving the
correctness of imperative programs.

E.g. say you have this assignment:

   x <- x + 1

and you want to deduce what preconditions must exist in order for the
desired outcome   x = 42   to be true after the execution of the
statement. What do you do? You pretend that the program is not
modifying a variable in place, but rather manufacturing a new
environment out of an old one. In the new environment, the variable X
has a value that is one greater than the corresponding variable in the
old environment. To distinguish the two variables, you call the one in
the old environment X' .

You can then transform the assignment by substituting X' for X in the
right hand side and it becomes

  x <= x' + 1

and from that, the precondition  x' = 41  is readily deduced from the
x = 42  postcondition.

Just to be able to sanely reason about the imperative program and its
destructive variable assignment, you had to nicely separate past and
future, rename the variables, and banish the in-place modification from
the model.




More information about the Python-list mailing list