On 12/8/2012 7:03 PM, Obrst, Leo J. wrote:
> There is limited research in general for denotational
> semantics of procedural programming. (01)
There has been an enormous amount of research in that area, but
it usually depends on a special language for writing the procedures: (02)
1. Formal specifications: The Vienna Definition Language (VDL) was
a logic-based language and methodology (VDM) that was started by
Heinz Zemanek in the 1960s. Their most notable achievement was
the formal definition of PL/I, which led to important changes in
the language. They used an axiomatic method for specifying an
abstract machine that executed the language. This method is
logic-based, but it's not really denotational semantics. (03)
2. Scott-Strachey denotational semantics: In the early 1970s,
Dana Scott worked at Oxford U. with Christopher Strachey
on denotational semantics. Scott earned his PhD at Princeton
with Alonzo Church as his thesis adviser. It's no coincidence
that he based the semantics on lambda calculus. Joseph Stoy
wrote a book on that semantics (1977). (04)
3. Hoare Logic: Tony Hoare developed a system for representing,
analyzing, and reasoning about programs. It's based on
"Hoare Triples": (05)
{Preconditions} Command {Postconditions} (06)
Then he developed methods for relating the preconditions and
postconditions of any procedure to those of each command or
subprocedure in it. When such procedures are combined with logic,
the preconditions and postconditions can be added to the axioms
of the ontology. For example, Peano's axioms could specify the
arithmetic operators that are implemented procedurally. (07)
4. Functional programming: A function is a formal object in logic,
and it can also be implemented efficiently on a digital computer.
Functional programming is a method of creating programs as pure
functions defined as the composition of more primitive functions.
The resulting program *is* a logical expression that has a well-
defined denotation. McCarthy designed LISP as a functional
language, but the "scruffies" added a lot of procedural stuff. (08)
5. Logic programming: This is a relation-based alternative to
functional programming. Cordell Green proposed it in 1969.
Prolog is the most widely known version, but it has a lot
of procedural features. But there are more pure versions. (09)
6. Pi calculus. This is Robin Milner's method for specifying
concurrent systems that pass messages among themselves.
Milner describes it as the concurrent extension to lambda
calculus: any function can be implemented by message passing,
but pi calculus is much more flexible and extensible. (010)
At VivoMind, we use a method of message passing that implements
a version of pi calculus for message passing among independent
modules or agents. For a purely formal system, the agents would
have to be specified by some pure version of functional or
logic programming. (011)
In practice, it's necessary to accommodate legacy systems and
anything anyone might invent in the future. That would limit
the ability to prove everything formally. But it's still possible
to do some useful reasoning: (012)
1. Every module would have some specified constraints (preconditions
and postconditions) on what it does with messages. (013)
2. But these constraints would be *underspecified*. Any module
might have side effects that other modules might not know. (014)
3. This is a realistic approach that is better than what we have
today, but requiring total specifications of what each module
does is impossible to achieve. (015)
4. Furthermore, privacy and security reasons would make total
knowledge undesirable or even dangerous. (016)
John (017)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (018)
|