#|
 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
 WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
 LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "mc20-2" using the compiled version.

;          Proof of the Correctness of the STRLEN Function
#|
This is part of our effort to verify the Berkeley string library.  The
Berkeley string library is widely used as part of the Berkeley Unix OS.
This is the source code of strlen function in the Berkeley string library.
/* find the length of str[] */
size_t
strlen(str)
const char *str;
{
register const char *s;
for (s = str; *s; ++s);
return(s - str);

}
The MC68020 assembly code of the C function strlen on SUN-3 is given as
follows.  This binary is generated by "gcc -O".
0x25b0 <strlen>:        linkw fp,#0
0x25b4 <strlen+4>:      movel fp@(8),d0
0x25b8 <strlen+8>:      moveal d0,a0
0x25ba <strlen+10>:     tstb a0@
0x25bc <strlen+12>:     beq 0x25c4 <strlen+20>
0x25be <strlen+14>:     addqw #1,a0
0x25c0 <strlen+16>:     tstb a0@
0x25c2 <strlen+18>:     bne 0x25be <strlen+14>
0x25c4 <strlen+20>:     subl a0,d0
0x25c6 <strlen+22>:     negl d0
0x25c8 <strlen+24>:     unlk fp
0x25ca <strlen+26>:     rts
The machine code of the above program is:
<strlen>:    0x4e56  0x0000  0x202e  0x0008  0x2040  0x4a10  0x6706  0x5248
<strlen+16>: 0x4a10  0x66fa  0x9088  0x4480  0x4e5e  0x4e75
'(78      86      0       0       32      46      0       8
  32      64      74      16      103     6       82      72
  74      16      102     250     144     136     68      128
  78      94      78      117)
|#
; in the logic, the above program is defined by (strlen-code).

Definition: strlen-code

= '(78 86 0 0 32 46 0 8 32 64 74 16 103 6 82 72 74 16
      102 250 144 136 68 128 78 94 78 117)

Conservative Axiom: strlen-load strlen-loadp (s) = (evenp (strlen-addr)

∧ (strlen-addr ∈ N)

∧ nat-rangep (strlen-addr, 32)

∧ rom-addrp (strlen-addr, mc-mem (s), 28)

∧ mcode-addrp (strlen-addr, mc-mem (s), strlen-code))

Simultaneously, we introduce the new function symbols strlen-loadp and strlenaddr.

Theorem: stepn-strlen-loadp strlen-loadp (stepn (s, n)) = strlen-loadp (s)

; the computation time of the program.

Definition: strlen1-t (i, n, lst) = if i < n

then if get-nth (i, lst) = null then 6

else splus (3, strlen1-t (1 + i, n, lst)) endif else 0 endif

Definition: strlen-t (n, lst) = if get-nth (0, lst) = 0 then 9

else splus (6, strlen1-t (1, n, lst)) endif

; an induction hint.

Definition: strlen-induct (s, i* , i, n, lst) = if i < n

then if get-nth (i, lst) = null then t

else strlen-induct (stepn (s, 3), add (32, i* , 1), 1 + i, n, lst) endif else t endif

; the preconditions of the initial state.

Definition: strlen-statep (s, str, n, lst) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (mc-pc (s), mc-mem (s), 28)

∧ mcode-addrp (mc-pc (s), mc-mem (s), strlen-code) ∧ ram-addrp (sub (32, 4, read-sp (s)), mc-mem (s), 12) ∧ ram-addrp (str, mc-mem (s), n) ∧ mem-lst (1, str, mc-mem (s), n, lst) ∧ disjoint (str, n, sub (32, 4, read-sp (s)), 12) ∧ (str = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (slen (0, n, lst) < n) ∧ (n ∈ N) ∧ uint-rangep (n, 32))

; an intermediate state.

Definition: strlen-s0p (s, str, i* , i, n, lst) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (sub (32, 16, mc-pc (s)), mc-mem (s), 28) ∧ mcode-addrp (sub (32, 16, mc-pc (s)), mc-mem (s), strlen-code) ∧ ram-addrp (read-an (32, 6, s), mc-mem (s), 12) ∧ ram-addrp (str, mc-mem (s), n) ∧ mem-lst (1, str, mc-mem (s), n, lst) ∧ disjoint (str, n, read-an (32, 6, s), 12) ∧ equal* (read-an (32, 0, s), add (32, str, i* )) ∧ (str = read-dn (32, 0, s)) ∧ (i = nat-to-uint (i* )) ∧ (slen (i, n, lst) < n) ∧ (i* ∈ N) ∧ nat-rangep (i* , 32) ∧ (n ∈ N) ∧ uint-rangep (n, 32))

; from the intial state s to exit: s --> sn.

Theorem: strlen-s-sn (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) = 0)) → ((mc-status (stepn (s, 9)) = 'running)

∧ (mc-pc (stepn (s, 9)) = rts-addr (s)) ∧ (nat-to-uint (read-dn (32, 0, stepn (s, 9))) = 0) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 9)))

= add (32, read-an (32, 7, s), 4)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 9))) = read-an (32, 6, s)))

Theorem: strlen-s-sn-rfile (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) = 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: strlen-s-sn-mem (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) = 0) ∧ disjoint (x, k, sub (32, 4, read-sp (s)), 12)) → (read-mem (x, mc-mem (stepn (s, 9)), k) = read-mem (x, mc-mem (s), k))

; from the initial state s to s0: s --> s0.

Theorem: strlen-s-s0 (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) ≠ 0)) → strlen-s0p (stepn (s, 6), str, 1, 1, n, lst)

Theorem: strlen-s-s0-else (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) ≠ 0)) → ((linked-rts-addr (stepn (s, 6)) = rts-addr (s))

∧ (linked-a6 (stepn (s, 6)) = read-an (32, 6, s))

∧ (read-rn (32, 14, mc-rfile (stepn (s, 6))) = sub (32, 4, read-sp (s))))

Theorem: strlen-s-s0-rfile (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) ≠ 0) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: strlen-s-s0-mem (strlen-statep (s, str, n, lst) ∧ (get-nth (0, lst) ≠ 0) ∧ disjoint (x, k, sub (32, 4, read-sp (s)), 12)) → (read-mem (x, mc-mem (stepn (s, 6)), k) = read-mem (x, mc-mem (s), k))

; from s0 to exit (base case), from s0 to s0 (induction case).
; base case: s0 --> exit.

Theorem: strlen-s0-sn-base (strlen-s0p (s, str, i* , i, n, lst) ∧ (get-nth (i, lst) = 0)) → ((mc-status (stepn (s, 6)) = 'running)

∧ (mc-pc (stepn (s, 6)) = linked-rts-addr (s)) ∧ (nat-to-uint (read-dn (32, 0, stepn (s, 6))) = i) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 6))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 6))) = add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 6)), k) = read-mem (x, mc-mem (s), k)))

Theorem: strlen-s0-sn-rfile-base (strlen-s0p (s, str, i* , i, n, lst) ∧ d2-7a2-5p (rn) ∧ (get-nth (i, lst) = 0)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= read-rn (oplen, rn, mc-rfile (s)))

; induction case: s0 --> s0.

Theorem: strlen-s0-s0 (strlen-s0p (s, str, i* , i, n, lst) ∧ (get-nth (i, lst) ≠ 0)) → (strlen-s0p (stepn (s, 3), str, add (32, i* , 1), 1 + i, n, lst)

∧ (read-rn (32, 14, mc-rfile (stepn (s, 3))) = read-rn (32, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 3)) = linked-a6 (s))

∧ (linked-rts-addr (stepn (s, 3)) = linked-rts-addr (s))

∧ (read-mem (x, mc-mem (stepn (s, 3)), k) = read-mem (x, mc-mem (s), k)))

Theorem: strlen-s0-s0-rfile (strlen-s0p (s, str, i* , i, n, lst) ∧ d2-7a2-5p (rn) ∧ (get-nth (i, lst) ≠ 0)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 3)))

= read-rn (oplen, rn, mc-rfile (s)))

; put together (s0 --> exit).

Theorem: strlen-s0p-info strlen-s0p (s, str, i* , i, n, lst) → ((i < n) = t)

Theorem: strlen-s0-sn let sn be stepn (s, strlen1-t (i, n, lst)) in strlen-s0p (s, str, i* , i, n, lst) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s))

∧ (nat-to-uint (read-dn (32, 0, sn)) = strlen (i, n, lst))

∧ (read-rn (32, 14, mc-rfile (sn)) = linked-a6 (s))

∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (sn), k) = read-mem (x, mc-mem (s), k))) endlet

Event: Disable strlen-s0p-info.

Theorem: strlen-s0-sn-rfile (strlen-s0p (s, str, i* , i, n, lst) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, strlen1-t (i, n, lst))))

= read-rn (oplen, rn, mc-rfile (s)))

; the correctness of the STRLEN program.

Theorem: strlen-statep-info strlen-statep (s, str, n, lst) → (n ≄ 0)

Theorem: strlen-correctness let sn be stepn (s, strlen-t (n, lst)) in strlen-statep (s, str, n, lst) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = rts-addr (s)) ∧ (read-rn (32, 14, mc-rfile (sn))

= read-rn (32, 14, mc-rfile (s))) ∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-sp (s), 4)) ∧ (d2-7a2-5p (rn)

→ (read-rn (oplen, rn, mc-rfile (sn))

= read-rn (oplen, rn, mc-rfile (s))))

∧ (disjoint (x, k, sub (32, 4, read-sp (s)), 12)

→ (read-mem (x, mc-mem (sn), k)

= read-mem (x, mc-mem (s), k)))

∧ (uread-dn (32, 0, sn) = strlen (0, n, lst))) endlet

Event: Disable strlen-t.

; some properties of strlen.
; see the file cstring.events.

Event: Make the library "strlen" and compile it.

Index

add, 3–7

d2-7a2-5p, 4–7 disjoint, 3–5, 7

equal*, 4 evenp, 2–4

get-nth, 3–6

linked-a6, 5, 6 linked-rts-addr, 5, 6

mc-mem, 2–7 mc-pc, 3–6 mc-rfile, 4–7 mc-status, 3–6 mcode-addrp, 2–4 mem-lst, 3, 4

nat-rangep, 2, 4 nat-to-uint, 4–6 null, 3

ram-addrp, 3, 4 read-an, 4–6 read-dn, 4–6 read-mem, 3–7 read-rn, 4–7 read-sp, 3–5, 7 rom-addrp, 2–4 rts-addr, 4–6

slen, 3, 4 splus, 3 stepn, 3–6 stepn-strlen-loadp, 3 strlen, 6, 7 strlen-addr, 2 strlen-code, 2–4 strlen-correctness, 6 strlen-induct, 3 strlen-load, 2 strlen-loadp, 2, 3 strlen-s-s0, 4 strlen-s-s0-else, 5 strlen-s-s0-mem, 5 strlen-s-s0-rfile, 5 strlen-s-sn, 4 strlen-s-sn-mem, 4 strlen-s-sn-rfile, 4 strlen-s0-s0, 5 strlen-s0-s0-rfile, 6 strlen-s0-sn, 6 strlen-s0-sn-base, 5 strlen-s0-sn-rfile, 6 strlen-s0-sn-rfile-base, 5 strlen-s0p, 4–6 strlen-s0p-info, 6 strlen-statep, 3–6 strlen-statep-info, 6 strlen-t, 3, 6 strlen1-t, 3, 6 sub, 3–5, 7

uint-rangep, 3, 4 uread-dn, 7