Hardware/doc preservatoion, was Re: rarest computers.

From: Andy Holt <andyh_at_andyh-rayleigh.freeserve.co.uk>
Date: Mon Aug 9 00:02:35 2004

> PS. It is certainly true that programs can be proven to match their
> specification. That's not quite the same as proving them bug free --
> it now requires the specification to be bug free.
> But such proofs in no way require the absence of a stack. That's
> actually rather obvious, because any program that uses a stack can be
> rewritten into a program that does not use one. But in fact such a
> rewrite does not help readability at all.
> It probably is not a coincidence that the scientist who did much early
> work on stacks is also the scientist who spent a lifetime working on
> program correctness (E.W.Dijkstra).
However (!) if stacks are used on real (rather than theoretical) hardware
then (limited) space must be allocated for them. It can be difficult to
prove that the maximum depth is never exceeded. In a recursive situation it
may even be impossible to prove this as Ackerman's fuction can easily

Received on Mon Aug 09 2004 - 00:02:35 BST

This archive was generated by hypermail 2.3.0 : Fri Oct 10 2014 - 23:36:33 BST