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.theory
Subject: Semantics & Provability
Message-ID: <1910@uwm.edu>
Date: 16 Jan 90 04:09:03 GMT
References: <1909@uwm.edu>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Organization: University of Wisconsin-Milwaukee
Lines: 200


     This is another forwarded response to a letter, which I feel might be of
general interest (the mail to this user bounced too).

>From: gateley@m2.csc.ti.com (John Gateley)
Date: Mon, 15 Jan 90 10:20:15 CST
Subject: Re: Program verification is a proven concept

Hi Mark,

In article <1888@uwm.edu> you write:
>I must've missed the boat: I always prove my programs correct.  Pathologies
>in provability (which are theoretically guaranteed) almost always indicate
>flaws in design.  Therefore undecibeability is actually an AID in program
>verification, not an obstacle.

I am very curious: which language(s) do you program in, and could you
send me an example of a program plus proof?

Thanks,

john
gateley@m2.csc.ti.com

------------------------------------------------------------

The imperative languages I program in are C, and Pascal (and also the
assembly for the Intel 8051 family).

I'll send you a proof of a program segment illustrating some very basic rules:

PROVE:
N = 2; X = 4;
for (I = 0, Y = 1; I < N; I++; Y *= X);
printf("%d", Y);

PRINTS OUT THE VALUE 16.

(1) A for-loop in C is equivalent to a while loop (as specified in the K&R
reference).  Making the transformation specified in the source here gives:

N = 2; X = 4; I = 0; Y = 1;
while (I < N) {I++; Y *= X;}
printf("%d", Y);

(2) Under certain conditions (not to be delineated here) as assignment
                              V op= C
is equivalent to
                             V = V op C
These conditions are met here.  Likewise I++ transforms to I = I + 1 in this
context.  This results in:

N = 2; X = 4; I = 0; Y = 1;
while (I < N) {I = I + 1; Y = Y * X;}
printf("%d", Y);

The conditions, or course, relate to the possibility to side-effects, such as
in
			      V += V++ - --V;

An algebraic rule to handle this would be implementation dependent.  For
example, if a compiler evaluates from left-to right, the assignment above
might be reducible successively to:

       x1 = V++;            x2 = --V;          V += x1 - x2;

   x1 = V; V = V + 1;   V = V - 1; x2 = V;    V =  V + x1 - x2;

	x1 = V;                x2 = V;          V = V + x1 - x2;
(notice the cancellation)

		           V = V + V - V;

			       V = V;

				 ; (the null statement)

where x1, and x2 are variables not occurring elsewhere in the program.

(3) A while-loop is equivalent to an INFINITELY nested sequence of
if-statements expressed recursively by the following rule:

while (B) do S  ==  if (B) {S; while (B) do S}
i.e.
      if (B) {S; if (B) {S; if (B) {S; ...}}}

This rule will be used in the following reductions below.

(4) The following are equivalent:

if (B) S1; else S2; T  ==  if (B) {S1; T} else {S2; T}

applied in the case of the sequence:

while (I < N) {I = I + 1; Y = Y * X;}
printf("%d", Y);

this produces an infinitely-nested series of branches defined recursively by:

xx = if (I < N) {I = I + 1; Y = Y * X; xx} else printf("%d", Y);

(5) A rule analogous to the BETA REDUCTION rule applies for assignment
statements of the form: Simple-Variable = Expression.  When used on the
sequence:

N = 2; X = 4; I = 0; Y = 1; xx

(with xx defined as above), this gives the successive reductions:

N = 2; X = 4; I = 0; Y = 1; xx
->
X = 4; I = 0; Y = 1; xx'
->
I = 0; Y = 1; xx''
where xx', xx'' are defined by

xx' = if (I < 2) {I = I + 1; Y = Y * X; xx'} else printf("%d", Y);
xx'' = if (I < 2) {I = I + 1; Y = Y * 4; xx''} else printf("%d", Y);

I = 0; Y = 1; xx''
->
Y = 1; if (0 < 2) {I = 0 + 1; Y = Y * 4; xx''} else printf("%d", Y);
->
if (TRUE) {I = 1; Y = 1 * 4; xx''} else printf("%d", 1);
->
I = 1; Y = 4; xx''
->
Y = 4; if (1 < 2) {I = 1 + 1; Y = Y * 4; xx''} else printf("%d", Y);
->
if (TRUE) {I = 2; Y = 4 * 4; xx''} else printf("%d", 4);
->
I = 2; Y = 16; xx''
->
Y = 16; if (2 < 2) {I = 2 + 1; Y = Y * 4; xx''} else printf("%d", Y);
->
if (FALSE) {I = 3; Y = 16 * 4; xx''} else printf("%d", 16);
->
printf("%d", 16);
->
printf("16");

These are very fine-grained steps, however.  In their place, and based directly
on the rules used in manipulating the loop, there is a more general theorem
that can be used to generate a system of Diophantine equations from this
loop. 
   More generally, the rules only provide a theoretical foundation, and are
not to be used on a practical level -- so there are more powerful tools of
analysis that can be developed, based directly on them, that can be used in
their stead.
   For example (3), (4) and other identities involving control-constructs can
be used as the basis for transforming and optimizing control-constructs.  I've
used this once to transform a C code segment from:

NameInsert(N, Head, Tail)
struct NameList *N, **Head, **Tail;
{
   if (*Tail == 0) {
      N->Prev = N->Next = 0; *Head = *Tail = N;
   } else {
      (*Head)->Prev = N; N->Prev = 0;
      N->Next = *Head; *Head = N;
   }
}

NameDelete(N, Head, Tail)
struct NameList *N, **Head, **Tail;
{
   if (N->Prev == 0)
      if (N->Next) {
         *Head = N->Next; N->Next->Prev = 0;
      } else *Tail = *Head = 0;
   else if (N->Next == 0)
      if (N->Prev) {
         *Tail = N->Prev; N->Prev->Next = 0;
      } else *Tail = *Head = 0;
   else {
      N->Prev->Next = N->Next; N->Next->Prev = N->Prev;
   }
}

to:

NameInsert(N, Head, Tail)
NameList N, *Head, *Tail;
{
   if (*Tail == 0) *Tail = N; else (*Head)->Prev = N;
   N->Prev = 0; N->Next = *Head;
   *Head = N;
}

NameDelete(N, Head, Tail)
NameList N, *Head, *Tail;
{
   if (*Head == N) *Head = N->Next; else N->Prev->Next = N->Next;
   if (*Tail == N) *Tail = N->Prev; else N->Next->Prev = N->Prev;
}

The software this came from was a 100k teleconferencing program, which I
optimized to under 50k and verified, there were a couple other (valid)
assumptions that were needed to make the transformation above.