next up previous contents
Next: The marker phase of Up: Imperative programs Previous: Hoare logic: Inversion



The work documented in this section has been contributed by Rod Burstall, Adriana Comagnoni and Thomas Schreiber have been working as part of a collaboration with Harlequin Ltd., who write LISP compilers amongst other products. It is a couple of loops which update an array as one scan of the marking phase.

Fri May 24 19:01:27 BST 1996