Fwd: Algorithm derivation

[Jeremy Weissmann]

Enjoy!

+j

---------- Forwarded message ----------
From: Koray Erkan <ke-...@isnet.net.tr>
Date: 2012/3/7
Subject: Algorithm derivation
To: Jeremy Weissmann <jer...@mathmeth.com>




Hi Jeremy

 

(Please read the following note in HTML.)

 

This note is inspired by WF066. It offers a very simple intro to deriving algorithms, and is easy enough to understand. Or so you think when you read it.

 

Trouble is, I'm not familiar with a single source/material that lays out the techniques he refers to when he characterizes the techniques he uses there as "standard."

 

I, for my part, am still having difficulty with deriving some quite basic algorithms/loops from predicates that you would think should be obvious enough to render calculationally into program code.

 

Let me illustrate by a little exercise.

 

Assume we want to show that two arrays, a and b, are "rotated" versions of each other. We can formalize this as:

 

(0)    P: (E i: 0 < i < N: (A j: 0 < j < N: a[j] = b[(i+j) mod N])).

 

Our task: Derive the algorithm. (Note: We return true when the arrays are empty.)

 

My "intuitive" code for this is:

 

|[   i, j: int

;    i, j := 0, 0

;    do i /= N and j /= N

     -> if a[j]  = b[(i+j) mod N] -> j := j+1

        |  a[j] /= b[(i+j) mod N] -> i, j := i+1, 0

        fi

     od

;    print(j = N)

]|

 

I am not able to derive this algorithm from (0).

 

I tried the simplest cases like these:

 

(1)    P0: 0 < n < N

       P1: x == (A i: 0 < i < n: b.i)

 

    (n := n+1).P1

==        { replacement }

    x == (A i: 0 < i < n+1: b.i)

==        { split term }

    x == (A i: 0 < i < n: b.i) /\ b.n

==        { def. x from P1 }

    x == x /\ b.n

 

Hence:

 

|[  n: int

;   x, n := true, 0

;   do x and n /= N

    -> x, n := b.n, n+1

    od

    { R: x }

]|

 

OK, this was simple enough, but is this the only way of expressing this? How about this version?

 

|[  i, n: int

;   i, n := 0, 0

;   do i /= N

    -> if  b.i -> i, n := i+1, n+1

       |  ¬b.i -> i := N

       fi

    od

    { R: n = N }

]|

 

How do we show that either algorithm maps back to P1?

 

Here's another one:

 

(2)    P0: 0 < m < M /\ 0 < n < N

       P1: (E i: 0 < i < m: (A j: 0 < j < n: b.i.j))

 

My intuitive code for this is :

 

|[  m, n: int

;   m, n := 0, 0

;   do m /= M and n /= N

    -> if  b.m.n -> n := n+1

       |  Â¬b.m.n -> m, n := m+1, 0

       fi

    od

    { R: n == N }

]|

 

Again, I am not able to derive this calculationally from P1.

 

Is there any document you can direct me to where I can find those "standard" derivation techniques?

 

Thanks.

 

Cheers

-- Koray