8 Aug
2004
8 Aug
'04
5:02 p.m.
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
demonstrate.
Andy