-----------------------------------------
PART-1
-----------------------------------------

*** 1. b,c

    Note: (d) is correct under partial correctness, but not under
    total correctness since S may not terminate.

*** 2. c

   Note-1:

	The wp wrt u1=u2 is:

	    u1=u2[new LINK/u2][new LINK/u1]

	    = {apply the inner subst }

	    false[new LINK/u1]

	    = 

	    false

   Note-2

       The wp wrt (EXISTS z:LINK.  z.link=v) is:

            (EXISTS z:LINK.  z.link=v)[new LINK/u2][new LINK/u1]

            = { apply the subst on u2 }

            ((EXISTS z:LINK.  (z.link=v)[new LINK/u2]) \/ (u2.link=v)[new LINK/u2])[new LINK/u1]

            = { apply the subst on u2 in the body of EXISTS }

            ((EXISTS z:LINK.  z.link=v) \/ (u2.link=v)[new LINK/u2])[new LINK/u1]

            = { apply the subst on u2; note that u2.link is subst with the default null }

            ((EXISTS z:LINK.  z.link=v) \/ (null=v))[new LINK/u1]

	    = { now apply the subst on u1 ... after quite similar sequence you'll get: }

            (EXISTS z:LINK.  z.link=v) \/ (null=v) \/ (null=v)


*** 3. c (discussed in the lecture)


*** 4. b

       Note: well, (a) false would be far too strong for the
       initialization. (b) true would be too weak to imply the
       post-condition. (c) i<=n is invariant, but it is not sufficient
       to imply that your termination metric (which is i) is bounded
       below.

-----------------------------------------
PART-2
-----------------------------------------

>>>>> 1.

For convenience, introduce an abbreviation "ok" (see below). The proof
plan:

   { 0 < n, Pinit is skipped }

   i:=0; s:=T ;

   { I, see PIC and PEC; PTC1,2 are skipped (they are quite trivial);
     termination metric: m = n-i }

   while i < n - 1 do { s := s /\ (a[i] = a[i + 1]) ; i:=i+1 }

   { s = ok (n-1) }

assuming

  ok i = (FORALL k : 0<= k < i : a[k] = a[k + 1])

  I = (s = ok i) /\ 0<=i<n

        
-------------------------------
PROOF PEC
   A1: (s = ok i) /\ 0<=i<n
   A2: i>=n-1
   G:  (s = ok (n-1))

   1. { follows from i<n part of A1 and A2}        i=n-1

   2. { rewrite the 1-st conjunct of A1 with 1 }   s = ok (n-1)

-------------------------------
PROOF PIC
   A1: (s = ok i) /\ 0<=i<n
   A2: i<n-1
   G:  wp loop-body I

   1.  { wp calc }
 
        G = (s /\ (a[i]=a[i+1]) = ok (i+1))  /\   0<=i+1<n

   2. { see the proof below }
        s /\ (a[i]=a[i+1]) = ok (i+1)
 
              ok (i+1)
            = {def. ok}
              (FORALL k : 0<= k <i+1 : a[k] = a[k+1])
            = { domain merge, justified by 0<=i, which is implied by A1}
              (FORALL k : 0<=k<i \/ k=i : a[k] = a[k+1]) 
            = { domain split + FORALL over sing }
              (FORALL k : 0<=k<i : a[k]=a[k+1]) /\ (a[i]=a[i+1])
            = {def. ok}
              ok i /\ (a[i]=a[i+1])
            = { rewrite with the first conjunct of A1 }
              s /\ (a[i]=a[i+1])

  3. { follows from the 2nd conjunct of A1 } 0<=i+1

  4. { follows from A2 } i+i<n

  5. { conjunction of 2,3,4 }  (s /\ (a[i]=a[i+1]) = ok (i+1)) /\ 0<=i+1<n

  6. { rewrite 5 with 1 }  G


>>>>> 2. 

Well... this shouldn't be too difficult. I'll leave it to you to
puzzle it out.


>>>>> 3.

Goal:

  { 0 < n }
 
  i:=0; s := T ; // init
  while i<n-1  /\ a[i]>=0 
    do
    { s := s /\ (a[i] = a[i + 1]) ; i:=i+1 } // body

  { Q1 \/ Q2 }

DEF: I = as in No. 1
DEF: Q1 = (s = (FORALL k : 0<=k<n-1 : a[k] = a[k + 1])
DEF: Q2 = (EXISTS k : 0<=k<n-1 : a[k]<0)
-------

1. { has been proven in No 1 }

   { 0<n } init {I} 

2. { has been proven in No 1 }

   {I} while i<n-1 do body {Q1}

3. { post-cond weakening on 2 }

   {I} while i<n-1 do body {Q1 \/ Q2}

4. { see the proof below } I /\ i<n-1 /\ ~a[i]>=0 ==> Q2

         PROOF P
         A1  : I
         A2  : i<n-1
         A3  : ~a[i]>=0
         Goal:  (EXISTS k : 0<=k<n-1 : a[k]<0)

         1. { follows from A3 } a[i]<0

         2. { follows from 2nd conjunct of I } 0<=i

         3. { combining 2 and A2} 0<=i<n-1

         4. { EXISTS-intro on 1 and 3 } (EXISTS k : 0<=k<n-1 : a[k]<0)

5. { has been proven in No 1 }  {I /\ i<n-1} body {I}

6. { Loop-str rule on 3,4,5 }

   {I} while i<n-1 /\ a[i]>=0 do body {Q1 \/ Q2}

7. {SEQ rule on 1 and 6 }

    G


>>>>> 4.

To prove the requested specification, we first transform the code to
the one below, which is equivalent. We also add assertions:

{ a[k]<0, see proof P } 

{P1, see note-1}  i := k; 

{P2, see note-2}  @x,@y := a[i],i

{P3, see note-3}  foo(@x,@y)

{P4, see note-4}  a[i],i := @x,@y

{Q: a[k]>0 }

Note-4: take P4 = wp wrt Q = (a(i repby @a))[k]>0

Note-3: obtain P3 via BB Reduction on P3 -->

   P3 = @x<=0 
        /\ 
        ((x'=y') /\ y'>0  ==> ((a(i repby x'))[k]>0))

Note-2: take P2 = wp wrt P3 = 

        a[i]<=0 
        /\ 
        ((x'=y') /\ y'>0  ==> ((a(i repby x'))[k]>0))

Note-1: take P1 = wp wrt P2 =

        a[k]<=0 
        /\ 
        ((x'=y') /\ y'>0  ==> ((a(k repby x'))[k]>0))

       = { simplifying repby }

        a[k]<=0 
        /\ 
        ((x'=y') /\ y'>0  ==> x'>0)

      = { the second conjunct is true, so can be eliminated }

        a[k]<=0

Proof P: well, you have to prove that a[k]<0 implies a[k]<=0, which is
trivial of course.


>>>>> 5.

To compute the wp, calculate the following substitutions:

 
         (EXISTS z:LINK.  z.link.link = w)[u/this.link][new LINK/u]


We first calculate the first substitution:


            (EXISTS z:LINK.  z.link.link = w)[u/this.link]

         =  { applying the substitution recursively }

            (EXISTS z:LINK.  (z.link.link = w)[u/this.link])
         
         =  { applying the substitution recursively }

            (EXISTS z:LINK.  ((z=this ? u : z.link) = this
                               ?
                               u : (z=this ? u : z.link).link) 

                              = w)

         =  { we'll rewrite this a bit further to prepare for the second subst. }

            (EXISTS z:LINK.   (z=this ? u=this : z.link=this)
                               ?
                               u=w : (z=this ? u.link=w : z.link.link=w))

Now applying the second subst. on the resulting formula:


            (EXISTS z:LINK.   (z=this ? u=this : z.link=this)
                               ?
                               u=w : (z=this ? u.link=w : z.link.link=w))
            [new LINK/u]

            = { new-object subst on EXISTS }

            (EXISTS z:LINK.   ((z=this ? u=this : z.link=this)
                               ?
                               u=w : (z=this ? u.link=w : z.link.link=w))
                              [new LINK/u]
             )
            \/ 

            ((u=this ? u=this : u.link=this)
              ?
              u=w : (u=this ? u.link=w : u.link.link=w))
              [new LINK/u]

            = { recursively applying new-object subst }

            (EXISTS z:LINK.   (z=this ? false : z.link=this)
                              ?
                              false : (z=this ? null=w : z.link.link=w))

            \/ 

            ((false ? false : null=this)
              ?
              false: (false ? null=w : null.link=w))

            = { after some simplification you'll get: }

            (null=w) \/ (EXISTS z:LINK.  z.link <> this /\ z.link.link=w)

            \/ 

            (null<>this /\ null.link=w)

            = { well, null.link gives "undefined", and in cOOre
            undefined=w cannot be true (even if w is also undefined) }

            (null=w) \/ (EXISTS z:LINK.  z.link <> this /\ z.link.link=w)