Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.ai
Subject: Semantics & provability
Keywords: meaning, symbol, understanding
Message-ID: <1907@uwm.edu>
Date: 16 Jan 90 02:51:20 GMT
References: <18883@bcsaic.UUCP> <1863@osc.COM> <1623@castle.ed.ac.uk>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Organization: University of Wisconsin-Milwaukee
Lines: 155

This response, which might be of general interest, has been forwarded to
this newsgroup (also the mail to the person indirectly mentioned in the letter
bounced).

* From lewis@godzilla.eecg.toronto.edu Mon Jan 15 08:09:55 1990
* From: david lewis <lewis@eecg.toronto.edu>
* To: markh@csd4.csd.uwm.edu
* Subject: Re: Program verification is a proven concept
* Date: 	Mon, 15 Jan 90 09:08:59 EST
* 
* You implied that there are algebraic rules for C. That would
* surprise me, due to the incredible aliasing problems. I would
* believe that you could express the semantics of C using denotational
* semantics, but that is not the easiest thing to manipulate. Can
* you point out any description of the semantics of C that can acutally
* be used?
* 
* For my own programs, I never bother to prove anything, since it is
* just too complex for any real program. I'm curious to hear a little
* bit more about your experience.
* 
* David Lewis

Date: Mon, 15 Jan 90 18:08:26 -0600
From: Mark William Hopkins <markh>
To: lewis@godzilla.eecg.toronto.edu, markh
Subject: Semantics & Proof

     A typical application, for me, would be to carry out an algebraic analysis
of a program or program segment either to verify it or to verify that some
assertion holds over it.  The end result can either be to prove that the
program does what it is supposed to do (i.e. demonstrate that the semantics
derived from the code matches the ever-vague "intent" -- with the latter
expressed in natural language or non-linguistically via diagrams), to
optimize the code -- by using algebraic rules to simplify code, or to
translate from one language to another.

     This letter is off the top of my head, so instead of trying to
deal with this in detail (especially with aliasing), I think it might be
more appropriate to forward you a response to another letter I received
(slightly edited).

     I'm assuming you're familiar with the lambda calculus, since it makes
quite a bit of reference to it.

------------------------------------------------------------
* markh@csd4.csd.uwm.edu (Mark William Hopkins) [14 Jan 90 02:21:43 GMT]:
* > Programs in even languages like C, Pascal can be manipulated via a set of
* > (complete) algebraic rules -- which form a foundation for the semantics
* > of the language in question.  I use such rules all the time.
* 
* I'm quite interested in this.  Do you have any examples online that
* you could send me (or do you use a pencil :-); can you send me any
* references?  Like so many others here, I am working in program semantics
* (CCS/lambda calculus), and am always interested in program proofs.

...
...

A simple rule in Pascal would look like this:

while B do S == if B then begin S; while B do S end

where B is any boolean expression, and S any statement, and "==" means
that both statements have precisely the same input-output semantics.

Another, more interesting, set of rules relating to pointers and to
structured types would allow you to prove that the Pascal sequence

A[I] := 3; B := A; B[I] := 2; writeln(A[I]:1)

will write out the value 3 (i.e. it is equivalent to the statement sequence
write("3"); writeln), and the C sequence

A[I] = 3; B = A; B[I] = 2; printf("%d\n", A[I]);

will write out the value 2 (it is equivalent to the statement printf("2\n");)

A key to the whole process is to directly translate the assignment statement
(involving simple variables) into the let statement of the extended
lambda calculus, and to translate assignments involving data structure
components or pointer references by using "updatable" functions.  For
example:

A[I] := 3; ...

would be translated into

let (A I) <- 3 in ...

and

P^ := 3; ...

as

let (VAL P) <- 3 in ... where VAL is a programmer-invisible updatable function
of type (^int -> int)

where

let (f a) <- b in E     means     let (f x) = if (= x a) b (f x) in E

or
	   (lambda f.E) (lambda x.if (= x a) b (f x))

Notice the difference between the results of

     let x = ... in
     ...
     let (f x) <- 3 in 
     let g = f in
     let (g x) <- 2 in (f x)
and
     let x = ... in
     ...
     let (x f) <- 3 in
     let g = f in
     let (x g) <- 2 in (x f)

One returns 3, and the other 2 (that is what underlies the difference between
the Pascal and C examples above).  The lambda calculus can model the
difference between "copying" and "sharing" (aliasing).

This correspondence between imperative and functional languages forms the
theoretical basis for the set of algebraic rules, but is not, itself, used as
a tool in the verification process.   The whole idea is to obviate the
need to have to bring in the lambda calculus by using a set of relatively
easy-to-use algebraic rules in its place.

Using algebraic rules alone, the above Pascal example would reduce like
this:
        A[I] := 3; B := A; B[I] := 2; writeln(A[I]:1)
==
	B := A{I <- 3}; B[I] := 2; writeln( A{I <- 3}[I]:1)
==
	A{I <- 3}[I] := 2; writeln( A{I <- 3}[I]:1)
==
	writeln( A{I <- 3}{I <- 2} {I <- 3}[I]:1)
==
	writeln(3:1)

where A{I <- x} is an extra-Pascal notation used to denote the lambda
expression:
	                 let (A I) <- x in A

One property of it used in the last reduction is:

	          A{I <- x}{I <- y} = A{I <- y}

This one reduction example illustrates that algebraic rules for a programming
language need not produce results that lie exclusively in that language.  It's
often more efficient to develop a set of rules that "preprocess" a program
segment into something outside that language, and subsequentially simplify
further analysis.