Re: Formal Semantics of the Java "new" Operator

From: Arthur J. O'Dwyer (ajo_at_nospam.andrew.cmu.edu)
Date: 05/01/04 

Date: Fri, 30 Apr 2004 22:30:58 -0400 (EDT)

On Fri, 30 Apr 2004, Mattias Wikstr?m wrote:
>
> Lauri Alanko <la@iki.fi> wrote...
> > Mattias Wikstr?m <mattias_wikst71@hotmail.com> wrote:
> > > I am interested in approaches to formally describing what the Java
> > > "new" operator does.
> >
> > Any book on the theory of programming languages ought to do.
<snip>
> > The basic idea is to have an explicit state which operations can
> > modify (that is, they can return updated states). The addresses of
> > objects are formalized as "locations" (e.g. integers), and each
> > allocation alters the state and marks that location as in use. That is
> > why each allocated object has a unique, distinct location.
>
> This was helpful (thanks!).
>
> What I now wonder is: What kind of thing may a location be?

  A "location," assuming I understand Lauri's terminology fully,
is simply that --- it's a "location." Asking "what is a location?"
is like asking "what is a number?": I may not be able to define it,
but I know it when I see it.

> I suppose
> that in mathematics it will typically be a natural number, whereas for
> a compiler writer it will typically be a relocatable memory address or
> an "int".

  You have very muddled ideas. What I think of as the "main stream"
of mathematics by and large does not try to describe computations.
A mathematical proof might show that X *is* computable, or simply
that X *exists* (or doesn't); but straight math isn't really concerned
with algorithms. Algorithms belong to computer science --- if pressed,
I'd say they belong to computer science /by definition/.

  "2+2 = 4" is a mathematical statement: it represents a true proposition.
"2+2 -> a" is an algorithm; it represents a procedure for storing the
value 4 in the location "a". Never the twain shall meet.

> In each of these cases there is arbitrariness involved: When the
> "new" operator gets called, an unused number must somehow be chosen.

  Muddled. Typical computers these days have what's called RAM, or
"random access memory," which is essentially a big pool of "storage,"
like a bunch of lockers lined up in a row. The RAM is indexed by
memory addresses, which are typically some sort of integers. Any
program that wants to use a particular part of RAM has to specify
exactly which "locker number" it wants to use, as part of the program.
For example, an implementation of a "stack" data structure might go
like this:

    m0 <- m1
    procedure PUSH x
      begin
        m[m0] <- x
        m0 <- m[m0] + 1
      end

Note that we're never "creating" any "new" memory; all we're doing
is performing deterministic computations using the memory we already
have installed on our computer. There is no magic "somehow" involved
here; no Axiom of Computer Choice is necessary.

> Whenever I encounter arbitrariness in mathematics, I want to
> understand its precise nature, and preferably do away with it. It
> seems to me that the only non-arbitrary way to model locations is to
> model them as...locations.

  Now you're catching on: Just as the only non-arbitrary way to
model integers is as... integers! And real numbers as... real numbers!
And strings as... strings!

> It seems to me that Java has something that can only be modelled in
> traditional mathematics at the expence of introducing arbitrariness of
> a special sort. This suggests using something other than traditional
> mathematics to do the modelling (Java, at worst ;-) ).

  As I said, mainstream math doesn't deal with algorithms. There are
all sorts of formal studies of algorithms, but you'll have to look to
computer science for them in the majority of cases, I think.

> Denotational semantics was what I primarily had in mind, but instead
> of trying to find a semantics for Java, I would pick something
> simpler. Let us say simply typed lambda calculus extended with a new
> kind of functions that always give /new/ values as their results. I do
> not know how to formalise this, but if you press me I may figure it
> out.

  Read a tutorial on ML (aka S[tandard]ML). As Lauri said, its
"references" are exactly what you're looking for.

-Arthur

Relevant Pages

  • Re: Collection Structure
    ... but here's a couple of algorithms to sort a collection with vb methods only: ... I'm figuring out that there will be some kind of method I could use to let a C++ procedure swap pointers to sort the ... but I don't know how the collection object structure is in memory so I couldn't know exactly how to do. ... technical resource I could take a look at? ...
    (microsoft.public.vb.com)
  • 6P=NP: Proof: Harvey Friedman Revised
    ... The equation P = NP concerns algorithms for deciding ... Discrete complexity theory is dependent on a formal ... that discusses Turing machines without resource bounds ... comparable to some of the great problems of mathematics ...
    (sci.math)
  • Re: random generator for a given period
    ... > that memory seems cheap without being so. ... The efficiency game it all about algorithms and rarely about polishing the code. ... Then you can sort on the random numbers with the array of indices passive. ... So what I'm looking for is a random numbers generator of a given period and with the range equal to the period. ...
    (sci.stat.math)
  • ebooks forum..
    ... Lie-Backlund Transformations in Applications Robert L. Anderson and 1 ... Interior Point Polynomial Algorithms in Convex Programming Yurii ... Linear Matrix Inequalities in System and Control Theory Stephen Boyd, ... Mathematics Applied to Deterministic Problems in the Natural ...
    (sci.med.nutrition)
  • Re: teaching a child - console or GUI
    ... Implementing tricks to make a RDBMS compete with an in-mem solution is not ... only requires adding some memory to some old server or workstation and copying ... data + server .exe on it. ... > I really do believe that the key to speed is algorithms, ...
    (comp.lang.pascal.delphi.misc)
Loading